• 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
      • Output-controls
      • Macros
      • Interfacing-tools
        • Io
        • Defttag
        • Sys-call
        • Save-exec
        • Quicklisp
        • Std/io
        • Oslib
        • Bridge
        • Clex
        • Tshell
          • Tshell-call
          • Tshell-call-unsound
          • Tshell-call-fn1
          • Tshell-ensure
            • Tshell-start
            • Tshell-run-background
            • Tshell-call-unsound-fn1
          • Unsound-eval
          • Hacker
          • ACL2s-interface
          • Startup-banner
          • Command-line
      • Interfacing-tools
        • Io
        • Defttag
        • Sys-call
        • Save-exec
        • Quicklisp
        • Std/io
        • Oslib
        • Bridge
        • Clex
        • Tshell
          • Tshell-call
          • Tshell-call-unsound
          • Tshell-call-fn1
          • Tshell-ensure
            • Tshell-start
            • Tshell-run-background
            • Tshell-call-unsound-fn1
          • Unsound-eval
          • Hacker
          • ACL2s-interface
          • Startup-banner
          • Command-line
        • Hardware-verification
        • Software-verification
        • Math
        • Testing-utilities
      • Tshell

      Tshell-ensure

      Ensure that shells are available for running sub-processes (may fork ACL2).

      Signature
      (tshell-ensure &optional (n '1)) → nil
      Arguments
      n — How many shells to start.
          Guard (posp n).

      If you want to use this in a book, you can wrap it in a value-triple, e.g.,

      (value-triple (tshell-ensure))

      It's also typically useful to put this before calls of tshell-call or tshell-run-background, to start up the shells if the user hadn't already gotten them started earlier.

      This is essentially just shellpool:ensure; see the Shellpool API documentation for details.

      Definitions and Theorems

      Function: tshell-ensure-fn

      (defun tshell-ensure-fn (n)
        (declare (xargs :guard (posp n)))
        (declare (ignorable n))
        (let ((__function__ 'tshell-ensure))
          (declare (ignorable __function__))
          (cw "Warning: under-the-hood definition of ~s0 not installed?"
              __function__)))