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