Major Section: ACL2-BUILT-INS
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-callis a command for the host operating system, and the second argument is a list of strings that are the arguments for that command. In GCL and perhaps other lisps, you can put the arguments with the command; but this is not the case, for example, in Allegro CL running on Linux.
The use of
prog2$ above is optional, but illustrates a typical sort
of use when one wishes to get the return status. See sys-call-status.
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, using a function supplied ``under the hood'' by the underlying Lisp system. 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.
sys-call does not touch the ACL2
sys-call-status updates the
file-clock field of the
state. One may
view that update as modifying the
fileclock to be at least as
recent as the time of the most recent
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
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.)
% 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>
Finally, we make a comment about output redirection, which also applies to
other related features that one may expect of a shell.
Sys-call does not
directly support output redirection. If you want to run a program,
and redirect its output, we suggest that you create a wrapper script,
to call instead. Thus
W might be a shell script containing the line:
P $* >& foo.outIf this sort of solution proves inadequate, please contact the ACL2 implementors and perhaps we can come up with a solution.