• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Recursion-and-induction
      • Hons-and-memoization
      • Events
      • Parallelism
      • History
      • Programming
      • Operational-semantics
      • Real
      • Start-here
        • Gentle-introduction-to-ACL2-programming
        • ACL2-tutorial
          • Introduction-to-the-theorem-prover
          • Pages Written Especially for the Tours
          • The-method
          • Advanced-features
          • Interesting-applications
          • Tips
          • Alternative-introduction
          • Tidbits
          • Annotated-ACL2-scripts
          • Startup
          • ACL2-as-standalone-program
          • ACL2-sedan
            • Defunc
            • Cgen
              • Defdata
              • Test?
              • ACL2s-defaults
              • Prove/cgen
              • Register-type
              • With-timeout
                • Defdata-attach
                • Testing-enabled
                • Defdata-aliasing-enabled
                • Cgen-single-test-timeout
                • Verbosity-level
                • Search-strategy
                • Num-print-counterexamples
                • Cgen-timeout
                • Cgen-local-timeout
                • Num-witnesses
                • Num-trials
                • Num-print-witnesses
                • Test-then-skip-proofs
                • Sampling-method
                • Recursively-fix
                • Num-counterexamples
                • Backtrack-limit
                • Print-cgen-summary
                • Cgen::flush
                • Backtrack-bad-generalizations
                • Use-fixers
                • Thm-no-test
                • Defthmd-no-test
                • Defthm-no-test
              • Ccg
              • Defdata
              • ACL2s-user-guide
              • ACL2s-tutorial
              • ACL2s-implementation-notes
              • Match
              • ACL2s-faq
              • ACL2s-intro
              • ACL2s-defaults
              • Definec
              • ACL2s-utilities
              • ACL2s-interface
              • ACL2s-installation
            • Talks
            • Nqthm-to-ACL2
            • Emacs
          • About-ACL2
        • Debugging
        • Miscellaneous
        • Output-controls
        • Macros
        • Interfacing-tools
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Cgen
    • Miscellaneous

    With-timeout

    Evaluate form with a timeout (in seconds)

    Evaluate form with a timeout in seconds.

    The general form is:

    with-timeout duration body timeout-form

    duration can be any rational value. A duration of 0 seconds disables the timeout mechanism, i.e its a no-op. Suppose it is not, and duration seconds elapse during evaluation of body then the evaluation is aborted and the value of timeout-form is returned; in the normal case the value of body is returned.

    The signature of body and timeout-form should be the same.

    Advanced Notes:

    This form should be called either at the top-level or in an environment where state is available and body has no free variables other than state. If the timeout-form is a long running computation, then the purpose of with-timeout is defeated.

    Usage: 
    (with-timeout 5 (fibonacci 40) :timed-out) 
    :doc with-timeout