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