Dear Isabelle developers, I've been keeping an eye on our Jenkins tests and we're almost stable. That is, most build go through without problems or fail because there are broken proofs. However, there's still the occasional unexplained "total failure of existence". The latest instance:
Running HOL-Codegenerator_Test ... HOL-Codegenerator_Test: theory Cmp HOL-Codegenerator_Test: theory Primes HOL-Codegenerator_Test: theory Less_False HOL-Codegenerator_Test: theory Records HOL-Codegenerator_Test: theory Sorted_Less HOL-Codegenerator_Test: theory AList_Upd_Del HOL-Codegenerator_Test: theory Eratosthenes HOL-Codegenerator_Test: theory List_Ins_Del HOL-Codegenerator_Test: theory Map_by_Ordered HOL-Codegenerator_Test: theory Set_by_Ordered HOL-Codegenerator_Test: theory Tree_Set HOL-Codegenerator_Test: theory Tree_Map HOL-Codegenerator_Test: theory Candidates HOL-Codegenerator_Test: theory Generate HOL-Codegenerator_Test: theory Generate_Binary_Nat HOL-Codegenerator_Test: theory Generate_Efficient_Datastructures HOL-Codegenerator_Test: theory Generate_Pretty_Char HOL-Codegenerator_Test: theory Generate_Target_Nat sh: xmalloc: .././shell.c:1620: cannot allocate 3 bytes (0 bytes allocated) poly: scanaddrs.cpp:338: void ScanAddress::ScanRuntimeWord(PolyWord*): Assertion `w->IsDataPtr()' failed. HOL-Codegenerator_Test FAILED The same session also throws aother error in another build: *** Code check failed for SML: "$ISABELLE_TOOL" process -e 'datatype ref = datatype Unsynchronized.ref' -f 'ROOT.ML' -l Pure *** At command "export_code" (line 83 of "~~/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy") Debugging the latter error is much harder because it doesn't tell us anything about the precise error from the ML system. I've checked the full log file and there's nothing relevant before the error. Isn't this supposed to capture stderr in the log output as well? Also, the exit code would be useful. Cheers Lars _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev