<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
<meta content="text/html; charset=ISO-8859-1"
http-equiv="Content-Type">
<title></title>
</head>
<body text="#000000" bgcolor="#ffffff">
Hi,<br>
<br>
<br>
My changes caused this error.<br>
<br>
I am working on different compilation schemes in Quickcheck.<br>
Quickcheck registers its type-class based generator construction in
the Datatype package in the HOL image.<br>
<br>
The complete Isabelle repository ran through (with all its
datatypes), but the Sigma theory seems to contain some unexpected
datatype.<br>
<br>
I will look at the problem immediately, and probably fix it within
the next couple of hours.<br>
<br>
<br>
Lukas<br>
<br>
<br>
On 04/08/2011 12:24 AM, Gerwin Klein wrote:
<blockquote
cite="mid:96104395-384F-4BAD-BBEA-8796BE0E7923@nicta.com.au"
type="cite">
<pre wrap="">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:
</pre>
<blockquote type="cite">
<pre wrap="">From: Gerwin Klein <a class="moz-txt-link-rfc2396E" href="mailto:kleing@ertos.nicta.com.au"><kleing@ertos.nicta.com.au></a>
Date: 8 April 2011 6:21:49 AM AEST
To: <a class="moz-txt-link-rfc2396E" href="mailto:kleing@cse.unsw.edu.au"><kleing@cse.unsw.edu.au></a>
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 <a class="moz-txt-link-freetext" href="http://afp.sourceforge.net/status.shtml">http://afp.sourceforge.net/status.shtml</a>
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
</pre>
<pre wrap="">
<fieldset class="mimeAttachmentHeader"></fieldset>
</pre>
<blockquote type="cite">
<pre wrap="">
</pre>
</blockquote>
<pre wrap="">
</pre>
<pre wrap="">
<fieldset class="mimeAttachmentHeader"></fieldset>
_______________________________________________
isabelle-dev mailing list
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<a class="moz-txt-link-freetext" href="https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev</a>
</pre>
</blockquote>
</blockquote>
<br>
</body>
</html>