David Aspinall <david.aspin...@ed.ac.uk> writes:

   useful hints in most cases.  Personally, I would think that running a
   big cvs update in the middle of scripting a complex file that depends
   on the libraries you're updating is not a sensible idea!!

With PVS I do this now and then for validating proof scripts in
the background. For instance, when working in B I notice that I
have to change something in A, where B depends on A. So I change
A, commit the changes to cvs and checkout a fresh copy in some
temp directory. In this temp directory I start a validation run
of all proofs, which can consume several hours. While this is
running I continue my original work in B (which is possible with
PVS, because PVS keeps proofs separate, such that you can
typecheck definitions and theorems without running any proofs).

When the validation run is finished I turn to the temp directory
and fix those proofs, that broke because of my changes in A. This
might require further changes... which I copy back into the
original directory. I then continue working on B, while the temp
directory runs another validation run in the background...

With coq this style of work is not (yet) possible, because you
cannot work in B, when A contains a broken proof. But hopefully
there will be an option -skip-proofs some day.

Changing files in the background also happens when working at
home: When finished at home I copy the sources to work and
hibernate the computer at home with the running proof assistant.
At work I continue and later I start the computer at home and
copy the changes from work. For the proof assistant at home files
were updated in the background. It should automatically detect
which files needs recompilation...


ProofGeneral-devel mailing list

Reply via email to