Tshell-call-unsound
Unsound variant of tshell-call which doesn't take state.
- Signature
(tshell-call-unsound cmd &key (print 't) (save 't))
→
(mv exit-status lines)
- 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).
This is equivalent to the old version of tshell-call, before
it was made sound by adding state.
It is unsound because it is not functional; two executions with the same
arguments might yield different results.
See tshell-call for usage information.
Definitions and Theorems
Function: tshell-call-unsound-fn
(defun tshell-call-unsound-fn (cmd print save)
(declare (xargs :guard (and (stringp cmd)
(symbolp print)
(booleanp save))))
(let ((__function__ 'tshell-call-unsound))
(declare (ignorable __function__))
(progn$
(cw "Warning: under-the-hood definition of ~s0 not installed?"
__function__)
(tshell-call-unsound-fn1 cmd print save))))
Theorem: natp-of-tshell-call-unsound.exit-status
(defthm natp-of-tshell-call-unsound.exit-status
(b* (((mv ?exit-status ?lines)
(tshell-call-unsound-fn cmd print save)))
(natp exit-status))
:rule-classes :type-prescription)
Theorem: string-listp-of-tshell-call-unsound.lines
(defthm string-listp-of-tshell-call-unsound.lines
(b* (((mv ?exit-status ?lines)
(tshell-call-unsound-fn cmd print save)))
(string-listp lines))
:rule-classes :rewrite)
Subtopics
- Tshell-call-unsound-fn1
- Unsound variant of tshell-call-fn1 which doesn't take state.
