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

Dmitriy Traytel traytel at in.tum.de
Thu Apr 25 11:39:57 CEST 2013


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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130425/397eb25b/attachment.html>


More information about the isabelle-dev mailing list