dump-sequent does not produce the promised `th-<theory name>.sequent` file

SRI-CSL / PVS

The People's Verification System

http://pvs.csl.sri.com

GNU General Public License v2.0

132 stars 32 forks source link

dump-sequent does not produce the promised `th-<theory name>.sequent` file #89

Open kai-e opened 1 year ago

kai-e commented 1 year ago

I'm chasing the cause of some proofs being tagged incomplete. Issuing M-x dump-sequent and answering y to the prompt doesn't produce a file (I can find). The only trace is in the buffer pvs which has these lines added:

sent:{(setq *dump-sequents-to-file* t)}

rec:{ 
t
pvs(51): }

rec:{nil
pvs(52): }

kai-e commented 1 year ago

This might be a smaller issue. Some files in lib/finite_sets appeared to have unfinished/untried proofs. I reran those and the .sequents files began to appear.

kai-e commented 1 year ago

Accidentally closed. Sorry for the noise. I do believe it's still an issue.