		Search-engine friendly clone of the ACL2 documentation.

Output-controls

Pso

Show the most recently saved output

Evaluate :pso in order to print output that was generated in an environment where output was being saved, as in gag-mode, which is active when ACL2 is invoked. Also see gag-mode.

Example Forms:

:pso                        ; Print saved output.

(pso)                       ; equivalent to the above
(pso :all)                  ; equivalent to the above
(pso :all nil)              ; equivalent to the above

(pso "Subgoal *1/2''")      ; Print saved output only for "Subgoal *1/2''".

(pso '"Subgoal *1/2'5'"
      "Subgoal *1/2'14'")   ; Print saved output starting with the output
                            ; for '"Subgoal *1/2'5'" and ending just
                            ; before the output for "Subgoal *1/2'14'".

(pso '("Subgoal *1/2'5'"  "Subgoal *1/2''")
     '("Subgoal *1/2'14'" "Subgoal *1/2'12'")
                            ; Print saved output
                            ; starting with the output for either
                            ; "Subgoal *1/2'5'" or "Subgoal *1/2''"
                            ; (whichever comes first)
                            ; and stopping just before the output for either
                            ; "Subgoal *1/2'14'" or "Subgoal *1/2'12'"
                            ; (whichever comes first).

General Form:

(pso start-goals-spec ; optional: default is :ALL
     stop-goals-spec  ; optional: default is NIL
     )

where both arguments are optional and have the defaults shown above. Thus, the keyword command :pso is equivalent to each of (pso), (pso :all), and (pso :all nil); see keyword-commands. The optional arguments restrict the output to specified goals, as follows; but the examples above probably provide an easier way to understand those arguments than the following explanation.

Start-goals-spec represents the set of start goal names. Its effects are described below. The value :all represents the set of all goal names, a string represents the set consisting of just that one goal name, and a list represents the set of all goal names in that list.
Stop-goals-spec represents the set of stop goal names. Its effects are described below, following the same conventions as above except that :all is not allowed.
Printing begins immediately if start-goals-spec is :all, else begins with the first goal whose name is in the set of start goal names.
If the set of stop goal names is empty (as is the case when the second optional argument is omitted), then printing takes place only for the first goal whose name is in the set of start goal names. Otherwise, printing continues starting with that goal, stopping only when a goal in the list of stop goal names is encountered, without any printing for that goal.

Note that saved prover output is cleared at every top-level prover call, including such calls made by: events (e.g., defthm and defun), thm, and proof-builder commands that invoke the prover. A single event can make more than one top-level prover call, for example: in the case of defun, one call made for termination and another for guard verification; and in the case of defthm, one call made for the proposed theorem and one for each corollary. If you want to see more than one proof log for a single top-level form, then instead of using :pso, first evaluate (set-gag-mode nil).

The ``Time'' printed in the summary shows the original times for the proof attempt, not the times for processing the :pso command.

Also see pso!, psog, psof, set-gag-mode, set-inhibit-output-lst, and set-print-clause-ids.