[isabelle-dev] Isabelle repository broken

[Lawrence Paulson]

I did run a full test of my changes, which in any event don’t look connected with the error message you report.
Larry

> On 24 May 2016, at 16:12, Makarius <makarius at sketis.net> wrote:
> 
> 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
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev