Re: [PG-devel] Proof tree code

[Paul A. Steckler]

Just to note, I'm adding a configuration option to force the use of the
existing Emacs mode, so Prooftree will always be available.

-- Paul
On May 13, 2016 11:08, "Pierre Courtieu"  wrote:

> 2016-05-13 9:49 GMT+02:00 Hendrik Tews :
> > 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.
>
> This might change with the idesave + Stm protocol.
>
> Paul are you using the Stm stuff?
>
> P.
> ___
> ProofGeneral-devel mailing list
> ProofGeneral-devel@inf.ed.ac.uk
> http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
>
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Re: [PG-devel] Proof tree code

[Pierre Courtieu]

2016-05-13 9:49 GMT+02:00 Hendrik Tews :
> 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.

This might change with the idesave + Stm protocol.

Paul are you using the Stm stuff?

P.
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Re: [PG-devel] Proof tree code

[Hendrik Tews]

Hi,

>> 2016-05-12 18:22 GMT+02:00 Paul A. Steckler :
>>> 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

Re: [PG-devel] Proof tree code

[Clément Pit--Claudel]

I think this would be the right strategy; Hendrik has been pretty good at 
keeping it up to until this point :)

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.
> 
> P.
> 
> 2016-05-12 18:22 GMT+02:00 Paul A. Steckler :
>> The code in generic/proof-tree appears to rely on proof shell modes.
>>
>> Is the `prooftree' tool in common use among Coq users?
>>
>> -- Paul
>> ___
>> ProofGeneral-devel mailing list
>> ProofGeneral-devel@inf.ed.ac.uk
>> http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
> ___
> ProofGeneral-devel mailing list
> ProofGeneral-devel@inf.ed.ac.uk
> http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
> 



signature.asc
Description: OpenPGP digital signature
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Re: [PG-devel] Proof tree code

[Pierre Courtieu]

I don't know. It is a nice peace of code. Maybe we can ask Hendrik to
port it once you have something working.

P.

2016-05-12 18:22 GMT+02:00 Paul A. Steckler :
> The code in generic/proof-tree appears to rely on proof shell modes.
>
> Is the `prooftree' tool in common use among Coq users?
>
> -- Paul
> ___
> ProofGeneral-devel mailing list
> ProofGeneral-devel@inf.ed.ac.uk
> http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
___
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel