[isabelle-dev] Proposing extensions to the Isabelle library?

[Makarius]

On Mon, 1 Jul 2013, Alessandro Coglio wrote:

> I have a patch that works with changeset 52498:d802431fe356. The command
>
> ./bin/isabelle build -a -o browser_info -o document=pdf -o document_graph
>
> succeeds (after applying the patch), even though the output says that 
> some theories are skipped due to what look like some undefined 
> environment variables -- I can send more precise information on this.

See also "Testing of changes (before push)" at the end of the important 
README_REPOSITORY file, e.g. that version 
http://isabelle.in.tum.de/repos/isabelle/file/d802431fe356/README_REPOSITORY#l282 
with its various command line examples.

Note that from a Isabelle user's point of view, option -o document_graph 
does not make much sense.  Sessions that require that say so in the ROOT. 
(This seems to have been copied from some outdated wiki somewhere.)

Option -o browser_info does not add any relevant information to a test run 
-- it can be omitted.  HTML generation is not going to crash unexpectedly.

Option -o document=pdf does provide some information about latex (and 
problems with it independently of Isabelle), but in practice that is much 
less relevant than making a full build at all -- ideally including AFP.


So apart from the information in README_REPOSITORY, this is what I am 
doing myself all the time:

   isabelle build -j4 -a -d '$AFP'

The best value for "-j N" and the implicit ISABELLE_BUILD_OPTIONS 
"threads=M" depends on the underlying hardware.


 	Makarius