TCCs going from "proved-complete" to "unfinished"

[Giulia Sindoni]

Hello,

Hope this is the right place for this kinds of questions!

My question relates TCCs,  bin files and batch mode with Prooflite.

Why do we TCCs go (sometimes, not always) from being "proved-complete" to being "unfinished", when I start a new pvs session? 

I noticed this when running a theorem in batch mode: the theorem was suddenly showing as proved-incomplete, even though it was previously showing as proved-complete (all lemmas on which the proof was based were proved and TCCs of all imported theories where proved too).

Thus I checked the TCCs of all relating theories, and they went indeed from "proved-complete" to "unfinished".  So, I had to rerun the TCCs. They had already being proved so the proofs were saved in the prf file. Then, the TCCs showed as "proved-complete". Then, when I run a theorem in batch mode, it showed as "proved-complete" again. But if I start a new session,  how do I make sure my TCCs stay "proved-complete"? I expect the issue might arise again in a new session.

Also, if I run a proof of the same theorem in the Emacs interactive mode, by running prove-proofchain, all the TCCs and lemmas relating to that theorem  are “proved-complete” (as expected) and the theorem is “proved-complete” too.

There is a mismatch between batch mode and interactive mode. I think maybe the bin files don’t get updated properly? 

Cheers,

Giulia

[Mariano Moscato]

Hi Giulia,

This is the right place for asking these questions :-)

Personally, I don't use very much this kind of precomupted information, but as long as I know this information is not stored in the binary files. The reason I believe is that the user files (in particular, `.pvs` and `.prf`) could have been changed between a pvs session and the next, so it's safer to asume nothing has been proved before the start of the current session.

If you development is big enough, I see having this information precomputed could save you a good amount of time. It would need some work on the PVS side to check that the latest date of modification of the user files is older than the binary files, but this check should be faster than rerunning all the proofs in such cases. If you are interested in this, I'd suggest to add an issue in the pvs repository: https://github.com/SRI-CSL/PVS/issues

By the way, which version of PVS are you using? PVS 7.1 or 8.0?

Kindly,

Mariano.

[Giulia Sindoni]

Hi Mariano,

Thank you so much for your quick reply!

I’m using PVS 8.0.

What you say makes sense, it is safer to assume nothing has been proved before the start of the current session. 

For me, the thing is that I’m ultimately looking at running PVS mainly in batch mode. Thus, I want to avoid opening the Emacs interface every time, and ask PVS to re-run the proofs of the TCCS, so that my theorem shows as proved AND complete. 

But maybe there is something similar to “prove-proofchain” (the command that on Emacs that analyses all the theorem's dependencies, checks the TCCSs and prints a summary), but instead does this in batch mode, i.e. using proveit?

I do understand, though, that PVS was born as an interactive theorem prover, so it makes sense that things are better suited to be run via the user-interface, rather than in batch mode.

Thanks again so much!

Giulia

[Mariano Moscato]

Hi Giulia,

It makes perfect sense to use PVS in batch mode. You can have proveit to prove every dependency of a given theory by using the `-i` option (you can see a description of this and other options in https://github.com/nasa/pvslib/blob/master/docs/Scripts.md or by typing `proveit --help`).

Let me know if this does the trick for you.

Kindly,
Mariano.

[Giulia Sindoni]

Thank you Mariano, that is really helpful!

Giulia