Hi, >> 2016-05-12 18:22 GMT+02:00 Paul A. Steckler <st...@stecksoft.com>: >>> The code in generic/proof-tree appears to rely on proof shell modes. >>> >>> Is the `prooftree' tool in common use among Coq users?
I used it all the time ;-) For coq, prooftree needs the following: 1) a unique proof goal identifier 2) the full sequent text of additionally generated proof goals 3) information about the instantiation status of existential variables 4) which goals contain which existential variables 5) the updated sequent text once an existential variable got instantiated. The existing implementation does 1 and 3 by modifying the generated output from coq when coq runs under PG. 4 is done with a simple regular expression on the proof goal text. For 2 and 5 I insert additional print commands into the queue of commands. Because you cannot print wrt. an old state, these print commands need to be inserted directly after the command that generates additional subgoals or that instantiate existential variables. > On 2016-05-12 12:33, Pierre Courtieu wrote: >> I don't know. It is a nice peace of code. Maybe we can ask Hendrik to >> port it once you have something working. I agree here. Please go ahead for the moment and ignore proof tree. Unfortunately, I cannot promise that I will be able to update prooftree eventually. It would of course be nice if you keep an eye on the above requirements such that we can plug in prooftree eventually with only little changes. Bye, Hendrik This email and any attachments thereto may contain private, confidential, and/or privileged material for the sole use of the intended recipient. Any review, copying, or distribution of this email (or any attachments thereto) by others is strictly prohibited. If you are not the intended recipient, please contact the sender immediately and permanently delete the original and any copies of this email and any attachments thereto. _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
