• 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-run-background

          Use tshell to run a sub-program in the background; don't wait for it to finish and don't get any output from it. (never forks ACL2).

          Signature
          (tshell-run-background cmd) → nil
          Arguments
          cmd — The command to give to the shell. It had better be well-formed. It can probably use input/output redirection without problems. We're basically going to run: (cmd) &.
              Guard (stringp cmd).

          Definitions and Theorems

          Function: tshell-run-background

          (defun tshell-run-background (cmd)
            (declare (xargs :guard (stringp cmd)))
            (let ((__function__ 'tshell-run-background))
              (declare (ignorable __function__))
              (cw "Warning: under-the-hood definition of ~s0 not installed?"
                  __function__)))