[isabelle-dev] Fwd: status (AFP)

[Gerwin Klein]

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
> 
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: report-devel.txt
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20110408/0d8373b1/attachment-0001.txt>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: afp-test-devel-2011-04-07.log
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20110408/0d8373b1/attachment-0001.log>
-------------- next part --------------
>