[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: isat...@macbroy2.informatik.tu-muenchen.de (Isabelle )
> Subject: status (AFP)
> Date: 16 December 2012 5:59:14 PM AEDT
> To: undisclosed-recipients:;
> 
> The status of the following AFP entries changed or remains FAIL: 
> [Possibilistic_Noninterference] is still on FAIL.
> [Separation_Logic_Imperative_HOL] is still on FAIL.
> 
> Full entry status at http://afp.sourceforge.net/status.shtml
> 
> AFP version: development -- hg id 519e8aa3ea9f
> Isabelle version: devel -- hg id e4dc37ec1427
> Test ended on: macbroy2, Sun Dec 16 07:59:14 CET 2012.
> 
> Have a nice day,
>  isatest
> 
Stream-Fusion: ok
Ramsey-Infinite: ok
Binomial-Heaps: ok
Ordinals_and_Cardinals: ok
ClockSynchInst: ok
Huffman: ok
Completeness: ok
Well_Quasi_Orders: ok
Abstract-Hoare-Logics: ok
Free-Boolean-Algebra: ok
Stuttering_Equivalence: ok
Girth_Chromatic: ok
Valuation: ok
InformationFlowSlicing_Intra: ok
FunWithFunctions: ok
Coinductive: ok
Possibilistic_Noninterference: FAIL
Heard_Of: ok
Abstract-Rewriting: ok
Matrix: ok
POPLmark-deBruijn: ok
MonoBoolTranAlgebra: ok
FeatherweightJava: ok
DiskPaxos: ok
Free-Groups: ok
Functional-Automata: ok
GraphMarkingIBP: ok
Transitive-Closure-II: ok
Tycon: ok
BytecodeLogicJmlTypes: ok
Finger-Trees: ok
WorkerWrapper: ok
Separation_Algebra: ok
General-Triangle: ok
Program-Conflict-Analysis: ok
LinearQuantifierElim: ok
GenClock: ok
Inductive_Confidentiality: ok
Recursion-Theory-I: ok
Efficient-Mergesort: ok
BinarySearchTree: ok
TLA: ok
Lam-ml-Normalization: ok
CoreC++: ok
Marriage: ok
Shivers-CFA: ok
SATSolverVerification: ok
InformationFlowSlicing_Inter: ok
Example-Submission: ok
SumSquares: ok
JiveDataStoreModel: ok
BDD: ok
Polynomials: ok
Datatype_Order_Generator: ok
Verified-Prover: ok
Topology: ok
KBPs: ok
ArrowImpossibilityGS: ok
Lazy-Lists-II: ok
Locally-Nameless-Sigma: ok
DataRefinementIBP: ok
JinjaThreads: ok
DPT-SAT-Solver: ok
Tarskis_Geometry: ok
RIPEMD-160-SPARK: ok
Flyspeck-Tame: ok
Regular-Sets: ok
RSAPSS: ok
LightweightJava: ok
Gauss-Jordan-Elim-Fun: ok
Separation_Logic_Imperative_HOL: FAIL
AVL-Trees: ok
Category: ok
AutoFocus-Stream: ok
CofGroups: ok
Perfect-Number-Thm: ok
Depth-First-Search: ok
Abortable_Linearizable_Modules: ok
Statecharts: ok
PseudoHoops: ok
Max-Card-Matching: ok
Bondy: ok
FunWithTilings: ok
SenSocialChoice: ok
CCS: ok
Open_Induction: ok
List-Index: ok
Markov_Models: ok
Cauchy: ok
Ordinal: ok
Myhill-Nerode: ok
Binomial-Queues: ok
Fermat3_4: ok
FOL-Fitting: ok
MuchAdoAboutTwo: ok
Dijkstra_Shortest_Path: ok
SIFPL: ok
Presburger-Automata: ok
Circus: ok
Transitive-Closure: ok
Impossible_Geometry: ok
Category2: ok
Integration: ok
MiniML: ok
NormByEval: ok
PCF: ok
SequentInvertibility: ok
Pi_Calculus: ok
FileRefinement: ok
FFT: ok
Robbins-Conjecture: ok
Compiling-Exceptions-Correctly: ok
Ordinary_Differential_Equations: ok
VolpanoSmith: ok
HotelKeyCards: ok
Tree-Automata: ok
FinFun: ok
Psi_Calculi: ok
Lower_Semicontinuous: ok
Start test for /home/isatest/afp/devel at Sun Dec 16 06:05:45 CET 2012, macbroy2

begin hg pull/update
pulling from ssh://isat...@afp.hg.sourceforge.net/hgroot/afp/afp
searching for changes
no changes found
end hg pull/update

AFP version: development -- hg id 519e8aa3ea9f
Isabelle version: devel -- hg id e4dc37ec1427

Building HOLCF ...
Finished HOLCF (0:00:36 elapsed time, 0:00:58 cpu time, factor 1.61)
Building HOL-Nominal ...
Finished HOL-Nominal (0:00:14 elapsed time, 0:00:22 cpu time, factor 1.57)
Building HOL-Multivariate_Analysis ...
Finished HOL-Multivariate_Analysis (0:01:54 elapsed time, 0:05:14 cpu time, 
factor 2.75)
Building HOL-Word ...
Finished HOL-Word (0:00:28 elapsed time, 0:01:02 cpu time, factor 2.21)
Building Jinja ...
Finished Jinja (0:04:02 elapsed time, 0:12:23 cpu time, factor 3.07)
Building LatticeProperties ...
Finished LatticeProperties (0:00:14 elapsed time, 0:00:21 cpu time, factor 1.50)
Building HOL-Probability ...
Finished HOL-Probability (0:01:30 elapsed time, 0:04:08 cpu time, factor 2.75)
Building HRB-Slicing ...
Finished HRB-Slicing (0:04:57 elapsed time, 0:15:15 cpu time, factor 3.08)
Building Slicing ...
Finished Slicing (0:04:43 elapsed time, 0:15:04 cpu time, factor 3.19)
Building Group-Ring-Module ...
Finished Group-Ring-Module (0:02:17 elapsed time, 0:06:49 cpu time, factor 2.98)
Building Simpl ...
Finished Simpl (0:01:42 elapsed time, 0:04:49 cpu time, factor 2.83)
Building Collections ...
Finished Collections (0:04:00 elapsed time, 0:09:28 cpu time, factor 2.36)
Building Refine_Monadic ...
Finished Refine_Monadic (0:01:05 elapsed time, 0:02:29 cpu time, factor 2.29)
Building List-Infinite ...
Finished List-Infinite (0:00:32 elapsed time, 0:01:10 cpu time, factor 2.18)
Building Nat-Interval-Logic ...
Finished Nat-Interval-Logic (0:00:34 elapsed time, 0:

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 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


Did you do anything, or did it come back by itself?

I did restart a number of mira processes---the nagios tool from our 
sysadmin are monitoring them, so Lars and I get emails if they do not 
run anymore.


Lukas

In the meantime I also killed a number of inactive poly processes on 
the usual test machines.



Makarius


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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 nor testboard have been working.

 http://isabelle.in.tum.de/reports/Isabelle
 http://isabelle.in.tum.de/testboard/Isabelle


Did you do anything, or did it come back by itself?

In the meantime I also killed a number of inactive poly processes on the 
usual test machines.



Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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 FLYSPECK_SKIP_PROOFS=true in my settings and then run *all* 
of AFP in 35min on a plain-old 8-core workstation.


The new Isabelle build configuration has the "condition" option to 
formalize the omission of theories, depending on given environment 
variables.  ISABELLE_FULL_TEST (undefined by default) is already used as a 
convention to guard extra tests that take unusually long time.


If ISABELLE_FULL_TEST would be checked instead of FLYSPECK_SKIP_PROOFS in 
afp/thys/Flyspeck-Tame/ArchComp.thy with the inverted meaning, then one 
could discontinue the AFP vs. AFP_big distinction.  It would work for 
everyone by default within the range of 0.5 .. 2h total.


The full test would then be run infrequently by one of the standard test 
frameworks in the background.



Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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
   http://isabelle.in.tum.de/testboard/Isabelle


For me there is still some dark matter here that I don't understand.  The 
totality of Mira configuration is difficult to see.


Without looking, I suspect that the update to polyml-5.5.0 
Isabelle/617869cd779c confuses Mira, which still has some odd references 
to the old /home/isabelle/contrib_devel with its funny symlinks.



Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2012-09-21 Thread Lukas Bulwahn 

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://isabelle.in.tum.de/reports/Isabelle
 http://isabelle.in.tum.de/testboard/Isabelle

Jasmin

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2012-09-21 Thread Tobias Nipkow 
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 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 following AFP entries changed or remains FAIL: 
> [KBPs] changed from FAIL to ok.
> 
> Full entry status at http://afp.sourceforge.net/status.shtml
> 
> AFP version: development -- hg id c3a75d6d802a
> Isabelle version: devel -- hg id 7bb0d515ccbc
> Test ended on: macbroy2, Fri Sep 21 09:10:43 CEST 2012.
> 
> Have a nice day,
>   isatest
> 
> 
> 
> 
> This body part will be downloaded on demand.
> 
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[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 following AFP entries changed or remains FAIL:
[KBPs] changed from FAIL to ok.

Full entry status at http://afp.sourceforge.net/status.shtml

AFP version: development -- hg id c3a75d6d802a
Isabelle version: devel -- hg id 7bb0d515ccbc
Test ended on: macbroy2, Fri Sep 21 09:10:43 CEST 2012.

Have a nice day,
  isatest



Stream-Fusion: ok
Ramsey-Infinite: ok
Binomial-Heaps: ok
Ordinals_and_Cardinals: ok
ClockSynchInst: ok
Huffman: ok
Completeness: ok
Well_Quasi_Orders: ok
Abstract-Hoare-Logics: ok
Free-Boolean-Algebra: ok
Stuttering_Equivalence: ok
Girth_Chromatic: ok
Valuation: ok
FunWithFunctions: ok
Coinductive: ok
Heard_Of: ok
Abstract-Rewriting: ok
Matrix: ok
POPLmark-deBruijn: ok
MonoBoolTranAlgebra: ok
FeatherweightJava: ok
DiskPaxos: ok
Free-Groups: ok
Functional-Automata: ok
GraphMarkingIBP: ok
Transitive-Closure-II: ok
Tycon: ok
BytecodeLogicJmlTypes: ok
Finger-Trees: ok
WorkerWrapper: ok
Separation_Algebra: ok
General-Triangle: ok
Program-Conflict-Analysis: ok
LinearQuantifierElim: ok
GenClock: ok
Inductive_Confidentiality: ok
Recursion-Theory-I: ok
Efficient-Mergesort: ok
BinarySearchTree: ok
TLA: ok
Lam-ml-Normalization: ok
CoreC++: ok
Marriage: ok
Shivers-CFA: ok
SATSolverVerification: ok
Example-Submission: ok
SumSquares: ok
BDD: ok
JiveDataStoreModel: ok
Polynomials: ok
Datatype_Order_Generator: ok
Verified-Prover: ok
Topology: ok
KBPs: ok
ArrowImpossibilityGS: ok
Lazy-Lists-II: ok
Locally-Nameless-Sigma: ok
DataRefinementIBP: ok
JinjaThreads: ok
HRB-Slicing: ok
DPT-SAT-Solver: ok
RIPEMD-160-SPARK: ok
Flyspeck-Tame: ok
Regular-Sets: ok
RSAPSS: ok
LightweightJava: ok
Gauss-Jordan-Elim-Fun: ok
AVL-Trees: ok
Category: ok
AutoFocus-Stream: ok
CofGroups: ok
Perfect-Number-Thm: ok
Depth-First-Search: ok
Abortable_Linearizable_Modules: ok
Statecharts: ok
PseudoHoops: ok
Max-Card-Matching: ok
FunWithTilings: ok
SenSocialChoice: ok
CCS: ok
List-Index: ok
Markov_Models: ok
Cauchy: ok
Ordinal: ok
Myhill-Nerode: ok
Binomial-Queues: ok
Fermat3_4: ok
FOL-Fitting: ok
MuchAdoAboutTwo: ok
Slicing: ok
Dijkstra_Shortest_Path: ok
SIFPL: ok
Presburger-Automata: ok
Circus: ok
Transitive-Closure: ok
Impossible_Geometry: ok
Category2: ok
Integration: ok
MiniML: ok
NormByEval: ok
PCF: ok
SequentInvertibility: ok
Pi_Calculus: ok
FileRefinement: ok
FFT: ok
Robbins-Conjecture: ok
Compiling-Exceptions-Correctly: ok
Ordinary_Differential_Equations: ok
VolpanoSmith: ok
HotelKeyCards: ok
Tree-Automata: ok
FinFun: ok
Psi_Calculi: ok
Lower_Semicontinuous: ok

Start test for /home/isatest/afp/devel at Fri Sep 21 06:31:44 CEST 2012, 
macbroy2

begin hg pull/update
pulling from ssh://isat...@afp.hg.sourceforge.net/hgroot/afp/afp
searching for changes
adding changesets
adding manifests
adding file changes
added 1 changesets with 1 changes to 1 files
1 files updated, 0 files merged, 0 files removed, 0 files unresolved
remote: Running preoutgoing hook
remote: Use of uninitialized value in concatenation (.) or string at 
/etc/mercurial/preoutgoing line 36.
end hg pull/update

AFP version: development -- hg id c3a75d6d802a
Isabelle version: devel -- hg id 7bb0d515ccbc

Building HOLCF ...
Finished HOLCF (0:00:50 elapsed time, 0:01:01 cpu time, factor 1.22)
Building HOL-Nominal ...
Finished HOL-Nominal (0:00:21 elapsed time, 0:00:23 cpu time, factor 1.09)
Building HOL-Multivariate_Analysis ...
Finished HOL-Multivariate_Analysis (0:03:00 elapsed time, 0:06:32 cpu time, 
factor 2.17)
Building HOL-Word ...
Finished HOL-Word (0:00:38 elapsed time, 0:01:07 cpu time, factor 1.76)
Building Jinja ...
Finished Jinja (0:05:48 elapsed time, 0:13:16 cpu time, factor 2.28)
Building LatticeProperties ...
Finished LatticeProperties (0:00:20 elapsed time, 0:00:22 cpu time, factor 1.10)
Building HOL-Probability ...
Finished HOL-Probability (0:01:43 elapsed time, 0:03:24 cpu time, factor 1.98)
Building Group-Ring-Module ...
Finished Group-Ring-Module (0:03:22 elapsed time, 0:07:08 cpu time, factor 2.11)
Building Simpl ...
Finished Simpl (0:02:35 elapsed time, 0:04:55 cpu time, factor 1.90)
Building Collections ...
Finished Collections (0:05:32 elapsed time, 0:08:31 cpu time, factor 1.53)
Building Refine_Monadic ...
Finished Refine_Monadic (0:01:51 elapsed time, 0:02:51 cpu time, factor 1.54)
Building List-Infinite ...
Finished List-Infinite (0:00:45 elapsed time, 0:01:18 cpu time, factor 1.73)
Building Nat-Interval-Logic ...
Finished Nat-Interval-Logic (0:00:50 elapsed time, 0:01:19 cpu time, factor 
1.58)
Running Flyspeck-Tame ...
Finished Flyspeck-Tame (0:03:12 elapsed time, 0:06:10 cpu time, factor 1.92)
Running JinjaThreads ...
Finished JinjaThreads (0:57:08 elapsed time, 1:51:07 cpu time, factor 1.94)
Running HRB-Slicing ...
Finished HRB-Slicing (0:05:54

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 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
"/mnt/nfsbroy/home/isatest/afp/devel/thys/JinjaThreads/BV/BVSpecTypeSafe.thy")
Exception- TOPLEVEL_ERROR raised

I guess this has to do with the following changeset:

changeset:   46665:c1d2ab32174a
user:bulwahn
date:Sat Feb 25 09:07:37 2012 +0100
summary: one general list_all2_update_cong instead of two special ones

http://isabelle.in.tum.de/repos/isabelle/rev/c1d2ab32174a
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2012-03-11 Thread Brian Huffman 
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
> "/mnt/nfsbroy/home/isatest/afp/devel/thys/JinjaThreads/BV/BVSpecTypeSafe.thy")
> Exception- TOPLEVEL_ERROR raised

I guess this has to do with the following changeset:

changeset:   46665:c1d2ab32174a
user:bulwahn
date:Sat Feb 25 09:07:37 2012 +0100
summary: one general list_all2_update_cong instead of two special ones

http://isabelle.in.tum.de/repos/isabelle/rev/c1d2ab32174a
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[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
"/mnt/nfsbroy/home/isatest/afp/devel/thys/JinjaThreads/BV/BVSpecTypeSafe.thy")
Exception- TOPLEVEL_ERROR raised

Tobias

 Original-Nachricht 
Betreff: status (AFP)
Datum: Sun, 11 Mar 2012 08:31:25 +0100 (CET)
Von: isat...@macbroy2.informatik.tu-muenchen.de (Isabelle )
An: undisclosed-recipients:;

The status of the following AFP entries changed or remains FAIL:
[JinjaThreads] is still on FAIL.

Full entry status at http://afp.sourceforge.net/status.shtml

AFP version: development -- hg id c0877261b9e2
Isabelle version: devel -- hg id b190913c3c41
Test ended on: macbroy2, Sun Mar 11 08:31:25 CET 2012.

Have a nice day,
  isatest



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[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)
Datum: Thu,  8 Mar 2012 08:26:35 +0100 (CET)
Von: isat...@macbroy2.informatik.tu-muenchen.de (Isabelle )
An: undisclosed-recipients:;

The status of the following AFP entries changed or remains FAIL:
[JinjaThreads] is still on FAIL.

Full entry status at http://afp.sourceforge.net/status.shtml

AFP version: development -- hg id 7906454ca15f
Isabelle version: devel -- hg id be56a254d880
Test ended on: macbroy2, Thu Mar  8 08:26:35 CET 2012.

Have a nice day,
  isatest



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[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")
val it = (): unit
Exception- TOPLEVEL_ERROR raised
*** ML error



I could not even inspect the proof state where it fails, as my machine 
is not able to load the theory.
If anyone here has an educated guess how this proof can be fixed, you 
should try.
There are at least two machines, lxbroy10 in Munich, and one in 
Australia, running regularly that can check these guesses once you push 
them.


Lukas


 Original Message 
Subject:status (AFP)
Date:   Fri, 21 Oct 2011 06:31:55 +1100
From:   Gerwin Klein 
To: undisclosed-recipients:;



The status of the following AFP entries changed or remains FAIL:
[JinjaThreads] is still on FAIL.

Full entry status athttp://afp.sourceforge.net/status.shtml

AFP version: development -- hg id a98f0ac6930a
Isabelle version: devel -- hg id c4fab1099cd0
Test ended on: lemma, Fri Oct 21 06:31:55 EST 2011.

Have a nice day,
  isatest



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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?
> 
>  http://isabelle.in.tum.de/devel/stats/afp.html

Yes.


> There used to be much less fluctuation with AFP on the hardware at TUM, IIRC.

A few years ago, yes, I think. More recently, the test used to crash almost 
every day at TUM, though, that's why I moved it to this server. The problems at 
the time seemed file system/NFS related. I have changed the setup since then 
and made it less dependent on NFS. Maybe it's time to move it back to TUM if we 
can get a dedicated (for the test time) machine there so we get more reliable 
timing results.


> Since the charts are derived from the "Finished" status it might also involve 
> the file-system.  Instead the inner "Timing" could be used to get closer to 
> the raw CPU characteristics.  Mira should also contain that information.

I doubt it's the file system, because there is almost no activity on the file 
system of that server at all. It doesn't run much else than long Isabelle 
sessions. The server is nowhere close to saturated in the current 
configuration, but it's still possible that having another concurrent Isabelle 
sessions interferes with the runtime.

I'd say we keep it with polyml-5.4.1 on that server for another week to find 
out if the version change fixed that particular problem and then I try moving 
the test back to a TUM server that doesn't run anything else at the same time.

Cheers,
Gerwin
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2011-10-14 Thread Gerwin Klein 

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(PolyWord, StackObject*, bool): Assertion
>>> `val.IsDataPtr()' failed.
>>> /home/kleing/volatile/isadist/Isabelle_13-Oct-2011/lib/scripts/run-polyml:
>>> line 77: 20095 Aborted "$POLY" -q $ML_OPTIONS
>>> Jinja FAILED
>> 
>> Yes, occasionally. Such hard crashes were more frequent in the past, and
>> we are running much more and bigger jobs now.
> 
> I pointed out in an email to Gerwin that this looks very like the bug that 
> was fixed in commit 1297 in Poly/ML head and 1318 in the fixes branch.  Which 
> version of Poly/ML was this?  It is possible that this could be the result of 
> a different bug in which case I will need to look more closely.

My version was poly-5.4.0 as distributed with Isabelle. I've switched the test 
to poly-5.4.1 now. We should know in a day or two if the problem still persists.

Cheers,
Gerwin
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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.
/home/kleing/volatile/isadist/Isabelle_13-Oct-2011/lib/scripts/run-polyml:
line 77: 20095 Aborted "$POLY" -q $ML_OPTIONS
Jinja FAILED


Yes, occasionally. Such hard crashes were more frequent in the past, and
we are running much more and bigger jobs now.


I pointed out in an email to Gerwin that this looks very like the bug 
that was fixed in commit 1297 in Poly/ML head and 1318 in the fixes 
branch.  Which version of Poly/ML was this?  It is possible that this 
could be the result of a different bug in which case I will need to look 
more closely.


Regards,
David
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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.
/home/kleing/volatile/isadist/Isabelle_13-Oct-2011/lib/scripts/run-polyml: line 77: 20095 
Aborted "$POLY" -q $ML_OPTIONS
Jinja FAILED


Yes, occasionally.  Such hard crashes were more frequent in the past, and 
we are running much more and bigger jobs now.


It often helps to modify ML_OPTIONS a bit, such as -H for the initial heap 
size.



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.tum.de/devel/stats/afp.html

There used to be much less fluctuation with AFP on the hardware at TUM, 
IIRC. Since the charts are derived from the "Finished" status it might 
also involve the file-system.  Instead the inner "Timing" could be used to 
get closer to the raw CPU characteristics.  Mira should also contain that 
information.



Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[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: 20095 Aborted "$POLY" -q $ML_OPTIONS
Jinja FAILED

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).

The problem does not seem to be Jinja itself, because Jinja does get built fine 
in one of the other sessions that depend on it later.

This is poly 5.4.0 64 bit on Linux, I might try updating it to 5.4.1 or the 
current svn. The same setup has been running without such problems for about a 
year, though. The only thing that I can think of that has changed in the last 
few weeks might be server load which has gone up, but is nowhere near 
saturated. And of course Isabelle is always changing, so the allocation of 
something might have changed as well.

Cheers,
Gerwin

Begin forwarded message:

> From: Gerwin Klein 
> Date: 14 October 2011 8:25:51 AM AEDT
> To: 
> Subject: status (AFP)
> 
> The status of the following AFP entries changed or remains FAIL: 
> [Jinja] is still on FAIL.
> 
> Full entry status at http://afp.sourceforge.net/status.shtml
> 
> AFP version: development -- hg id ceb9698de567
> Isabelle version: devel -- hg id 2214ba5bdfff
> Test ended on: lemma, Fri Oct 14 08:25:51 EST 2011.
> 
> Have a nice day,
>  isatest

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2011-10-11 Thread Gerwin Klein 

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 isabelle-release until AFP for 
>> Isabelle2011-1 is finalized.  I have ran some unsystematic tests on it and 
>> it produces very few failures.
> 
> What is the status of AFP anyway?  In the afp-devel repository I see both a 
> release tag (0e48fb185542) and post-release changes (eef0ef1627f9).

AFP is in the process of being released. This takes ages, because it needs to 
run every entry which takes > 10h. Adding a random problem here and there, and 
you're  looking at 2 days.

I've branched the 2011-1 release version, so in theory it's safe to push to 
devel as usual, I just didn't want to announce it yet before the release 
process isn't finished.

Gerwin
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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 ran some unsystematic tests on it and it 
produces very few failures.


What is the status of AFP anyway?  In the afp-devel repository I see both 
a release tag (0e48fb185542) and post-release changes (eef0ef1627f9).



Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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 
it produces very few failures.



Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2011-09-26 Thread Lars Noschinski 

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 something in the class setup changed slightly. Could somebody who 
is more up-to-date in this area have a look, please?


Done.


I might be missing something, but I haven't seen a fix in the 
repository? Nevertheless, I committed now the trivial 
semilattice_sup_class.sup -> sup_class.sup rename to JinjaThreads.


  -- Lars
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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 these AFP theories in 
the future.



Lukas
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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 like something in the class setup changed slightly. Could somebody 
>> who is more up-to-date in this area have a look, please?
> 
> Done.

Thanks. I've set the JinjaThreads test to run every day now, at least until the 
release.


>> After not running in the test for quite some time, JinjaThreads now
> comes back failing
> 
> This is one of the principal problems we have with JinjaThreads and
> FlyspeckTame that they don't run (more exactly, don't terminate)

JinjaThreads does terminate ;-), it just runs out of memory.

Flyspeck has always taken very long, but it terminates eventually.


> on our
> reference machines (macbroyXY, Apple IMac) since one year.  Somehow we
> must come to a solution for this, or at least figure out why this
> happends.  The mere size or massive computations alone cannot be the
> only reason for this.

It would certainly be nice to figure out where the memory is going in these 
computations and maybe even speed them up.

I have yet to pick up similar investigations for our seL4 proofs again. At 
least with the current polyml svn version, you can get more precise numbers on 
memory than before.

Cheers,
Gerwin
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2011-09-18 Thread Brian Huffman 
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/Cset_without_equal.thy")
> val it = (): unit
> Exception- TOPLEVEL_ERROR raised
> *** ML error
>
> It looks like something in the class setup changed slightly. Could somebody 
> who is more up-to-date in this area have a look, please?

This must be due to the recent changeset:

added syntactic classes for "inf" and "sup"
http://isabelle.in.tum.de/repos/isabelle/rev/5e51075cbd97

The fix is probably to replace "semilattice_sup_class.sup" with "sup_class.sup".

- Brian
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2011-09-18 Thread Florian Haftmann 
> *** 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 changed slightly. Could somebody 
> who is more up-to-date in this area have a look, please?

Done.


> After not running in the test for quite some time, JinjaThreads now
comes back failing

This is one of the principal problems we have with JinjaThreads and
FlyspeckTame that they don't run (more exactly, don't terminate) on our
reference machines (macbroyXY, Apple IMac) since one year.  Somehow we
must come to a solution for this, or at least figure out why this
happends.  The mere size or massive computations alone cannot be the
only reason for this.

Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[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 raised
*** ML error

It looks like something in the class setup changed slightly. Could somebody who 
is more up-to-date in this area have a look, please?

For the Isabelle release, we need to have all AFP entries in working order.

Cheers,
Gerwin

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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 :


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 somewhere in the function
derive_datatype_props in datatype_data.ML. When taking a quick look at
the code, I noticed that thy2 is used in two places (lines 311 and 322)
after it has already been modified. Is that intentional, or could this
be related to this bug, too?



Hi Stefan,

Thanks for your effort.
I have already fixed the error (on my local machine) -- it was actually 
related to some exception handling that has never been working, but was 
never triggered before this changeset.


Lukas



Greetings,
Stefan



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2011-04-08 Thread Stefan Berghofer 

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 somewhere in the function
derive_datatype_props in datatype_data.ML. When taking a quick look at
the code, I noticed that thy2 is used in two places (lines 311 and 322)
after it has already been modified. Is that intentional, or could this
be related to this bug, too?

Greetings,
Stefan

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2011-04-08 Thread Gerwin Klein 
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 want to be included?

Cheers,
Gerwin

On 08/04/2011, at 4:36 PM, Lukas Bulwahn wrote:

> 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 theory seems to contain some unexpected datatype.
> 
> I will look at the problem immediately, and probably fix it within the next 
> couple of hours.
> 
> 
> Lukas
> 
> 
> On 04/08/2011 12:24 AM, Gerwin Klein wrote:
>> 
>> Can someone have a look at what is going wrong in Locally-Nameless-Sigma? 
>> 
>> It looks like a bug in the datatype package is being triggered:
>> 
>> *** Stale theory encountered:
>> *** {Pure, Code_Generator, HOL, Orderings, Groups, Lattices, Set,
>> ***   Complete_Lattice, Typedef, Inductive, Fun, Product_Type, Rings, Fields,
>> ***   Sum_Type, Nat, Datatype, Complete_Partial_Order, Option, Power,
>> ***   Finite_Set, Relation, Predicate, Transitive_Closure, Partial_Function,
>> ***   Wellfounded, Meson, FunDef, Extraction, Metis, Plain, Big_Operators,
>> ***   Equiv_Relations, Int, Nat_Numeral, Nat_Transfer, Divides,
>> ***   Numeral_Simprocs, Semiring_Normalization, Groebner_Basis, SetInterval,
>> ***   Hilbert_Choice, Presburger, Recdef, Code_Numeral, Quotient, ATP, List,
>> ***   String, Typerep, Map, Random, Code_Evaluation, Enum, Lazy_Sequence,
>> ***   Quickcheck, DSequence, Random_Sequence, New_DSequence,
>> ***   New_Random_Sequence, Record, SMT, Sledgehammer, Refute, SAT,
>> ***   Predicate_Compile, Quickcheck_Exhaustive, Nitpick, Main, ListPre, FMap,
>> ***   Sigma:162, #, !}
>> *** At command "datatype" (line 80 of 
>> "/home/kleing/afp/devel/thys/Locally-Nameless-Sigma/Sigma/Sigma.thy")
>> 
>> Cheers,
>> Gerwin
>> 
>> Begin forwarded message:
>> 
>>> From: Gerwin Klein 
>>> Date: 8 April 2011 6:21:49 AM AEST
>>> To: 
>>> Subject: status (AFP)
>>> 
>>> The status of the following AFP entries changed or remains FAIL: 
>>> [Locally-Nameless-Sigma] is still on FAIL.
>>> 
>>> Full entry status at http://afp.sourceforge.net/status.shtml
>>> 
>>> AFP version: development -- hg id 29a8783494d0
>>> Isabelle version: devel -- hg id 7d08265f181d
>>> Test ended on: lemma, Fri Apr  8 06:21:49 EST 2011.
>>> 
>>> Have a nice day,
>>>  isatest
>>> 
>>> 
>>> 
>>> ___
>>> isabelle-dev mailing list
>>> isabelle-...@in.tum.de
>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2011-04-08 Thread Makarius 

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 first bad revision is:
changeset:   42230:594480d25aaa
user:bulwahn
date:Tue Apr 05 09:38:23 2011 +0200
summary: deriving bounded_forall instances in quickcheck_exhaustive


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2011-04-07 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 theory seems to contain some unexpected datatype.


I will look at the problem immediately, and probably fix it within the 
next couple of hours.



Lukas


On 04/08/2011 12:24 AM, Gerwin Klein wrote:

Can someone have a look at what is going wrong in Locally-Nameless-Sigma?

It looks like a bug in the datatype package is being triggered:

*** Stale theory encountered:
*** {Pure, Code_Generator, HOL, Orderings, Groups, Lattices, Set,
***   Complete_Lattice, Typedef, Inductive, Fun, Product_Type, Rings, Fields,
***   Sum_Type, Nat, Datatype, Complete_Partial_Order, Option, Power,
***   Finite_Set, Relation, Predicate, Transitive_Closure, Partial_Function,
***   Wellfounded, Meson, FunDef, Extraction, Metis, Plain, Big_Operators,
***   Equiv_Relations, Int, Nat_Numeral, Nat_Transfer, Divides,
***   Numeral_Simprocs, Semiring_Normalization, Groebner_Basis, SetInterval,
***   Hilbert_Choice, Presburger, Recdef, Code_Numeral, Quotient, ATP, List,
***   String, Typerep, Map, Random, Code_Evaluation, Enum, Lazy_Sequence,
***   Quickcheck, DSequence, Random_Sequence, New_DSequence,
***   New_Random_Sequence, Record, SMT, Sledgehammer, Refute, SAT,
***   Predicate_Compile, Quickcheck_Exhaustive, Nitpick, Main, ListPre, FMap,
***   Sigma:162, #, !}
*** At command "datatype" (line 80 of 
"/home/kleing/afp/devel/thys/Locally-Nameless-Sigma/Sigma/Sigma.thy")

Cheers,
Gerwin

Begin forwarded message:


From: Gerwin Klein
Date: 8 April 2011 6:21:49 AM AEST
To:
Subject: status (AFP)

The status of the following AFP entries changed or remains FAIL:
[Locally-Nameless-Sigma] is still on FAIL.

Full entry status at http://afp.sourceforge.net/status.shtml

AFP version: development -- hg id 29a8783494d0
Isabelle version: devel -- hg id 7d08265f181d
Test ended on: lemma, Fri Apr  8 06:21:49 EST 2011.

Have a nice day,
  isatest




___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

[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: isat...@atbroy51.informatik.tu-muenchen.de (Account Isatest)
To: undisclosed-recipients:;

The status of the following AFP entries changed or remains FAIL:
[Integration] is still on FAIL.

Tested version: development
Test ended on: atbroy51, Mon Sep  1 12:07:05 CEST 2008.

Have a nice day,
  isatest


-- next part --
An embedded and charset-unspecified text was scrubbed...
Name: report-devel
URL: 

-- next part --
An embedded and charset-unspecified text was scrubbed...
Name: afp-test-devel-2008-09-01.log
URL: