[isabelle-dev] Isabelle manuals as regular session documents

Makarius makarius at sketis.net
Thu Aug 30 16:05:20 CEST 2012


On Thu, 30 Aug 2012, Lars Noschinski wrote:

> On 28.08.2012 19:17, Makarius wrote:
>> * The Admin tool "isabelle build_doc" helps to populate the doc/
>> directory on the spot, such that "isabelle doc" finds the results.
>
> One comment from a UI perspective: "isabelle build_doc" seems to do 
> something, then fails with
>
> cp: cannot stat `/tmp/isabelle-lars12015/*.dvi': No such file or directory
> cp: cannot stat `/tmp/isabelle-lars12015/*.pdf': No such file or directory
>
> Took me a while to discover, that I either need to give "-a" or at least 
> one session explicitly.

This is still the old habit to make admin tools a bit rough ...


> Also, an option to list the available sessions would be nice (same holds 
> for "isabelle build")

The regular build mainly works via letter soups, i.e. you combine options 
to have a certain effect.  To get an overview of the whole situation 
without building, I am presently using "isabelle build -nva" or even 
"isabelle build -nval".

There are also some insider jokes built into build, because it has options 
"-b" (really build) and "-n" (no build), so you can emphasize and 
deemphasize things.

Eventually, I hope to see a Scala/Swing wrapper for the tool, so that 
command-line poetry will be replaced by a few persistent buttons, similar 
to the Find dialog in jEdit.


 	Makarius




More information about the isabelle-dev mailing list