list of discrepancies between SBCL- and Allegro-PVS

[kai-e]

1. SBCL stores all proof commands in ALL CAPS; this confuses Allegro (sometimes)
2. file-targetting proof commands (status-proof-pvs-file, prove-pvs-file, etc.) finish with a message such as

PVS file pythagoras.pvs not found

3. 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):

4. 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.