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