The afp test is now back to normal operation and the devel website update is
working again as well.
The two below are real failures, possibly have been there for a while masked by
the problems the test had.
Cheers,
Gerwin
Begin forwarded message:
> From: isat...@macbroy2.informatik.tu-muenche
On 09/24/2012 09:33 PM, Makarius wrote:
On Fri, 21 Sep 2012, Lukas Bulwahn wrote:
I am just at the moment trying to get it running again.
Lukas
On 09/21/2012 10:54 AM, Jasmin Christian Blanchette wrote:
Am 21.09.2012 um 09:18 schrieb Tobias Nipkow:
The testboard runs most of the AFP.
For
On Fri, 21 Sep 2012, Lukas Bulwahn wrote:
I am just at the moment trying to get it running again.
Lukas
On 09/21/2012 10:54 AM, Jasmin Christian Blanchette wrote:
Am 21.09.2012 um 09:18 schrieb Tobias Nipkow:
The testboard runs most of the AFP.
For the last three days, neither the tests no
On Fri, 21 Sep 2012, Tobias Nipkow wrote:
This is just another reminder that people should watch the AFP when they
check in changes, and fix them. The testboard runs most of the AFP.
Once the testboard recovers, one could make this a bit more complete. I
usually have FLYSPECK_SKIP_PROOFS=tru
On Fri, 21 Sep 2012, Jasmin Christian Blanchette wrote:
Am 21.09.2012 um 09:18 schrieb Tobias Nipkow:
The testboard runs most of the AFP.
For the last three days, neither the tests nor testboard have been working.
http://isabelle.in.tum.de/reports/Isabelle
http://isabelle.in.tum.de/te
I am just at the moment trying to get it running again.
Lukas
On 09/21/2012 10:54 AM, Jasmin Christian Blanchette wrote:
Am 21.09.2012 um 09:18 schrieb Tobias Nipkow:
The testboard runs most of the AFP.
For the last three days, neither the tests nor testboard have been working.
http://
Am 21.09.2012 um 09:18 schrieb Tobias Nipkow:
> The testboard runs most of the AFP.
For the last three days, neither the tests nor testboard have been working.
http://isabelle.in.tum.de/reports/Isabelle
http://isabelle.in.tum.de/testboard/Isabelle
Jasmin
___
That's very kind of him, assuming he was not the one who broke KBPs. This is
just another reminder that people should watch the AFP when they check in
changes, and fix them. The testboard runs most of the AFP.
Tobias
Am 21/09/2012 09:12, schrieb Lukas Bulwahn:
> Thanks to Dmitriy's effort, all AF
Thanks to Dmitriy's effort, all AFP entries run successfully again.
Original Message
Subject:status (AFP)
Date: Fri, 21 Sep 2012 09:10:43 +0200 (CEST)
From: isat...@macbroy2.informatik.tu-muenchen.de (Isabelle )
To: undisclosed-recipients:;
The status of the
I hope changeset 2cdf5c71b818 in the AFP solves the issue.
Lukas
On 03/11/2012 01:02 PM, Brian Huffman wrote:
On Sun, Mar 11, 2012 at 12:09 PM, Tobias Nipkow wrote:
One error in JinjaThreads was fixed, here is the next one:
*** Unknown fact "list_all2_update_cong2" (line 467 of
"/mnt/nfsbroy
On Sun, Mar 11, 2012 at 12:09 PM, Tobias Nipkow wrote:
> One error in JinjaThreads was fixed, here is the next one:
>
> *** Unknown fact "list_all2_update_cong2" (line 467 of
> "/mnt/nfsbroy/home/isatest/afp/devel/thys/JinjaThreads/BV/BVSpecTypeSafe.thy")
> *** At command "apply" (line 467 of
> "/
One error in JinjaThreads was fixed, here is the next one:
*** Unknown fact "list_all2_update_cong2" (line 467 of
"/mnt/nfsbroy/home/isatest/afp/devel/thys/JinjaThreads/BV/BVSpecTypeSafe.thy")
*** At command "apply" (line 467 of
"/mnt/nfsbroy/home/isatest/afp/devel/thys/JinjaThreads/BV/BVSpecTypeS
Since fixing JinjaThreads gets worse as time elapses, pls fix it asap.
It has been broken for a number of days now.
*** Unknown fact "num_AB_s" (line 129 of
"/mnt/nfsbroy/home/isatest/afp/devel/thys/JinjaThreads/Common/BinOp.thy")
Tobias
Original-Nachricht
Betreff: status (AFP)
Hi all,
JinjaThreads currently probably fails because of the changeset
6e422d180de8 (http://isabelle.in.tum.de/repos/isabelle/rev/6e422d180de8)
*** empty result sequence -- proof command failed
*** At command "apply" (line 2941 of
"/home/kleing/afp/devel/thys/JinjaThreads/Compiler/JVMJ1.thy
On 14/10/2011, at 8:02 PM, Makarius wrote:
>> We're investigating if possibly something is wrong with the test server's
>> memory, but it seems unlikely (our L4.verified sessions are larger and
>> stable).
>
> Is this the machine that is producing these test results?
>
> http://isabelle.in.tu
On 14/10/2011, at 9:32 PM, David Matthews wrote:
> On 14/10/2011 10:02, Makarius wrote:
>> On Fri, 14 Oct 2011, Gerwin Klein wrote:
>>
>>> Is anyone else observing intermittent problems like this?
>>>
>>> Building Jinja ...
>>> poly: scanaddrs.cpp:107: PolyWord
>>> ScanAddress::ScanStackAddress
On 14/10/2011 10:02, Makarius wrote:
On Fri, 14 Oct 2011, Gerwin Klein wrote:
Is anyone else observing intermittent problems like this?
Building Jinja ...
poly: scanaddrs.cpp:107: PolyWord
ScanAddress::ScanStackAddress(PolyWord, StackObject*, bool): Assertion
`val.IsDataPtr()' failed.
/home/kl
On Fri, 14 Oct 2011, Gerwin Klein wrote:
Is anyone else observing intermittent problems like this?
Building Jinja ...
poly: scanaddrs.cpp:107: PolyWord ScanAddress::ScanStackAddress(PolyWord,
StackObject*, bool): Assertion `val.IsDataPtr()' failed.
/home/kleing/volatile/isadist/Isabelle_13-Oct
Is anyone else observing intermittent problems like this?
Building Jinja ...
poly: scanaddrs.cpp:107: PolyWord ScanAddress::ScanStackAddress(PolyWord,
StackObject*, bool): Assertion `val.IsDataPtr()' failed.
/home/kleing/volatile/isadist/Isabelle_13-Oct-2011/lib/scripts/run-polyml: line
77: 2009
On 11/10/2011, at 8:43 PM, Makarius wrote:
> On Tue, 11 Oct 2011, Makarius wrote:
>
>> On Tue, 11 Oct 2011, Gerwin Klein wrote:
>>
>>> The AFP test is back to testing against normal isabelle tip. I'm assuming
>>> the failures below are due to that.
>>
>> Maybe it is better to leave it at isab
On Tue, 11 Oct 2011, Makarius wrote:
On Tue, 11 Oct 2011, Gerwin Klein wrote:
The AFP test is back to testing against normal isabelle tip. I'm assuming
the failures below are due to that.
Maybe it is better to leave it at isabelle-release until AFP for
Isabelle2011-1 is finalized. I have r
On Tue, 11 Oct 2011, Gerwin Klein wrote:
The AFP test is back to testing against normal isabelle tip. I'm
assuming the failures below are due to that.
Maybe it is better to leave it at isabelle-release until AFP for
Isabelle2011-1 is finalized. I have ran some unsystematic tests on it and
i
On 18.09.2011 14:37, Florian Haftmann wrote:
*** Undeclared constant: "semilattice_sup_class.sup"
*** At command "definition" (line 20 of
"/home/kleing/afp/devel/thys/JinjaThreads/Execute/Cset_without_equal.thy")
val it = (): unit
Exception- TOPLEVEL_ERROR raised
*** ML error
It looks like some
Thanks. I've set the JinjaThreads test to run every day now, at least until the
release.
In Munich, we now also use our number cruncher lxbroy10 to run the large
(non-frequently tested) AFP sessions within the new testing infrastructure.
This should give us some more light on failures of th
On 18/09/2011, at 10:37 PM, Florian Haftmann wrote:
>> *** Undeclared constant: "semilattice_sup_class.sup"
>> *** At command "definition" (line 20 of
>> "/home/kleing/afp/devel/thys/JinjaThreads/Execute/Cset_without_equal.thy")
>> val it = (): unit
>> Exception- TOPLEVEL_ERROR raised
>> *** ML e
On Sun, Sep 18, 2011 at 1:42 AM, Gerwin Klein wrote:
> After not running in the test for quite some time, JinjaThreads now comes
> back failing:
>
> *** Undeclared constant: "semilattice_sup_class.sup"
> *** At command "definition" (line 20 of
> "/home/kleing/afp/devel/thys/JinjaThreads/Execute/
> *** Undeclared constant: "semilattice_sup_class.sup"
> *** At command "definition" (line 20 of
> "/home/kleing/afp/devel/thys/JinjaThreads/Execute/Cset_without_equal.thy")
> val it = (): unit
> Exception- TOPLEVEL_ERROR raised
> *** ML error
>
> It looks like something in the class setup change
After not running in the test for quite some time, JinjaThreads now comes back
failing:
*** Undeclared constant: "semilattice_sup_class.sup"
*** At command "definition" (line 20 of
"/home/kleing/afp/devel/thys/JinjaThreads/Execute/Cset_without_equal.thy")
val it = (): unit
Exception- TOPLEVEL_ER
On 04/08/2011 01:03 PM, Stefan Berghofer wrote:
Quoting Lukas Bulwahn :
Hi,
My changes caused this error.
I am working on different compilation schemes in Quickcheck.
Quickcheck registers its type-class based generator construction in
the Datatype package in the HOL image.
Hi Lucas,
acco
Quoting Lukas Bulwahn :
Hi,
My changes caused this error.
I am working on different compilation schemes in Quickcheck.
Quickcheck registers its type-class based generator construction in the
Datatype package in the HOL image.
Hi Lucas,
according to the trace, the exception occurs somewher
Thanks.
I didn't want to be particularly pushy, but since Tobias is away I wanted to
make sure people are aware that the test is failing.
It may be a good idea to put all regular Isabelle committers on the
notification list for the AFP test.
Does that make sense? Is there anyone who does not
On Fri, 8 Apr 2011, Lukas Bulwahn wrote:
My changes caused this error.
I am working on different compilation schemes in Quickcheck. Quickcheck
registers its type-class based generator construction in the Datatype
package in the HOL image.
For the record, this is what hg bisect said:
The fi
Hi,
My changes caused this error.
I am working on different compilation schemes in Quickcheck.
Quickcheck registers its type-class based generator construction in the
Datatype package in the HOL image.
The complete Isabelle repository ran through (with all its datatypes),
but the Sigma theo
Integration has been failing for a couple of days now. Anybody feel
responsible for fixing it? Most likely something to do with the reals...
Tobias
Original Message
Subject: status (AFP)
Date: Mon, 1 Sep 2008 12:07:05 +0200 (CEST)
From: isat...@atbroy51.informatik.tu-muenchen.d
34 matches
Mail list logo
