IsarMathLib version 1.6.7 released

This release includes the new HTML rendering tool that replaces tiddlyisar (which still compiles and works ). I updated all IsarMathLib theories that were not fully updated for Isabelle 2008 removing legacy keywords like constdefs and prems and added missing comments. As a result all IsarMathLib theories except those translated from Metamath are now presented at the FormalMath.org site.

There is no new formalized mathematics in this release.

Advertisements

Tags: ,

8 Responses to “IsarMathLib version 1.6.7 released”

  1. pdf23ds Says:

    I’m currently working on a nicer HTML output for Metamath that shows the substitutions explicitly. I think it’ll improve readability by an order of magnitude. I hope it becomes official.

    After that, though, I’ll be working on something related to Isar. So I’m wondering–which features of Isar do you really use?

    I’m leaning towards making a graphical interactive prover that translates trivially to an Isar-like language. Well, probably something simpler than Isar. I find Isar hard to follow, personally. Do you find that as you learn it and use it for larger proofs that it becomes nicer to use?

    Ideally I’d have something where you could easily access the level of explicitness in Metamath when reading a proof, while still giving proof writers access to the large steps possible with Isabelle and Isar. This might be possible by simply adding a few extra tools to Isar (or it might already be possible by pretty-printing proof terms) but I’m looking for something really nice.

  2. slawekk Says:

    > which features of Isar do you really use?

    The short answer is that I use a subset of Isar that makes formal proofs as similar to the natural language proofs as I can. If you want to design a new language I think that would be the principle to follow.

    > Do you find that as you learn it and use it for larger proofs that it becomes nicer to use?

    The answer depends on whether we talk about writing proofs or reading proofs. As for writing I would compare the learning curve to Java. It becomes easier after about two months of use. It happens sooner than with Haskell, but not as soon as with Python. Of course you still gain experience after that, but most of the skill is acquired in the first two months.

    As for reading I can’t say as I don’t have experience reading someone else’s Isar proofs, especially ZF proofs written in declarative style. I have always thought that Isar is the easiest to read among all proof languages. Metamath presentations are easy to understand if you focus on one particular step. However, following a proof consisting of hundreds of such elementary steps is close to impossible if you are not the author.

    > I find Isar hard to follow, personally.

    It is always relative to other proof languages. Are other proof languages easier to follow? If so, specifically what makes them better in that respect? That would be interesting to know and of course to design a language that takes the best from the others.

  3. pdf23ds Says:

    On topic for once, a problem I have with the isarmathlib.org as it stands is that the gifs display incrementally as the page loads, and every time a gif is loaded, the page reflows. That’s incredibly distracting. Above that, the javascript seems to want to wait until the page has displayed the text versions of whatever before it tries to show the pngs, and so you see the text version for a second before the javascript executes.

    I don’t know how much you can change the code running there (how familiar you are with it), but if you had complete control I would say it would be better to try to not show anything in the main panel until you show the png equations, and then to set the width and height properties on all image tags so that no reflow is necessary after the image is loaded. I think that would make the initial loading and display much smoother.

    (You may have trouble seeing this on a local copy of the site due to the very low latency, but it’s extremely obvious on the website.)

    I’m doing something along these lines with my display code for Metamath. Check it out here. Of course, it’s much easier in my case since I only display one glyph per image, and no images are generated dynamically, so I always know the size beforehand. (Comments welcome on my presentation, of course.)

  4. slawekk Says:

    The code that displays math on the FormalMath.org site is jsMath. It’s an implementation of TeX layout algorithms in JavaScript. It does not use PNG’s or GIFs (perhaps as fonts?I don’t know much about it). It is a bit slow, but trying to modify it to implement kind of what you suggest is way over my head. It may not even be possible by design. From what I have seen it is about twice as fast on Firefox than IE and having the proper TeX fonts installed also speeds it up a bit. Probably the best I can do is to include some text on the front page explaining what is going on and suggest to use Firefox for viewing.

  5. pdf23ds Says:

    Ahhh, I don’t have those fonts. I guess in the absence of those fonts it uses images instead. Because I’m definitely getting a page full of pngs.

  6. pdf23ds Says:

    Yes, when I download and install fonts from here, all is well. (Though I still see stuff flashing around when it loads.)

    I think the workaround would be pretty simple, though. Simply set the style of your main panel to display:none, and then have the javascript stuff change that back to display:block once it’s done reformatting.

  7. slawekk Says:

    > Simply set the style of your main panel to display:none

    Thanks for the tip, I think this is something I would be able to do. However, this would mean that the user can see nothing until the jsMath processing is done? On longest theories that takes about 15 seconds. I could display something like “please wait for jsMath to finish”, but I am not sure this is better than a brief flash of TeX code.

  8. pdf23ds Says:

    Hmm. It would be more complicated, but perhaps possible to have the display attribute set and unset per lemma, so you see a lemma at a time flashing instead of a glyph at a time.

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: