[isabelle-dev] Proposing extensions to the Isabelle library?
makarius at sketis.net
Tue Jul 2 14:26:25 CEST 2013
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
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.
More information about the isabelle-dev