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

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

Uh, it's a bit of an unholy soup of all the languages (right now we're doing Haskell and Urweb, but I'm very happy to drop/add languages as necessary).

I know this problem of language diversity. In 2006/2007 I've spent a lot of time to investigate the situation, after having left Emacs Lisp mentally behind. This resulted in the bipedal approach of Isabelle/ML and Isabelle/Scala. In particular, everything outside the prover is standardized towards the JVM platform, and my own implementations use Scala exclusively -- Java merely happens to be the implementation language of some existing jar stuff being used.

Scala can be used in many ways, and I successfully imitate the traditional ML style, with a little bit of add-ons of the richer Scala type-system. Some people use Scala like Java, some others like Haskell (e.g. the scalaz community).

The JVM is "bad", but much less than most other frameworks out there. Moreover it is not a toy -- rich client applications and web applications can be built more or less routinely on the JVM. The JVM also supports concurrent and parallel programming in a robust way, and Scala provides more and more high-level abstractions for it.

Compared to single-threaded untyped Emacs Lisp, this is all a big improvement. (The advantages don't come for free, because other built-in problems of the JVM need to be addressed, such as very odd ideas of "platform-independence".)

Actually, in this case I would have wanted to cut out the middleman, lib-ified Coq and just run 'open Coq' and directly do this (this may be worth doing anyway, independent of this conversation, although I don't have infinite time).

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

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


ProofGeneral-devel mailing list

Reply via email to