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.

Formalmath.org

The new HTML rendering of IsarMathLib is ready.

Creating it was easier than I had expected. The most tricky part of the Isar to HTML translator is the Isar parser, but that was done when creating the TiddlyWiki rendering, and didn’t require any changes. Producing HTML from internal representation was just a simple rewrite of the existing TiddlyWiki markup generator. I had to learn some JavaScript and haXe to implement expanding proofs and reference hints, but not much and it was an interesting experience.The CSS layout was created with an online frameset generator with some minor tweaks.

There is one remaining serious issue that I don’t know how to resolve. Some proofs don’t expand on click. One can see an example of this problem in the proof of lemma func1_1_L12 in the func1 theory. The only subproof there does not change cursor and background color on mouse hover (implemented with CSS) and does not expand on click (haXe and JavaScript). Curiously, TiddlyWiki presentation has a very similar problem, see the proof of prod_list_of_lists in the Semigroup_ZF tiddler. This happens in Firefox 3.0.5 on Ubuntu and IE7 and Firefox on Windows XP. If you have an idea what might be causing this, please let me know.

P.S. This turned out to be a jsMath issue.