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
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

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

Reply via email to