[isabelle-dev] Failures in HOL-Codegenerator_Test

[Lars Hupel]

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