[isabelle-dev] Isabelle repository broken

Makarius makarius at sketis.net
Tue May 24 17:12:37 CEST 2016


The Isabelle repository is broken at 76cb6c6bd7b8 (paulson) or
6a17bcddd6c2 (eberlm).

The failure is as follows:
### theory "Generate_Binary_Nat"
### 197.201s elapsed time, 259.420s cpu time, 8.924s GC time
*** "List.coset" is not a constructor, on left hand side of equation, in
theorem:
*** permutations_of_set (List.coset ?xs) \<equiv>
*** Code.abort (STR ''Permutation of set complement not supported'')
***  (\<lambda>_. permutations_of_set (List.coset ?xs))
*** At command "export_code" (line 83 of
"~~/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy")


https://ci.isabelle.systems/jenkins shows many dark clouds and
thunderbolts, but I have no clue where to look precisely.


In principle, such a situation cannot happen: everybody knows that
pushes to the Isabelle repository require a full test that is equivalent
to "isabelle build -a".


	Makarius


More information about the isabelle-dev mailing list