Sys-call
Make a system call to the host operating system
Example Forms:
(sys-call "cp" '("foo.lisp" "foo-copied.lisp"))
(prog2$ (sys-call "cp" '("foo.lisp" "foo-copied.lisp"))
(sys-call-status state))
The first argument of sys-call is a command for the host operating
system, and the second argument is a list of strings that are the arguments
for that command.
The use of prog2$ in the second example form above is optional, but
illustrates how to get the return status. See sys-call-status.
Sys-call itself always returns nil.
WARNING: The details of how sys-call works can vary among
different host Lisp implementations! Consider for example wildcard expansion,
such as when executing the form (sys-call "ls" '("*.lisp")). For
ACL2 built on Allegro CL, CCL, CMUCL, GCL, or SBCL, we have seen this result
in an error message such as "No such file or directory", even though
files with names of the form *.lisp are present in the current
directory; but for ACL2 built on LispWorks, a list of such filenames is
printed.
More generally, we note that sys-call does not provide some features
that one may expect of a shell. We mentioned wildcard expansion above; other
sorts of shell expansion may also not be supported, such as ~/.
Sys-call also does not directly support output redirection. If you want
to run a program, P, and redirect its output, one option is to create a
wrapper script, W to call instead. Thus W might be a shell script
containing the line:
P $* >& foo.out
Another approach is suggested by a passage in the CCL
manual: call the shell program. For example, here is how one might list
the .lisp files in a directory.
(sys-call "sh" '("-c" "ls *.lisp"))
For related utilities, see sys-call* and sys-call+. Both of
those utilities return a suitable status (rather than requiring a separate
call of a separate function, sys-call-status, as described later
below). Also, sys-call+ returns the command's output, but (like
sys-call) sys-call* does not. An important distinction is that both
sys-call+ and sys-call* can make their calls to the operating system
during proofs, unlike sys-call as we now explain.
Sys-call does not invoke the operating system when it is invoked
inside the theorem prover or proof-builder. The following example,
from Eric Smith, illustrates this point: presumably we only want to reason
about the return value, not write a file during a proof!
(defttag foo)
(thm (equal (sys-call "touch" (list "/tmp/XXX"))
nil)
:hints (("Goal" :in-theory (disable (:type-prescription sys-call)))))
Through Version 7.4, running this example did indeed create file
/tmp/XXX if that file did not already exist. Now, the executable-counterpart of sys-call is disabled, which avoids that
specific behavior. Moreover: even with that executable-counterpart enabled,
no file is created; sys-call returns nil without invoking the
operating system. If such an evaluation attempt occurs during invocation of a
clause-processor or metafunction, then an error will be
signaled.
General Form:
(sys-call cmd args)
This function logically returns nil. However, it makes the indicated
call to the host operating system, as described above (not during a proof),
using a function supplied ``under the hood'' by the underlying Lisp system.
This is an advanced feature that requires a trust tag (see below). As noted
above, host lisps differ on their handling of sys-call; see the raw Lisp
definition of ACL2 source function system-call for details, including
exactly the underlying Lisp code that is invoked. You can then look at that
host lisp's manual for details about that underlying function.
On occasions where one wishes to obtain the numeric status returned by the
host operating system (or more precisely, by the Lisp function under the hood
that passes the system call to the host operating system), one may do so; see
sys-call-status. The status value is the value returned by that Lisp
function, which may well be the same numeric value returned by the host
operating system for the underlying system call.
Note that sys-call does not touch the ACL2 state; however,
sys-call-status updates the acl2-oracle field of the
state.
Be careful if you use sys-call! It can be used for example to
overwrite files, or worse! We view a use of sys-call as a call to the
operating system that is made outside ACL2. The following example from Bob
Boyer shows how to use sys-call to execute, in effect, arbitrary Lisp
forms. ACL2 provides a ``trust tag'' mechanism that requires execution of a
defttag form before you can use sys-call; see defttag.
(Note: The setting of the raw Lisp variable *features* below is just to
illustrate that any such mischief is possible. Normally *features* is a
list with more than a few elements. Also, note that this log is from many
years ago; the feature shown, :AKCL-SET-MV, is no longer present.)
% cat foo
print *0x85d2064=0x838E920
detach
q
% acl2
... boilerplate deleted
ACL2 !>(sys-call "gdb -p $PPID -w < foo >& /dev/null " nil)
NIL
ACL2 !>:q
Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP).
ACL2>*features*
(:AKCL-SET-MV)
ACL2>
Subtopics
- Sys-call+
- Make a system call to the host OS, returning status and output
- Tshell
- A fancy alternative to sys-call that features output streaming
and capture, exit-code capture, interruption, and better control over when
forking occurs.
- Sys-call-status
- Exit status from the preceding system call
- Sys-call*
- Make a system call to the host OS, returning a status
