Tshell-call
Use tshell to run a sub-program and wait for it to finish. (never
forks ACL2).
- Signature
(tshell-call cmd &key (print 't) (save 't) (state 'state))
→
(mv exit-status lines state)
- Arguments
- cmd — This is the command to run. It can actually be a full-blown shell script.
It should not require any input from the user.
Guard (stringp cmd).
- print — This says whether we should print the lines produced by cmd as
they are produced. nil means print nothing, t means print
everything, and any other symbol fn means call the raw Lisp
function fn to do the printing. Custom output functions are an
advanced feature; see tshell-raw.lsp for details.
Guard (symbolp print).
- save — This says whether we should capture the stdout/stderr lines produced
by cmd and return them as the lines output. If you aren't
going to analyze the program's output, you might want to set this to
nil to cut down on memory usage.
Guard (booleanp save).
- Returns
- exit-status — The exit code from the command. Typically 0 means success
and any non-zero value means failure. This is only
sensible if finishedp is t.
Type (natp exit-status).
- lines — The output from the command (from both standard output and
standard error.) Note that lines will always just be
nil if you're using :save nil.
Type (string-listp lines).
- state — Type (state-p1 state), given (state-p1 state).
Before using tshell-call you need to make sure that the bash
processes for tshell have been started; see tshell-start and tshell-ensure.
Note that :save and :print are independent from one-another; you
can print without saving, save without printing, save and print, or do neither
and just get the exit code.
Definitions and Theorems
Function: tshell-call-fn
(defun tshell-call-fn (cmd print save state)
(declare (xargs :stobjs (state)))
(declare (xargs :guard (and (stringp cmd)
(symbolp print)
(booleanp save))))
(let ((__function__ 'tshell-call))
(declare (ignorable __function__))
(b* (((mv exit-status lines state)
(tshell-call-fn1 cmd print save state)))
(mv (nfix exit-status)
(if (string-listp lines) lines nil)
state))))
Theorem: natp-of-tshell-call.exit-status
(defthm natp-of-tshell-call.exit-status
(b* (((mv ?exit-status ?lines ?state)
(tshell-call-fn cmd print save state)))
(natp exit-status))
:rule-classes :type-prescription)
Theorem: string-listp-of-tshell-call.lines
(defthm string-listp-of-tshell-call.lines
(b* (((mv ?exit-status ?lines ?state)
(tshell-call-fn cmd print save state)))
(string-listp lines))
:rule-classes :rewrite)
Theorem: state-p1-of-tshell-call.state
(defthm state-p1-of-tshell-call.state
(implies (state-p1 state)
(b* (((mv ?exit-status ?lines ?state)
(tshell-call-fn cmd print save state)))
(state-p1 state)))
:rule-classes :rewrite)
Theorem: state-p-of-mv-nth-2-of-tshell-call-fn-when-state-p
(defthm state-p-of-mv-nth-2-of-tshell-call-fn-when-state-p
(implies (state-p state)
(state-p (mv-nth 2
(tshell-call-fn cmd print save state)))))
Theorem: w-of-mv-nth-2-of-tshell-call-fn
(defthm w-of-mv-nth-2-of-tshell-call-fn
(equal (w (mv-nth 2
(tshell-call-fn cmd print save state)))
(w state)))
Subtopics
- Tshell-call-unsound
- Unsound variant of tshell-call which doesn't take state.
