Goodbye ProofGeneral

Some recent messages on the Isabelle mailing list bring the information that the Isabelle team is working on a new interface for Isabelle and possibly other provers that will replace Emacs based ProofGeneral. The new interface will be written in Scala. Scala is an multiparadigm language (OO and functional) that runs on JVM. This is an interesting choice of technology that suggests something about the design goals (I am speculating again). Applications writen in Scala can run on any platform that has JVM. In particular, one can write applets in Scala that can be run in a browser. Scala is a general purpose language, but seems to be particularly good for web programming. There are a couple of web programming frameworks written in Scala, Lift being the most popular, competing with Rails. So the new interface will be multiplatform and easy to integrate with web applications (wiki?). Hopefully this will make Isabelle proving environment closer to being network transparent – a user interface, possibly running in a browser and sending formalized text for verification to an Isabelle server located (possibly) on a different host with dependencies scattered all over the internet.

So what about ProofGeneral? It seems that the next generation of PG based on Eclipse is still being actively developed. So soon Isabelle users may have a couple of new interfaces to choose from.

There are two ways of looking at authoring Isabelle theories. For some people this is similar to writing software. For those people the Eclipse interface may be better.

I use Isabelle for formalized mathematics so for me Isabelle is a back-end of a document preparation system. The front end  to such system should have features typical for a word processor rather than programmer’s editor. The features that are most important for me are the ease of setup and WISIWYG support for mathematical notation. Easy search for theorems (not necessarily semantic, just one based on strings in the comments would be good enough) would be nice too.


Tags: , ,

3 Responses to “Goodbye ProofGeneral”

  1. pdf23ds Says:

    So I guess it’d be more accurate to say “goodbye Emacs”. And, as far as I’m concerned, good riddance.

    I’m also going to have another frontend, though it’s not going to be oriented towards the expert user, at least initially. It’ll be oriented towards the student of math. And it’ll be much more Windows friendly. (I think that ProofGeneral doesn’t work with the windows version of Emacs, though it sounds like the Scala-based interface should be more easily portable.)

    I still haven’t decided whether to reimplement Isabelle’s core inference engine or to communicate with an Isabelle process, but I’m slightly leaning towards the former. It’d be good to have another implementation of Isabelle’s core anyways. And it doesn’t sound like too much work, either.

  2. slawekk Says:

    it’ll be much more Windows friendly

    I hope that does not imply “Linux hostile”. There are not much reasons to not to write multiplatform applications nowdays. If not Java then gtk or wxWidgets are more than enough to run the same app on Windows and X Window. And in this case making the whole system a web application and running the front end in the browser also makes sense.

    reimplement Isabelle’s core inference engine

    The need is rather to have an alternative implementation of Isar. This includes the inference engine. I think you mentioned you are a constructivist. Will your system support ZF?

  3. gavenkoa Says:

    Go away bad Emacs! And some sadly.

    Eclipse as word editor look not much more differently as Emacs. But its button so sweet, and do not need know anything internal.

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: