[isabelle-dev] Testing AFP at TUM [was: Isabelle cs. 70300f1b6835]

Makarius makarius at sketis.net
Mon Oct 22 10:39:39 CEST 2012


On Mon, 22 Oct 2012, Gerwin Klein wrote:

>
> On 22/10/2012, at 1:46 AM, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:
>
>>> Yes, I know. I already fixed Collections on Friday and I am going to go
>>> back to this problem on Monday.
>>
>> Btw. whenever I'm testing the AFP these days without relying on the
>> testboard I use the following on one of the lxbroy2…4 machines
>>
>> ISABELLE_FULL_TEST= isabelle afp_build -A -- -o browser_info -o
>> document=pdf -o document_graph -j 2
>
> You shouldn't need most of these options: afp_build already provides all but -j 2

In general "-o document_graph" does not make much sense on the command 
line: it is part of the "configuration" of a session, i.e. hardwired into 
its ROOT specification.

I have already realized in several other situations that the "scope" of 
options is not always clear, and not formalized in any way.


 	Makarius


More information about the isabelle-dev mailing list