• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
      • Break-rewrite
      • Proof-builder
      • Accumulated-persistence
      • 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
        • Forward-chaining-reports
        • Proof-tree
        • Print-gv
        • Dmr
        • With-brr-data
        • Splitter
        • Guard-debug
        • Set-debugger-enable
        • Redo-flat
        • Time-tracker
        • Set-check-invariant-risk
        • Removable-runes
        • Efficiency
        • Explain-near-miss
        • Tail-biting
        • Failed-forcing
        • Sneaky
        • Invariant-risk
        • Failure
        • Measure-debug
        • Dead-events
        • Compare-objects
        • Prettygoals
        • Remove-hyps
        • Type-prescription-debugging
        • Pstack
        • Trace
        • Set-register-invariant-risk
        • Walkabout
        • Disassemble$
        • Nil-goal
        • Cw-gstack
        • Set-guard-msg
        • Find-lemmas
        • Watch
        • Quick-and-dirty-subsumption-replacement-step
        • Profile-all
        • Profile-ACL2
        • Set-print-gv-defaults
        • Minimal-runes
        • Spacewalk
        • Try-gl-concls
        • Near-misses
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • 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