[isabelle-dev] AFP broken

Makarius makarius at sketis.net
Tue Feb 18 13:50:36 CET 2014

This refers to Isabelle/892a425c5eaa and AFP/d2082ef48089:

No such file: "/Users/makarius/isabelle/afp-devel/thys/Random_Graph_Subgraph_Threshold/Big_Operators.thy"
The error(s) above occurred for theory "Big_Operators" (required by "Subgraph_Threshold" via "Ugraph_Properties" via "Ugraph_Lemmas") (file "/Users/makarius/isabelle/afp-devel/thys/Random_Graph_Subgraph_Threshold/Ugraph_Lemmas.thy")
The error(s) above occurred in session "Random_Graph_Subgraph_Threshold" (file "$AFP/Random_Graph_Subgraph_Threshold/ROOT")
0:00:27 elapsed time, 0:00:31 cpu time, factor 1.14

So it is not just a failed test run, but a static failure of the source 
dependencies.  At least it shows that various rounds of refinement of 
these error messages have now converged to something useful.

These days I am heating my office with CPU power as follows:

   isabelle build -j4 -a -d '$AFP'

This gives both a warm feeling and saves a lot of time to guess what went 
utterly wrong elsewhere.  The full run takes about 1h.


More information about the isabelle-dev mailing list