• 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
          • Sys-call+
          • Tshell
            • Tshell-call
            • Tshell-call-unsound
            • Tshell-call-fn1
            • Tshell-ensure
              • Tshell-start
              • Tshell-run-background
              • Tshell-call-unsound-fn1
            • Sys-call-status
            • 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
            • Sys-call+
            • Tshell
              • Tshell-call
              • Tshell-call-unsound
              • Tshell-call-fn1
              • Tshell-ensure
                • Tshell-start
                • Tshell-run-background
                • Tshell-call-unsound-fn1
              • Sys-call-status
              • 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__)))