On Fri, 6 Apr 2012, Edward Z. Yang wrote:

I'm actually building a domain-specific frontend for Coq, and I didn't feel like reimplementing all of ProofGeneral's parsing hacks! It's not much: it's going to be a pedagogical theorem prover for first order logic, but the idea is to closely support different deduction styles (e.g. natural deduction, sequent calculus, etc.)

The "parsing hacks" are hacks as long as there is an attempt to define that in a generic protocol. For example, Isabelle/Scala now lets the prover do that reliably (either in ML or Scala). I have recently discussed with some Coq insiders how to do the same specifically for Coq, using existing Vernacular or CoqIde functionality.

Anyway, what is your front-end technology (also the programming language platform for that)? Why are you using PGIP anyway?

Consider this tiny library to exchange algebraic datatypes between different processes in a reasonably portable way:

This is for OCaml and SML, in Isabelle/Scala there is a Scala version already. The claim is that it can be ported to any reasonable programming language in about 1 day (probably not Java).

ProofGeneral-devel mailing list

Reply via email to