After hacking on PG all yesterday, and working out how to dispatch
between two shell modes, I think a forked, Coq-only version is the
better solution. Name suggestions? :-)

At the other end, I think that there should be a separate binary for
the XML (or whatever it turns out to be) protocol, say `coqserver'.
It's operating in a different way than coqtop-as-a-REPL. That would be
simplify the codebase for coqtop. Although I haven't yet dealt with
the extra channels that the toploop-coqide mode gives, I'm still
liking the idea of using HTTP and a REST API as the basic
communication mechanism.

-- Paul


On Fri, May 6, 2016 at 3:51 PM, David Aspinall <david.aspin...@ed.ac.uk> wrote:
> That sounds right (but could lead to confusion!).  What I did was to fork a
> version of PG and cut it down to something fairly minimal. - D.
>
>
> On 06/05/2016 14:34, Paul A. Steckler wrote:
>>
>> The proof-shell mode comes with a lot of associated state, like
>> regexps, buffers,  etc. Some bits of that state would be useful in the
>> new mode I'm creating, others not.
>>
>> I'm thinking that I can share the same state variables for the new
>> mode, because I'll never have an active proof shell mode and the new
>> mode active at the same time. Yes?
>> I'd hate to have to duplicate state.
>>
>> If I load two .v files in emacs, it seems I can only work on one at a
>> time using Proof General, and there's only one proof-shell mode window
>> active.
>>
>> -- Paul
>>
>>
>> On Fri, May 6, 2016 at 3:15 PM, David Aspinall <david.aspin...@ed.ac.uk>
>> wrote:
>>>
>>> I did something like this once to support PGIP, which was a sort of
>>> pre-cursor of PIDE based on exchanging XML messages. You can find the
>>> source in the CVS repo PG Kit repo (Kit/src/pgemacs).  But it probably
>>> isn't useful: it's about 10 years old and the case we wanted to allow
>>> was input coming voluntarily from the prover to PG (think
>>> progress/annotations etc), rather than the other way around.  - David
>>>
>>> On 06/05/2016 11:48, Paul A. Steckler wrote:
>>>>
>>>> Proof General defines a shell mode, proof-shell, and an associated
>>>> message filter. My thought now is to define an alternate-universe
>>>> shell mode, proof-shell-noprompt and an associated message filter.
>>>>
>>>> -- Paul
>>>>
>>>>
>>>>
>>>> On Fri, May 6, 2016 at 1:27 AM, Pierre Courtieu
>>>> <pierre.court...@cnam.fr> wrote:
>>>>>
>>>>> I am sorry to say that I already asked myself about everything you
>>>>> asked here, and, despite you suggest more smart answers than I did
>>>>> myself I don't see any good enough idea yet. About the prompt: a *lot*
>>>>> of things (everything really) in pg depend on the fact that 1 command
>>>>> = 1 prompt exactly.
>>>>>
>>>>> Once again, don't dismiss starting from scratch without thinking a
>>>>> while about it. Actually large parts of pg could be reused.
>>>>>
>>>>> P.
>>>>>
>>>>>
>>>>> 2016-05-05 19:59 GMT+02:00 Clément Pit--Claudel
>>>>> <clement....@gmail.com>:
>>>>>>
>>>>>> I entirely agree with this point; I argued in this direction on a
>>>>>> recent coq-dev thread.
>>>>>>
>>>>>> On 2016-05-05 12:24, Paul A. Steckler wrote:
>>>>>>>
>>>>>>> I'm not a fan of this idea. The IDE and the prover should be only
>>>>>>> loosely-coupled, with a clearly-defined communication protocol
>>>>>>> between
>>>>>>> them.
>>>>>>>
>>>>>>> A plugin introduces a tight coupling between these components. Yes,
>>>>>>> it's only a plugin, so the scope of the coupling is limited. But it
>>>>>>> still seems undesirable to me.
>>>>>>>
>>>>>>> -- Paul
>>>>>>>
>>>>>>> On Thu, May 5, 2016 at 4:58 PM, Clément Pit--Claudel
>>>>>>> <clement....@gmail.com> wrote:
>>>>>>>>
>>>>>>>> Not entirely clear to me :) I think there'd be some amount of design
>>>>>>>> work there as well.
>>>>>>>>
>>>>>>>> On 2016-05-05 10:39, Paul A. Steckler wrote:
>>>>>>>>>
>>>>>>>>> With that toploop plugin installed on the coqtop side installed,
>>>>>>>>> what
>>>>>>>>> does Proof General see from its shell?
>>>>>>>>>
>>>>>>>>> -- Paul
>>>>>>>>>
>>>>>>>>> On Thu, May 5, 2016 at 4:34 PM, Clément Pit--Claudel
>>>>>>>>> <clement....@gmail.com> wrote:
>>>>>>>>>>
>>>>>>>>>> Hi Paul,
>>>>>>>>>>
>>>>>>>>>> Here's another approach that I forgot to mention: we could build a
>>>>>>>>>> separate Emacs toploop as a plugin, which would inherit most of 
>>>>>>>>>> CoqIDE's
>>>>>>>>>> toploop (you know that I have mixed feelings about that, but it may 
>>>>>>>>>> be the
>>>>>>>>>> most pragmatic approach).
>>>>>>>>>>
>>>>>>>>>> Clément.
>>>>>>>>>>
>>>>>>>>>> On 2016-05-05 10:17, Clément Pit--Claudel wrote:
>>>>>>>>>>>
>>>>>>>>>>> Hi Paul,
>>>>>>>>>>>
>>>>>>>>>>> You could indeed modify PG to handle the first prompt
>>>>>>>>>>> differently, or even Coq.
>>>>>>>>>>> In the long run, though, I don't think the approach is
>>>>>>>>>>> sustainable. PG is very much hardcoded to expect one prompt for 
>>>>>>>>>>> every query
>>>>>>>>>>> it sends: thus, even though you may get something working pretty 
>>>>>>>>>>> quickly by
>>>>>>>>>>> hacking around this prompt thing, I think we'll see more breakages 
>>>>>>>>>>> with
>>>>>>>>>>> every evolution of the new protocol.
>>>>>>>>>>>
>>>>>>>>>>> Here's a slightly different idea. Right now, PG adds an
>>>>>>>>>>> abstraction layer on top of a REPL model. What you could do is 
>>>>>>>>>>> reimplement
>>>>>>>>>>> the same abstraction, but on top of Coq's new asynchronous model.
>>>>>>>>>>> Concretely, my suggestion is to make a separate library to talk to 
>>>>>>>>>>> Coq's new
>>>>>>>>>>> API, which would provide the same interface 
>>>>>>>>>>> (proof-shell-invisible-command,
>>>>>>>>>>> proof-shell-ready-prover, proof-shell-invisible-cmd-get-result, 
>>>>>>>>>>> etc.).
>>>>>>>>>>>
>>>>>>>>>>> I think this would make your life easier. You would:
>>>>>>>>>>>
>>>>>>>>>>> 1. Identify a small (hopefully) collection of functions that
>>>>>>>>>>> Coq-ProofGeneral actually depends on (some sort of semi-explicit 
>>>>>>>>>>> interface,
>>>>>>>>>>> essentially).
>>>>>>>>>>> 2. Implement support for these functions using Coq's new API
>>>>>>>>>>> model
>>>>>>>>>>> 3. Modify the current implementation to call these functions or
>>>>>>>>>>> the legacy ones depending on the version of Coq.
>>>>>>>>>>>
>>>>>>>>>>> What do you think?
>>>>>>>>>>> Clément.
>>>>>>>>>>>
>>>>>>>>>>> On 2016-05-05 09:48, Paul A. Steckler wrote:
>>>>>>>>>>>>
>>>>>>>>>>>> I've already mentioned the issue described below to Clément
>>>>>>>>>>>> Pit-Claudel
>>>>>>>>>>>> and Pierre Courtieu, maybe others on this list have thoughts on
>>>>>>>>>>>> it.
>>>>>>>>>>>>
>>>>>>>>>>>> Proof General is welded to a model of receiving prompts from a
>>>>>>>>>>>> prover.
>>>>>>>>>>>> After it's received a prompt, PG can send something back to the
>>>>>>>>>>>> prover.
>>>>>>>>>>>>
>>>>>>>>>>>> The ideslave (politically incorrectly-named) mode in Coq,
>>>>>>>>>>>> developed
>>>>>>>>>>>> for CoqIDE abandons that model. In that mode, Coq just waits for
>>>>>>>>>>>> XML
>>>>>>>>>>>> from an IDE, without first offering a prompt.
>>>>>>>>>>>>
>>>>>>>>>>>> In ideslave mode, it seems that Coq sends back responses wrapped
>>>>>>>>>>>> in
>>>>>>>>>>>> <value> tags, so you can use that as a pseudo-prompt. Hmm, I
>>>>>>>>>>>> think the
>>>>>>>>>>>> prompt regexp would have to look for both the closing tag, and
>>>>>>>>>>>> the
>>>>>>>>>>>> single-tag version, <value ... />.
>>>>>>>>>>>>
>>>>>>>>>>>> Even with that, there's still a bootstrapping issue, because
>>>>>>>>>>>> there's
>>>>>>>>>>>> no prompt to s start with. I could probably modify PG to not
>>>>>>>>>>>> look for
>>>>>>>>>>>> that first prompt.
>>>>>>>>>>>>
>>>>>>>>>>>> Is there some good way to handle this?
>>>>>>>>>>>>
>>>>>>>>>>>> -- 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
>>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>> _______________________________________________
>>>>>>>>>> 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
>>>>
>>>> _______________________________________________
>>>> ProofGeneral-devel mailing list
>>>> ProofGeneral-devel@inf.ed.ac.uk
>>>> http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
>>>>
>>>
>>> --
>>> The University of Edinburgh is a charitable body, registered in
>>> Scotland, with registration number SC005336.
>>>
>>> _______________________________________________
>>> ProofGeneral-devel mailing list
>>> ProofGeneral-devel@inf.ed.ac.uk
>>> http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
>>
>>
>
> --
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
>
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to