[isabelle-dev] AFP broken
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