[isabelle-dev] AODV

[Gerwin Klein]

> On Wed, 10 Dec 2014, Tobias Nipkow wrote:
>
>> On 09/12/2014 21:50, Makarius wrote:
>>> On Wed, 10 Dec 2014, Gerwin Klein wrote:
>>> >  “build -a” is still going to miss document preparation errors in the >  AFP,
>>> >  though, so it’s still not really the right command to run for testing >  it.
>>>
>>> We've had that discussion occasionally.  Nowadays I usually do full
>>> "build -a -d '$AFP'" quite aggresively, but rarely -o document=pdf.
>>> It is just a matter to get the most relevant information out of the
>>> test.
>>
>> For the AFP test we don't want to most relevant or most of the information but all of it. It is as simple as that.
>
> That is the batch mode test somewhere in the background.

Both options were batch mode. At least I don’t think Florian was running this in Isabelle/jedit.


> This thread was started by Florian Haftmann, because the canonical manual test became very slow without a good reason, as we have learned now.
>
> In the past years there has been a continuous struggle to keep the Isabelle + AFP build time in check, with an incredible advance of the prover technology around it.  This advantage should not be spoilt by redundant ROOT files, especially since there are 2-3 easy ways to do better.

One of which is not to run “build -a” on the entire world ;-)

In my setup at least I have additional components for other projects I’m working on, so running plain ‘build -a’ rarely makes sense. The story is different when only core Isabelle and AFP are the registered components which would be the case when the main work is on the Isabelle side.

For that scenario, I do see your point. “build -a” is convenient for a somewhat faster test before one pushes to the main repository. The relatively rare document build failures will be caught in the regression test which does run with the right document options.

I’ll have a look at changing the ROOT file, the development mode for the AODV entry is mostly over anyway, so I might just remove the additional sessions.

Cheers,
Gerwin


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.