		Search-engine friendly clone of the ACL2 documentation.

Tshell

A fancy alternative to sys-call that features output streaming and capture, exit-code capture, interruption, and better control over when forking occurs.

Tshell is an ACL2 wrapper around the Shellpool library for Common Lisp, which is available via quicklisp. It allows you to run external programs from within ACL2, and has many nice features for handling output, etc.

Shellpool has its own API documentation, which you may find useful.

Usage

Note that Tshell requires trust-tags because its implementation requires some raw Lisp code. The book to load is:

(include-book "centaur/misc/tshell" :dir :system)

After loading this book, the first step is then to launch one or more shells, e.g.,

(value-triple (tshell-ensure))

This is a thin wrapper around shellpool:ensure. It launches the subsidiary bash shells that tshell/shellpool will use to run programs. This step requires forking ACL2 itself, so you typically want to do this early in your ACL2 session, before you have allocated tons of memory.

After that, you can start launching programs using tshell-call or tshell-run-background. For instance,

ACL2 !>(tshell-call "echo hello")
(tshell-call "echo hello")
hello             ;; <-- output from subprogram, streamed
(0 ("hello"))   ;; <-- exit code 0, output lines

Subtopics

Tshell-call: Use tshell to run a sub-program and wait for it to finish. (never forks ACL2).
Tshell-call-unsound: Unsound variant of tshell-call which doesn't take state.
Tshell-call-fn1: Logical story for tshell-call.
Tshell-ensure: Ensure that shells are available for running sub-processes (may fork ACL2).
Tshell-start: Start additional shells for running sub-processes (forks ACL2).
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).
Tshell-call-unsound-fn1: Unsound variant of tshell-call-fn1 which doesn't take state.