[isabelle-dev] Fwd: status (AFP)

2012-12-16 Thread Gerwin Klein
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:

Re: [isabelle-dev] Fwd: status (AFP)

2012-09-24 Thread Makarius
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

Re: [isabelle-dev] Fwd: status (AFP)

2012-09-24 Thread Lukas Bulwahn
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

[isabelle-dev] Fwd: status (AFP)

2012-09-21 Thread Lukas Bulwahn
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

Re: [isabelle-dev] Fwd: status (AFP)

2012-09-21 Thread Jasmin Christian Blanchette
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

Re: [isabelle-dev] Fwd: status (AFP)

2012-09-21 Thread Makarius
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

Re: [isabelle-dev] Fwd: status (AFP)

2012-09-21 Thread Makarius
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

[isabelle-dev] Fwd: status (AFP)

2012-03-11 Thread Tobias Nipkow
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

Re: [isabelle-dev] Fwd: status (AFP)

2012-03-11 Thread Lukas Bulwahn
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

[isabelle-dev] Fwd: status (AFP)

2012-03-07 Thread Tobias Nipkow
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)

[isabelle-dev] Fwd: status (AFP)

2011-10-20 Thread Lukas Bulwahn
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)

Re: [isabelle-dev] Fwd: status (AFP)

2011-10-14 Thread Makarius
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.

Re: [isabelle-dev] Fwd: status (AFP)

2011-10-14 Thread David Matthews
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.

Re: [isabelle-dev] Fwd: status (AFP)

2011-10-14 Thread Gerwin Klein
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?

[isabelle-dev] Fwd: status (AFP)

2011-10-13 Thread Gerwin Klein
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:

Re: [isabelle-dev] Fwd: status (AFP)

2011-10-11 Thread Makarius
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

Re: [isabelle-dev] Fwd: status (AFP)

2011-10-11 Thread Makarius
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

Re: [isabelle-dev] Fwd: status (AFP)

2011-09-21 Thread Lukas Bulwahn
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

[isabelle-dev] Fwd: status (AFP)

2011-09-18 Thread Gerwin Klein
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

Re: [isabelle-dev] Fwd: status (AFP)

2011-09-18 Thread Brian Huffman
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

Re: [isabelle-dev] Fwd: status (AFP)

2011-09-18 Thread Gerwin Klein
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

Re: [isabelle-dev] Fwd: status (AFP)

2011-04-08 Thread 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. The complete Isabelle repository ran through (with all its datatypes), but the Sigma

Re: [isabelle-dev] Fwd: status (AFP)

2011-04-08 Thread Stefan Berghofer
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

Re: [isabelle-dev] Fwd: status (AFP)

2011-04-08 Thread Lukas Bulwahn
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.

[isabelle-dev] [Fwd: status (AFP)]

2008-09-01 Thread Tobias Nipkow
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: