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
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
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
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
Meanwhile, I encourage you to develop a patch which supports the uses
you're most interested in!
ProofGeneral-devel mailing list
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.