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

[Alessandro Coglio]

Thank you for the information. I will use the suggested build commands.

It sounds like I should also look into the AFP. Is http://hg.code.sf.net/p/afp/code the correct repo URL? If some changes to the AFP are needed, should I create an hg patch for those as well, which then I'll send along with the patch for the Isabelle repo?



On Jul 2, 2013, at 5:26 AM, Makarius <makarius at sketis.net> wrote:

> 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