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

4) which goals contain which existential variables

5) the updated sequent text once an existential variable got

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

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

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


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

Reply via email to