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".
For now I commented the "Containers-Benchmarks" session out (AFP/
99c45df7f5af) - now the test will reveal further outdated constructs in
"Containers" (mostly related to Florian's reform of the code generation
for numerals).
The question remains, whether it is possible for the build tool to
proceed with other sessions if the imports of a single session are faulty.
Dmitriy
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
