Re: [PG-devel] An update on porting PG to Coq 8.5's new APIs

[Alan Schmitt]

On 2016-06-16 15:44, "Paul A. Steckler"  writes:

> I'm the one who'll be doing the programming on this project.
>
> As a long-time consumer of OCaml Weekly News, I'm happy to reciprocate
> by exposing what APIs are needed. :-)
>
> The coqtop XML API concludes each response with a  tag. We can
> probably offer something to indicate when that's happened.

It sounds perfect, thanks a lot.

Alan

-- 
OpenPGP Key ID : 040D0A3B4ED2E5C7
Monthly Athmospheric CO₂, Mauna Loa Obs. 2015-05: 403.94, 2016-05: 407.70


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

Re: [PG-devel] An update on porting PG to Coq 8.5's new APIs

[Clément Pit--Claudel]

Hi Alan,

We're hoping to get a pretty flexible codebase in the end, but more details on 
your use case would be useful :) What are the main difficulties that you ran 
into with the current codebase ?

Clément.

On 2016-06-16 03:27, Alan Schmitt wrote:
> Hello Clément,
> 
> Will this rewrite be monolithic, or will it be possible to use it to
> interact with Coq through elisp? I'm particularly interested in
> improving org-babel support for Coq (which works but is not very
> robust).
> 
> Thanks,
> 
> Alan
> 



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] An update on porting PG to Coq 8.5's new APIs

[Makarius]

On 16/06/16 00:07, Clément Pit--Claudel wrote:
> On 2016-06-15 17:51, Makarius wrote:
>> Concerning the "new" prover APIs of Coq and Isabelle in general: I was
>> in contact with Enrico Tassi when he introduced this for Coq -- it was
>> part of our Paral-ITP project at that time. My general impression is
>> that the new Coq API is more conservative than the PIDE protocol of
>> Isabelle: PIDE is quite demanding on the other side to process a lot of
>> information in real-time.
> 
> Not sure whether this is what you had in mind, but there does exist a PIDE 
> implementation built on top of the new Coq API 
> (https://bitbucket.org/coqpide/pidetop). It's used by at least one Coq IDE 
> (Coqoon ­— it's pretty cool, btw).

Yes, that is by Carst Tankink -- I was working with him over 6 months,
before I left France. Later the Coqoon guys also joined the move,
because I encouraged them to do that, but it never became first-class
for Coq.

You see, I am somehow behind many of the prover IDE modernization
projects, but not all of them.

Ultimately, what counts is what really works, and what is really maintained.


Makarius




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] An update on porting PG to Coq 8.5's new APIs

[Clément Pit--Claudel]

On 2016-06-15 17:51, Makarius wrote:
> Concerning the "new" prover APIs of Coq and Isabelle in general: I was
> in contact with Enrico Tassi when he introduced this for Coq -- it was
> part of our Paral-ITP project at that time. My general impression is
> that the new Coq API is more conservative than the PIDE protocol of
> Isabelle: PIDE is quite demanding on the other side to process a lot of
> information in real-time.

Not sure whether this is what you had in mind, but there does exist a PIDE 
implementation built on top of the new Coq API 
(https://bitbucket.org/coqpide/pidetop). It's used by at least one Coq IDE 
(Coqoon ­— it's pretty cool, btw).



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] An update on porting PG to Coq 8.5's new APIs

[Clément Pit--Claudel]

On 2016-06-15 17:41, Stefan Monnier wrote:
>> There might be a tiny minority of Isabelle users who did not follow new
>> releases in the last 2 years and are still using Isabelle2014 with Proof
>> General.  I don't see a problem with that: they just won't be able to
>> upgrade Proof General and remain stable on both.
> 
> In an ideal world, the new PG Coq code should make it easier to support
> the "new" Isabelle API.  It would be good for someone somewhat familiar
> with the "new" Isabelle API to keep an eye on the new PG Coq code (or for
> those working on the new PG Coq code to take a look at the "new"
> Isabelle API).

Thanks Stefan :) 

I share that hope; I think the new code will be a good basis for such a 
development. I've looked at a few other protocols over the last year, including 
the Isabelle protocol/PIDE, Dafny's and F*'s protocols, and some of the stuff 
that David wrote about PGIP; extending the new code to support these things 
should be much easier than it would have been previously.

Cheers,
Clément.



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] An update on porting PG to Coq 8.5's new APIs

[Makarius]

On 15/06/16 23:41, Stefan Monnier wrote:
>> There might be a tiny minority of Isabelle users who did not follow new
>> releases in the last 2 years and are still using Isabelle2014 with Proof
>> General.  I don't see a problem with that: they just won't be able to
>> upgrade Proof General and remain stable on both.
> 
> In an ideal world, the new PG Coq code should make it easier to support
> the "new" Isabelle API.  It would be good for someone somewhat familiar
> with the "new" Isabelle API to keep an eye on the new PG Coq code (or for
> those working on the new PG Coq code to take a look at the "new"
> Isabelle API).

I have tried to activate people still interested in Emacs over many
years, in order to take a look what is going on in Isabelle/PIDE. I
don't think anybody will suddenly show up, although one could give such
a hypothetical person a last chance by posting on isabelle-users.


Concerning the "new" prover APIs of Coq and Isabelle in general: I was
in contact with Enrico Tassi when he introduced this for Coq -- it was
part of our Paral-ITP project at that time. My general impression is
that the new Coq API is more conservative than the PIDE protocol of
Isabelle: PIDE is quite demanding on the other side to process a lot of
information in real-time.

This is actually the deeper reason, why I gave up the single-threaded
LISP machine of Emacs in 2007 and moved towards the multi-threaded JVM,
even though the JVM is a bit ugly.

BTW, I complained about the "master / slave" terminology of the new Coq
protocol when Enrico introduced that in 2012/2013, not for P.C. reasons
but for technological ones. In PIDE, the front-end and back-end are
peers that continuously exchange a lot of information in both directions.


Makarius

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

Re: [PG-devel] An update on porting PG to Coq 8.5's new APIs

[Clément Pit--Claudel]

On 2016-06-15 17:31, Makarius wrote:
> One could formally ask on the isabelle-users mailing list, if anybody
> wants to join pg-devel for further discussion, although I wouldn't
> expect much from it.

Thanks! Feel free to post such an email there, but I wouldn't press much for 
it: I share you analysis that staying with the current release is a good option 
for these people.



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] An update on porting PG to Coq 8.5's new APIs

[Stefan Monnier]

>> 2. Refactor PG to delimit new interfaces, and somehow support both the old
>> REPL mode and the new async mode.
>> 3. Refactor PG to use the new async mode, dropping the REPL and support for
>> old proof assistants on the way.

Actually, I think the best way to do 2 is to first do 3 and then see how
to merge the new and the old.

> There might be a tiny minority of Isabelle users who did not follow new
> releases in the last 2 years and are still using Isabelle2014 with Proof
> General.  I don't see a problem with that: they just won't be able to
> upgrade Proof General and remain stable on both.

In an ideal world, the new PG Coq code should make it easier to support
the "new" Isabelle API.  It would be good for someone somewhat familiar
with the "new" Isabelle API to keep an eye on the new PG Coq code (or for
those working on the new PG Coq code to take a look at the "new"
Isabelle API).


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

Re: [PG-devel] An update on porting PG to Coq 8.5's new APIs

[Makarius]

On 15/06/16 23:17, Clément Pit--Claudel wrote:

> It would be useful to hear from current users of PG for proof assistants 
> other than Coq, to see if we could think of a transition plan for them (in 
> particular, if there exists a newer, asynchronous protocol for that proof 
> assistant, it would be good to hear more about it with the hope of supporting 
> is as well once the Coq port is completed).  It would also be useful to hear 
> from users of less-commonly-used features of PG, so that we can make sure 
> that they remain compatible.

There might be a tiny minority of Isabelle users who did not follow new
releases in the last 2 years and are still using Isabelle2014 with Proof
General. I don't see a problem with that: they just won't be able to
upgrade Proof General and remain stable on both.

One could formally ask on the isabelle-users mailing list, if anybody
wants to join pg-devel for further discussion, although I wouldn't
expect much from it.


Makarius




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

[PG-devel] An update on porting PG to Coq 8.5's new APIs

[Clément Pit--Claudel]

Hey PG-devel,

Paul is starting to work on porting PG to support new features introduced in 
Coq 8.5 (in particular a new async API). You can see a demo of the new API in 
action at https://asciinema.org/a/b84ph360841x3c9lwq6pyihm9 (note in particular 
how the last proof completes before the other ones are processed; note also 
that this isn't PG, just a prototype that I made hosted at 
https://github.com/cpitclaudel/elcoq/).

We had long on and off-list discussions on how to best do this, wondering how 
much of the existing proof-shell code could be reused and shared. The answer 
was "not much", mostly because Coq's new async protocol isn't compatible with 
the one-prompt-one-response model that PG relies on. Based on this, there were 
essentially three ways to go:

1. Abandon the current Proof General, and start a new Emacs mode entirely, 
gradually merging-in bits and pieces of Proof General (indentation code, syntax 
highlighting, etc).

2. Refactor PG to delimit new interfaces, and somehow support both the old REPL 
mode and the new async mode.

3. Refactor PG to use the new async mode, dropping the REPL and support for old 
proof assistants on the way.

I personally don't like option 1 at all.

Option 2 was considered and partly attempted, but it does turn out to be very 
costly to implement cleanly, and it adds to the complexity without bringing 
much: support for most other provers is partly broken, and the refactoring 
would not fix them.

Option 3 is relatively easy and lets us return quickly to fully supporting Coq 
in PG, thereby hopefully allowing PG to remain the editor of choice for Coq. 
Unfortunately, it also means that the next release of Proof General will not be 
backwards compatible.  We'll mitigate this by tagging a last-good version 
before removing the REPL-management code, and editing the README to clarify how 
to use that version.

For these reasons, we settled on option 3.  It would be useful to hear from 
current users of PG for proof assistants other than Coq, to see if we could 
think of a transition plan for them (in particular, if there exists a newer, 
asynchronous protocol for that proof assistant, it would be good to hear more 
about it with the hope of supporting is as well once the Coq port is 
completed).  It would also be useful to hear from users of less-commonly-used 
features of PG, so that we can make sure that they remain compatible. Proof 
Tree is one; what are the others?

Cheers,
Clément.




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