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
demand
much more radical restructuring on the parts of the proof assistant. "Ceci
n'est pas une développeur Coq".
Cheers,
Edward
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
