<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>