Hi Hendrik, Quick reply to your second message:
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,
...
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.
Thanks a lot for explaining these use cases. I think it's a good way to think about the scenarios that should be supported, or, at least, not prevented.
If the developer believes (or the system knows) that the proofs are not going to be broken by changed statements or missing definitions, etc, then continuing scripting while there are updates in ancestors is OK, of course. If the changes are made by someone else you might want to be more careful!
The simple-minded file-level locking/decoration is supposed to give a little bit of information so that the developer has some interaction to point out these dependencies and finds out about changes. If you're closely aware of the dependencies (e.g. through writing Makefiles and running compiler on command line), it probably doesn't matter much. I think that was the conclusion Pierre persuaded me of last time I raised the multiple file support with him. Maybe once people get used to automatic compilation it would seem useful.
I'll think about your second message in a bit more detail and respond in a while.
Meanwhile, I encourage you to develop a patch which supports the uses you're most interested in!
Best wishes, - David _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
