David Aspinall <[email protected]> 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... Bye, Hendrik _______________________________________________ ProofGeneral-devel mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
