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.
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
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:
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
> ***
> 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
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
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:
***
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
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
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
10 matches
Mail list logo