Re: [isabelle-dev] Isabelle repository broken

2016-05-24 Thread Manuel Eberl
Argh! You are correct. Today is /not/ my day. I'm on it. On 24/05/16 18:42, Makarius wrote: On 24/05/16 18:34, Manuel Eberl wrote: I'm confident that I'll have everyting up and running again soon. BTW, current Isabelle/8230358fab88 now looks like too much has been committed.

Re: [isabelle-dev] Isabelle repository broken

2016-05-24 Thread Makarius
On 24/05/16 18:34, Manuel Eberl wrote: > I'm confident that I'll have everyting up and running again soon. BTW, current Isabelle/8230358fab88 now looks like too much has been committed. Makarius ___ isabelle-dev mailing list

Re: [isabelle-dev] Isabelle repository broken

2016-05-24 Thread Manuel Eberl
Yes, this was my fault. The problem was that I stupidly forgot to commit my changes before I pushed to the testboard and thus did not see the problems caused by my changes. I'm confident that I'll have everyting up and running again soon. Manuel On 24/05/16 17:22, Jasmin Blanchette wrote:

Re: [isabelle-dev] Isabelle repository broken

2016-05-24 Thread Jasmin Blanchette
On 24.05.2016, at 17:12, Makarius 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 > ***

Re: [isabelle-dev] Isabelle repository broken

2016-05-24 Thread Lars Hupel
> https://ci.isabelle.systems/jenkins shows many dark clouds and > thunderbolts, but I have no clue where to look precisely. Jenkins is a complex piece of software (much more complex than Isabelle), so it is indeed hard to figure out where to click. The best way to stay on top of the current

Re: [isabelle-dev] Isabelle repository broken

2016-05-24 Thread 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 wrote: > > The Isabelle repository is broken at 76cb6c6bd7b8 (paulson) or > 6a17bcddd6c2 (eberlm). > > The failure is

[isabelle-dev] Isabelle repository broken

2016-05-24 Thread Makarius
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: ***

Re: [isabelle-dev] Isabelle repository broken

2015-04-22 Thread Makarius
On Mon, 13 Apr 2015, Johannes Hölzl wrote: BTW, can the predicate_compiler setup s.t. typedefs are ignored automatically? Is there anybody who understands that aspect of the predicate compiler? Makarius ___ isabelle-dev mailing list

[isabelle-dev] Isabelle repository broken

2015-04-13 Thread Makarius
In current 7ff7fdfbb9a0 there is this breakdown: HOL-Quickcheck_Examples FAILED *** No specification for Abs_filter *** At command quickcheck (line 150 of ~~/src/HOL/Quickcheck_Examples/Hotel_Example.thy) *** No specification for Abs_filter *** At command quickcheck (line 145 of

Re: [isabelle-dev] Isabelle repository broken

2015-04-13 Thread Johannes Hölzl
Sorry this was my fault. isabelle build -a does not guarantee that the current changes are actually committed... BTW, can the predicate_compiler setup s.t. typedefs are ignored automatically? - Johannes Am Montag, den 13.04.2015, 11:28 +0200 schrieb Makarius: In current 7ff7fdfbb9a0 there