SBCL stores all proof commands in ALL CAPS; this confuses Allegro (sometimes)
file-targetting proof commands (status-proof-pvs-file, prove-pvs-file, etc.) finish with a message such as
PVS file pythagoras.pvs not found
Proof commands that interact with the user such as (undo), (quit), or the prompt whether one would like to save a proof when it's done, don't show up in the *pvs* buffer right away. Instead, for instance, after a proof was finished
Trying repeated skolemization, instantiation, and if-lifting,
Q.E.D.
^G
shows up. The prompt is not shown before something is entered (y in this case, and then no).
y
Would you like the proof to be saved? (yes or no)
Please type "yes" for yes or "no" for no.
no
Would you like the proof to be saved? (yes or no)
Run time = 0.18 secs.
Real time = 145.20 secs.
NIL
PVS(26):
Times reported for proofs look wrong. They typically are, e.g.
little_known_pythagorean..............proved - complete [SHOSTAK](0.00 s)
even when considerable time was spent running that proof.
status-proof-pvs-file,prove-pvs-file, etc.) finish with a message such as(undo),(quit), or the prompt whether one would like to save a proof when it's done, don't show up in the*pvs*buffer right away. Instead, for instance, after a proof was finishedshows up. The prompt is not shown before something is entered (
yin this case, and thenno).