[isabelle-dev] AODV

[Makarius]

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.

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.


 	Makarius

----------------------------------------------------------------------------
                   http://stop-ttip.org  1,122,322 people so far
----------------------------------------------------------------------------