<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; ">Thanks. <div><br></div><div>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. </div><div><br></div><div>It may be a good idea to put all regular Isabelle committers on the notification list for the AFP test.</div><div><br></div><div>Does that make sense? Is there anyone who does not want to be included?</div><div><br></div><div>Cheers,</div><div>Gerwin<br><div><br><div><div>On 08/04/2011, at 4:36 PM, Lukas Bulwahn wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite">
<div 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>
</div>
</blockquote></div><br></div></div></body></html>