On Sun, 8 Apr 2012, Edward Z. Yang wrote:

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

You would have compare that to the datatypes for term and proofterm in Isabelle, see src/Pure/term.ML and src/Pure/proofterm.ML, respectively.

XML/YXML alone does not do anything, it merely provides a simple tree format to transport arbitrary ML datatype values. The wrapping for that essentially duplicates the datatype specfification once more on each side of the inter-process communication, but not more.

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.

I've found it very challenging to get a half-decent PGIP implementation in Isabelle. In the historcial attempts at that, there is a famous comment by David Aspinall and Christoph Lüth here (from 2004):


In particular this bit:

   If we had proper parse trees it would be easy, although having a
   fixed type of trees might be tricky with Isar's extensible parser.

Ex falso quodlibet consequitur ... or more appropiately "Lasciate ogne speranza, voi ch'intrate" (Dante passing through the Gates of Hell).

Many discussions over many years later, all problems are basically solved, although the way to do it turned out quite differently than first anticipated in early PGIP drafts. (The main idea is to use YXML again to sneak useful markup into messages produced by the prover.)

ProofGeneral-devel mailing list

Reply via email to