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
----------------------------------------------------------------------------_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
