Get the "application level" command line arguments passed to ACL2.
(argv &optional (state 'state)) → (mv arguments state)
In the logic, this function reads from the ACL2 oracle and coerces whatever it finds into a string-listp. In the execution, we use whatever mechanism the host Lisp provides for reading the command line arguments that were given to ACL2.
Dead simple, right? Well, not really.
Usually ACL2 itself, or any custom program you build atop ACL2 using save-exec, is really just an image that is executed by the runtime for the host Lisp. For instance, when you build ACL2 on CCL, you get:
#!/bin/sh export CCL_DEFAULT_DIRECTORY=/path/to/ccl exec /path/to/ccl/lx86cl64 -I /path/to/saved_acl2.lx86cl64 -K ISO-8859-1 -e "(acl2::acl2-default-restart)" -- "$@"
So this script is invoking the Lisp runtime, named
The important thing to note here is that command-line options like
Fortunately, most Lisps have a special mechanism to separate their runtime
options from the application options. In Allegro, CCL, CLISP, and CMUCL, this
is done with a special
So on these Lisps, as long as you are running ACL2 or your save-image using
a "proper" shell script,
Unfortunately, GCL and LispWorks do not have such an option, so on these Lisps we do something very half-assed:
So even though the Lisp doesn't know about
But this isn't perfect. Since the Lisp doesn't know to stop processing
options when it sees
(defun argv-fn (state) (declare (xargs :stobjs (state))) (declare (xargs :guard t)) (let ((__function__ 'argv)) (declare (ignorable __function__)) (b* ((- (raise "Raw Lisp definition not installed?")) ((mv err val state) (read-acl2-oracle state))) (if (and (not err) (string-listp val)) (mv val state) (mv nil state)))))
(defthm string-listp-of-argv.arguments (b* (((mv ?arguments acl2::?state) (argv-fn state))) (string-listp arguments)) :rule-classes :rewrite)
(defthm state-p1-of-argv.state (implies (force (state-p1 state)) (b* (((mv ?arguments acl2::?state) (argv-fn state))) (state-p1 state))) :rule-classes :rewrite)
(defthm true-listp-of-argv (true-listp (mv-nth 0 (argv))) :rule-classes :type-prescription)