New versions of Isabelle, I3P and IsarMathLib

A new version of Isabelle was released on June 23rd. This version is called  Isabelle2009-2 which I find bit strange in 2010.The standard installation is simple and includes the ZF logic. To work with IsarMathLib it’s probably a good idea to change the ISABELLE_LOGIC prameter in etc/settings to ZF.

The changes in the new version are related mostly to HOL. There is a small change in naming of some environment variables, so I released IsarMathLib 1.6.10 to make sure the library checks out of the box by typing “isabelle make”. This IsarMathLib version contains no new formalized mathematics.

Isabelle2009-2 contains “the preliminary Isabelle/jEdit application demonstrates the emerging Isabelle/Scala layer for advanced prover interaction and integration”. Here is a screenshot of the editor showing TopologicalGroup_ZF theory.

The new jEdit based Isabelle interface

The display of the Isabelle math symbols is flawless. The subscripts (\<^isub> in source) are not displayed though.

I was unable to use this as an actual interface to Isabelle. When I select “Plugins/Isabelle/Activate current buffer” the colors change somewhat. From the ps output it seems that Isabelle process starts, but there is some kind of failure in lib/scipts/feeder.pl. I couldn’t do anything else. I didn’t try too hard though.

Following the Isabelle release a new version of the I3P interface was relesed as well. There is some improvement in rendering math symbols possibly because of improvement in the Isabelle font. However the display of symbols is still not reliable. Some symbols (like \<tau>) are rendered correctly in some places but not others. Some, like \<langle> and \<rangle> are not displayed at all. This is not a problem with Isabelle fonts as the jEdit based interface displays those symbols correctly. The subscripts are also not rendered as such.

Advertisements

5 Responses to “New versions of Isabelle, I3P and IsarMathLib”

  1. jsalvati Says:

    I’ve recently become interested in formal math. What do you think the best resources/methods are for learning formal math and how higher mathematics are constructed? I have an engineer’s math background + some basic set theory topology and some passing knowledge of first order logic.

  2. slawekk Says:

    learning formal math and how higher mathematics are constructed

    I am of course biased, but I do believie that Isabelle/ZF + IsarMathLib is best for that.
    As for the resources there is not much. Just install Isabelle, download IsarMathLib, look at how proofs are done there and try to do somethig similar. You can ask me questions if you run into problems, prefererably at the IsarMathLib mailing list.

    Alternatively, you can try Metamath. It’s more hardcore, but there is a larger community around it.

  3. John Says:

    Hi,

    The IsarMathLib link appears incorrect; it should be http://nongnu.askapache.com/isarmathlib/isarmathlib-1.6.10.tar.gz.

    Thanks!

  4. slawekk Says:

    Fixed. Thanks.

  5. James Frank Says:

    Another thanks for putting out information that, most likely, not one other person in the whole WWW has put out, at least as a friendly snippet that’s not buried in some manual.

    I was tempted to go with Coq just because they provide a Windows binary that works by magic (plus there’s more books and tutorials for Coq than Isabelle).

    Getting set up for Linux was painful, since I need it to run off of a USB drive.

    But this post was useful because of your comment about the Isabelle distribution missing the ZF logic, and the simple instructions on how to build it.

    Also, pointing me in the direction of i3p helped me out. I hate Emacs, since I never took the time to figure it out, and jEdit runs too slow on this old computer that I sometimes work on.

    It all runs slow, since I’m running Ubuntu under VirtualBox with 1 gigabyte of memory, but I couldn’t use jEdit.

Leave a Reply

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

WordPress.com Logo

You are commenting using your WordPress.com 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: