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:
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
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
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
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
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
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
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
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 Nipkownip...@in.tum.de wrote:
One error in JinjaThreads was fixed, here is the next one:
*** Unknown fact list_all2_update_cong2 (line 467
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 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.
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.
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?
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:
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
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
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
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_ERROR
On Sun, Sep 18, 2011 at 1:42 AM, Gerwin Klein gerwin.kl...@nicta.com.au 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
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 error
It looks
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
Quoting Lukas Bulwahn bulw...@in.tum.de:
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
On 04/08/2011 01:03 PM, Stefan Berghofer wrote:
Quoting Lukas Bulwahn bulw...@in.tum.de:
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.
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:
25 matches
Mail list logo