• 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
      • Debugging
      • Miscellaneous
        • Term
        • Ld
        • Hints
        • Type-set
        • Ordinals
        • Clause
        • ACL2-customization
        • With-prover-step-limit
        • Set-prover-step-limit
        • With-prover-time-limit
        • Local-incompatibility
        • Set-case-split-limitations
        • Subversive-recursions
        • Specious-simplification
        • Defsum
        • Gcl
        • Oracle-timelimit
        • Thm
        • Defopener
        • Case-split-limitations
        • Set-gc-strategy
        • Default-defun-mode
        • Top-level
        • Reader
        • Ttags-seen
        • Adviser
        • Ttree
        • Abort-soft
        • Defsums
        • Gc$
        • With-timeout
          • Coi-debug::fail
          • Expander
          • Gc-strategy
          • Coi-debug::assert
          • Sin-cos
          • Def::doc
          • Syntax
          • Subversive-inductions
        • 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