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