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.
Makarius
_______________________________________________
ProofGeneral-devel mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
