Run-script
Run a script.
Run-script is a utility for testing evaluation of the forms in
a given file, to check that the output is as expected. The forms need not be
embedded event forms (see events), and they need not all evaluate
successfully; for example, a thm form may produce a failed proof
attempt.
General form:
(run-script NAME
:inhibited-summary-types i-s-t ; default '(time steps)
:inhibit-output-lst i-o-l ; default '(proof-tree)
:ld-error-action action ; default ':continue
)
where the keyword arguments are evaluated. For information on the keyword
arguments, see set-inhibited-summary-types, set-inhibit-output-lst, and ld-error-action.
Example form:
(run-script "mini-proveall")
When you call (run-script NAME), the forms in NAME-input.lsp
are evaluated and a transcript is written to NAME-log.out.
Forms that are commands change the logical world.
NOTE: The time-tracker utility is disabled by run-script.
After a call of run-script, you need to evaluate (time-tracker t) if
you want to return to the default behavior (where the time-tracker capability
is enabled). Similarly, printing of ‘; Hons-Note’ comments
are suppressed by run-script (more precisely: whenever state
global 'script-mode has a non-nil value).
To use run-script for regression testing, you will need
to create three files in addition to the input file, as described below.
For an example, see the files books/demos/mini-proveall-*.* in
the community-books; there, NAME is mini-proveall.
- NAME-input.lsp — the file of forms to be evaluated
- NAME-book.acl2 — a file containing the following, where the
indicated zero or more include-book forms are exactly those that are
in NAME-input.lsp (note that the form (ubu 1) can perhaps be omitted
but is needed in some cases, e.g., see
books/projects/paco/books/proveall-book.acl2)
(include-book "tools/run-script" :dir :system)
(run-script "NAME") ; optionally add keyword arguments
(ubu 1)
; Help dependency scanner.
#||
(depends-on "NAME-log.txt")
(depends-on "NAME-input.lsp")
(include-book ...)
(include-book ...)
...
||#
- NAME-book.lisp — a small file containing only these two forms:
(in-package "ACL2")
(assert-event
(identical-files-p "NAME-log.txt" "NAME-log.out"))
- NAME-log.txt — the expected result from evaluating the forms in
NAME-input.lsp
To create NAME-log.txt, initially create it as the empty file (or,
actually, create any file with that name). Then run the test, for example
using cert.pl (see build::cert.pl) as follows.
<PATH_TO_books/build>/cert.pl -j 8 NAME-book
Now inspect the generated file NAME-log.out. When you are satisfied
that it is as expected, move it to NAME-log.txt. The cert.pl
command displayed above should now succeed.
NOTE: If you fail to create file NAME-log.txt, you will likely see an
error message of the following form when you run cert.pl.
make: *** No rule to make target `NAME-log.txt', needed by `NAME-book.cert'.
The solution is to create the missing file NAME-log.txt, for example
with the following shell command.
touch NAME-log.txt
Remarks.
- Note for ACL2(r) users: The prompt is set by run-script so that the
usual "(r)" is not printed.
- If you want commands like :pe to avoid printing event
numbers, put the form (assign script-mode 'skip-ldd-n) into your
*-input.lsp file. See community-book file
demos/floating-point-input.lsp for an example.
- Run-script always sets gag-mode to its default,
:goals.
