[isabelle-dev] Fwd: status (AFP)

[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 <kleing at ertos.nicta.com.au>
>>> Date: 8 April 2011 6:21:49 AM AEST
>>> To: <kleing at cse.unsw.edu.au>
>>> 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-dev at in.tum.de
>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110408/0f08cdca/attachment-0002.html>