How to generate html version of Isabelle theory

Question

I have an Isabelle theory file, called John.thy. I would like to show it to my friend, but my friend doesn't have Isabelle, and the raw .thy files aren't very easy to read. I have seen some web-pages in the Isabelle library (like this one: http://isabelle.in.tum.de/library/HOL/Finite_Set.html) that have pretty syntax highlighting, and I would like my theory to look like that.

So how can I make John.html? I have looked at the documentation and it all looks rather scary and difficult, what with all the build files and make files and the like. Could some kind soul explain the simplest way to do this?

maybe you could also change the capitalization to John.thy and John.html in your post (to make the convention apparent for future readers). Then I could drop my comment about it from my answer. — chris

chris chris · Accepted Answer · 2013-07-25T00:47:33

First the answer to your question (see also the Isabelle System Manual, Section 3.2 - System build options):

To generate HTML for your John.thy, create a file named ROOT, in the same directory as John.thy, with the following contents

session John = "HOL" +
  theories
    John

and then, staying in that same directory, invoke

isabelle build -d . -o browser_info -v John

where

-d . specifies that the current directory should be searched for sessions (which are specified in a ROOT file)
-o browser_info is the essential flag to generate HTML (a.k.a. browser info), and
-v (the verbose flag) is useful to see in which directory the result is put

The above invocation will output something similar to

Started at Thu Jul 25 09:38:20 JST 2013 [...]
[...]
Session Pure
Session HOL (main)
Session John
Running John ...
John: theory John
[...]
Browser info at /home/username/.isabelle/Isabelle2013/browser_info/HOL/John
[...]

(where [...] indicates omitted output). So here you see which directory you have to consult to obtain the HTML files.

Having said this, for at least the following reasons I personally prefer PDF over HTML:

with -o browser_info you get a bunch of files in a directory (instead of just a single self-contained file when using -o document=pdf)
not all Isabelle symbols are nicely rendered in HTML (whereas you have full control over symbols when generating PDFs)

Note: If you're using the Isabelle application for Mac OS, you may need to replace isabelle above with /Applications/Isabelle2013.app/Isabelle/bin/isabelle or add /Applications/Isabelle2013.app/Isabelle/bin/ to your PATH.

How to generate html version of Isabelle theory

1 Answers