Re: [PG-devel] PG and Coq ideslave mode

[David Aspinall]

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

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

Re: [PG-devel] PG and Coq ideslave mode

[Clément Pit--Claudel]

On 2016-05-06 09:34, Paul A. Steckler wrote:
> 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.

That's correct.



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] PG and Coq ideslave mode

[Paul A. Steckler]

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

Re: [PG-devel] PG and Coq ideslave mode

[David Aspinall]

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  
> 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 :
>>> 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
  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
>>  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
>  tags, so you can use that as 

Re: [PG-devel] PG and Coq ideslave mode

[Paul A. Steckler]

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

 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
 

[PG-devel] Last Call for Papers: Workshop on User Interfaces for Theorem Provers (UITP 2016 @ IJCAR), Coimbra, Portugal, Deadline May 17th *NEW* (was May 9th, 2016)

[David Aspinall]

Subject: [Stp] Last Call for Papers: Workshop on User Interfaces for
Theorem Provers (UITP 2016 @ IJCAR), Coimbra, Portugal, Deadline May
17th *NEW* (was May 9th, 2016)
Date: Fri, 6 May 2016 06:40:13 +
From: Grov, Gudmund 
To: s...@macs.hw.ac.uk , d...@macs.hw.ac.uk


 Last Call for Papers

  UITP 2016
  12th International Workshop on User Interfaces for Theorem Provers
in connection with IJCAR 2016
  July 2nd, 2016, Coimbra, Portugal
  http://www.informatik.uni-bremen.de/uitp/current/
* NEW Submission deadline: May 17th, 2016 *

--
NEWS:
- Invited Speaker: Sylvain Conchon (LRI, France) giving a talk about
  "AltGr-Ergo, a graphical user interface for the SMT solver Alt-Ergo"
- Submission deadline postponed by one week to May, 17th, 2016
--

The  User  Interfaces  for  Theorem  Provers  workshop  series  brings
together   researchers  interested   in   designing,  developing   and
evaluating interfaces  for interactive proof systems,  such as theorem
provers,  formal  method  tools,  and  other  tools  manipulating  and
presenting mathematical formulas.

While  the reasoning  capabilities of  interactive proof  systems have
increased dramatically over the last years, the system interfaces have
often  not   enjoyed  the   same  attention   as  the   proof  engines
themselves.  In many  cases,  interfaces remain  relatively basic  and
under-designed.

The User  Interfaces for  Theorem Provers  workshop series  provides a
forum for  researchers interested in improving  human interaction with
proof  systems. We  welcome participation  and contributions  from the
theorem proving, formal  methods and tools, and  HCI communities, both
to  report on  experience with  existing systems,  and to  discuss new
directions. Topics covered include, but are not limited to:

- Application-specific  interaction mechanisms  or designs  for prover
  interfaces Experiments and evaluation of prover interfaces
- Languages and tools for authoring, exchanging and presenting proof
- Implementation  techniques (e.g.  web  services, custom  middleware,
  DSLs)
- Integration of interfaces and tools to explore and construct proof
- Representation and manipulation of mathematical knowledge or objects
- Visualisation of mathematical objects and proof
- System descriptions

UITP 2016 is a one-day workshop to be held on Saturday, July 2nd, 2016
in Coimbra, Portugal, as a IJCAR 2016 workshop.

** Submissions **

Submitted   papers  should   describe   previously  unpublished   work
(completed or  in progress), and  be at least 4  pages and at  most 12
pages. We encourage concise and relevant papers. Submissions should be
in PDF format, and typeset with  the EPTCS LaTeX document class (which
can be downloaded from  http://style.eptcs.org/). Submission should be
done via EasyChair at
https://www.easychair.org/conferences/?conf=uitp16

All papers will be peer reviewed by members of the programme committee
and selected by the organizers in accordance with the referee
reports.

At  least one  author/presenter  of accepted  papers  must attend  the
workshop and present their work.

** Proceedings **

Authors will have the opportunity to incorporate feedback and insights
gathered during the  workshop to improve their  accepted papers before
publication  in the  Electronic  Proceedings  in Theoretical  Computer
Science (EPTCS - http://www.eptcs.org/).

** Important dates **

 Submission deadline: May 17th, 2016
 Acceptance notification: June 6th, 2016
 Camera-ready copy: June 20th, 2016
 Workshop: July 2nd, 2016

** Programme Committee **

 Serge Autexier, DFKI Bremen, Germany (Co-Chair)
 Pedro Quaresma, U Coimbra, Portugal (Co-Chair)
 David Aspinall, University of Edinburgh, Scotland
 Chris Benzmüller, FU Berlin, Germany & Stanford, USA
 Yves Bertot, INRIA Sophia-Antipolis, France
 Gudmund Grov, Heriott-Watt University, Scotland
 Zoltán Kovács, RISC, Austria
 Christoph Lüth, University of Bremen and DFKI Bremen, Germany
 Alexander Lyaletski, Kiev National Taras Shevchenko Univ., Ukraine
 Michael Norrish, NICTA, Australia
 Andrei Paskevich, LRI, France
 Christian Sternagel, University Innsbruck, Austria
 Enrico Tassi, INRIA Sophia-Antipolis, France
 Laurent Théry, INRIA Sophia-Antipolis, France
 Makarius Wenzel, Sketis, Germany
 Wolfgang Windsteiger, RISC Linz, Austria
 Bruno Woltzenlogel Paleo, TU Vienna, Austria


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