On Mon, Mar 26, 2012 at 7:23 PM, Makarius <makar...@sketis.net> wrote: > On Mon, 26 Mar 2012, Lukas Bulwahn wrote: > >> This problem is reproducible on our testboard servers. At the moment, all >> tests of changesets after 2a1953f0d20d have to be manually aborted because >> of that reason. I hope you find a solution quickly, otherwise we should >> deactivate the Proofs-Lambda theory to keep a stable testing environment. > > > OK, I have disabled HOL-Proofs-Lambda for the moment (cf. 500a5d97511a).
This is now fixed in a3a64240cd98, and I have re-enabled HOL-Proofs-Lambda. The problem was the code equation for function "nat" configured in Library/Code_Integer.thy which, in conjunction with Int.nat_numeral [code_abbrev], produced code that looped indefinitely. - Brian _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
