OK, you'll need to explain the binding between plug-ins and PG to me.

-- Paul

On Sat, May 7, 2016 at 3:38 PM, Clément Pit--Claudel
<clement....@gmail.com> wrote:
> Additionally, it would be nice to remain compatible with plugins :)
>
> On 2016-05-07 09:33, Clément Pit--Claudel wrote:
>> Hi Paul,
>>
>> I don't think we should give it a different name yet; I think it would 
>> create a lot of confusion.
>>
>> We can phrase this differently: what you are currently writing is a library 
>> that implements the protocol spoken by Coq. Ideally, we would be able to 
>> plug that library straight into proof general. Unfortunately, that isn't the 
>> case today. So, we'll have to modify PG. That's fine :)
>>
>> One particular strong point of proof general is its ability to talk to 
>> multiple versions of Coq. A full fork would be problematic, because it would 
>> loose this ability.
>>
>> Regarding the other part (coqserver), I think a coqdev thread would be more 
>> appropriate.
>>
>> Clément.
>>
>> On 2016-05-07 02:48, Paul A. Steckler wrote:
>>> 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
>>>
>>
>>
>>
>> _______________________________________________
>> 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

Reply via email to