run-script

(in-package "ACL2")

(defxdoc run-script
  :parents (testing-utilities)
  :short "Run a script."
  :long "<p>@('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 @(see events)), and they need not all evaluate
 successfully; for example, a @(tsee thm) form may produce a failed proof
 attempt.</p>

 <p>General form:</p>

 @({
 (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
             )
 })

 <p>where the keyword arguments are evaluated.  For information on the keyword
 arguments, see @(tsee set-inhibited-summary-types), @(tsee
 set-inhibit-output-lst), and @(tsee ld-error-action).</p>

 <p>Example form:</p>

 @({
 (run-script "mini-proveall")
 })

 <p>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 @(see command)s change the logical world.</p>

 <p>NOTE: The @(see 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 &lsquo;@('; Hons-Note')&rsquo; comments
 are suppressed by @('run-script') (more precisely: whenever @(see state)
 global @(''script-mode') has a non-@('nil') value).</p>

 <p>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 @(see community-books); there, @('NAME') is @('mini-proveall').</p>

 <ul>

 <li>@('NAME-input.lsp') &mdash; the file of forms to be evaluated</li>

 <li>@('NAME-book.acl2') &mdash; a file containing the following, where the
 indicated zero or more @(tsee 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 ...)
 ...
 ||#
 })</li>

 <li>@('NAME-book.lisp') &mdash; a small file containing only these two forms:

 @({
 (in-package "ACL2")
 (assert-event
  (identical-files-p "NAME-log.txt" "NAME-log.out"))
 })</li>

 <li>@('NAME-log.txt') &mdash; the expected result from evaluating the forms in
 @('NAME-input.lsp')</li>

 </ul>

 <p>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 @(see build::cert.pl)) as follows.</p>

 @({
 <PATH_TO_books/build>/cert.pl -j 8 NAME-book
 })

 <p>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.</p>

 <p>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').</p>

 @({
 make: *** No rule to make target `NAME-log.txt', needed by `NAME-book.cert'.
 })

 <p>The solution is to create the missing file @('NAME-log.txt'), for example
 with the following shell command.</p>

 @({
 touch NAME-log.txt
 })

 <p><b>Remarks.</b></p>

 <ul>

 <li>Note for ACL2(r) users: The prompt is set by @('run-script') so that the
 usual "(r)" is not printed.</li>

 <li>If you want commands like @(':')@(tsee pe) to avoid printing event
 numbers, put the form @('(assign script-mode 'skip-ldd-n)') into your
 @('*-input.lsp') file.  See @(see community-book) file
 @('demos/floating-point-input.lsp') for an example.</li>

 <li>@('Run-script') always sets @(tsee gag-mode) to its default,
 @(':goals').</li>

 </ul>")