[isabelle-dev] Fwd: status (AFP)

[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<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/85f56880/attachment-0002.html>