[isabelle] Report from our Isabelle course
(too old to reply)
Lars Hupel
2016-07-20 11:43:54 UTC
* Some suggested that it would be nice to have the documentation
available as a website, and not just PDFs. Websites have the
advantage that they are searchable by Google & co, easily linkable,
and generally more accessible than the somewhat rigid PDF format.
I think this is a worthwhile suggestion and one that might be
doable, at least if the TeX code producing the PDF documentation is
structured well enough to be fed to one of the TeX-to-HTML-
conversion tools.
yes, I also think that'd be great to have. Quite a while ago I tried the
various tools floating around the web but none of them worked well. (Not
sure whether the situation has changed.) I got the impression that it
might be better to produce HTML directly (given that we already have
"browser_info" files).

Jasmin Blanchette
2016-08-01 08:02:20 UTC
In the mean time, authors of Isabelle documentation can update their
sources to Isabelle markdown + antiquotations as much as possible. There
is still relatively much raw LaTeX in manuals that are not in my
The Nitpick and Sledgehammer manuals are of course particular offenders in this area. The Sledgehammer manual is pretty short and should be relatively easy to port. It's on my list, but feel free to bug me again if it doesn't get done in a timely enough fashion.

As for Nitpick, the goal is to replace it with Nunchaku, so it might we better to leave the manual as is and wait until the tool is obsoleted. (Nunchaku will soon be integrated in the development Isabelle, in time for the next release, but it may take 1-2 more release cycles before Nitpick is effectively subsumed.)

As for the Nunchaku manual, I will write it in the modern style.