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