• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • 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__)))