Excerpts from Makarius's message of Sat Apr 07 08:43:57 -0400 2012:
> Cutting out the middleman is a good start.  The lib-ified approach sounds 
> more like running everything in a single OCaml process, though.  The Coq 
> guys used to have that for CoqIde, but discontinued it for the forthcoming 
> Coq 8.4.  There are now two OCaml progresses to interact with Coq, 
> front-end and back-end.  There are some rudiments of a protocol for the 
> communication, e.g. see the vicinity of 
> https://github.com/coq/coq/blob/v8.4/toplevel/ide_intf.ml

I'm curious why they discontinued it; is it because lack of multithreaded
support in OCaml meant it was difficult to keep the interface responsive
while Coq was thinking hard about a calculation?

> Concerning the problem of finite time, it is a matter to convince the 
> right people to support the right concepts in the prover itself, such that 
> it becomes easy to connect sophisticated front-end applications.  My 
> XML/YXML encoding is just for raw data exchange, using algebraic datatypes 
> rather painlessly between inhomogenous processes.  On top of that some 
> more is required, like a document-oriented editing model for proof texts.

I took a look at the YXML encoding for Isabelle, and I was surprised by
how simple the ADT was.  To compare, here is Coq's base term type;
and it doesn't include all of the extra types referred to from it:

    type ('constr, 'types) kind_of_term =
      | Rel       of int
      | Var       of identifier
      | Meta      of metavariable
      | Evar      of 'constr pexistential
      | Sort      of sorts
      | Cast      of 'constr * cast_kind * 'types
      | Prod      of name * 'types * 'types
      | Lambda    of name * 'types * 'constr
      | LetIn     of name * 'constr * 'types * 'constr
      | App       of 'constr * 'constr array
      | Const     of constant
      | Ind       of inductive
      | Construct of constructor
      | Case      of case_info * 'constr * 'constr * 'constr array
      | Fix       of ('constr, 'types) pfixpoint
      | CoFix     of ('constr, 'types) pcofixpoint

> I am still in the process of discussing it with some Coq guys what could 
> be done here, to join the movement forwards, leaving odd TTY commands and 
> naive XML exchange behind.

One of the appeals of PGIP is that it doesn't ask very much on the part of
the theorem prover.  Just add some tags to your extant proof format; if you
dropped the tags, the text should look just like it did before.  I don't
have a good sense for what an all encompassing Isabelle/JEdit protocol
looks like (what about tactics? communication of proof state?), but it seems to 
much more radical restructuring on the parts of the proof assistant.  "Ceci
n'est pas une développeur Coq".

ProofGeneral-devel mailing list

Reply via email to