[isabelle-dev] Global build failures of the AFP in the testboard

[Makarius]

On Thu, 25 Apr 2013, Dmitriy Traytel wrote:

> Hi all,
>
> since "Containers" are in the AFP mira results in global crashes of the build 
> tool 
> (http://isabelle.in.tum.de/testboard/Isabelle/report/2cef0644d3d7416f8d7cea92e24fd694). 
> By global I mean that no session is built at all due to an outdated (wrt 
> Isabelle repository, e.g. 916271d52466) import of 
> "src/HOL/Library/Efficient_Nat.thy" in the session "Containers-Benchmarks".

That looks like a normal error reported correctly -- missing file while 
examining session AFP/Containers-Benchmarks -- no crash here.

After failing in this static phase of examining the session 
specifications, there is no attempt to continue with what is left over. 
That would be a bit more complex to do, and such extra complexity then 
leads to more potential for really bad breakdowns.


What is still unclear to me after so many years of testboard is how it 
actually used in practice.  I just do "isabelle build -j4 -a -d '$AFP'" to 
see immediately how everything works out.  It is also possible to make a 
quick integrity check via "isabelle build -n -a -d '$AFP'".


 	Makarius