• 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-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__)))