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.
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.,
This is a thin wrapper around
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