[isabelle-dev] AFP: Session AVL-Trees broken

[Makarius]

On Wed, 2 Jan 2013, Jasmin Blanchette wrote:

> Am 01.01.2013 um 22:38 schrieb Makarius:
>
>> Anyway, since the "smt" method seems to work right now, I propose to 
>> wire up a test where smt_certificates and smt_read_only_certificates 
>> are left unchanged if ISABELLE_FULL_TEST is enabled.  Does that make 
>> sense, according to the meaning of these options?  SMT/Z3 should run 
>> without any certificates getting in between.
>
> I gave something like this a try:
>
>    Änderung:        50666:6f48853f08d5
>    Marke:           tip
>    Nutzer:          blanchet
>    Datum:           Wed Jan 02 09:31:25 2013 +0100
>    Zusammenfassung: actually run Z3 for "SMT_Tests" when "ISABELLE_FULL_TEST" is enabled
>
>> The conditionioning of the theories can be done with a little bit of ML 
>> for the options.
>
> What I have right now (without any "ML conditioning") is that 
> "SMT_Tests" is not run when the full tests are disabled. Then there are 
> already several other files testing that SMT's certificate mechanism 
> works. But I won't stop anybody if they want to change the setup so that 
> "SMT_Tests" runs against certificates in non-full mode.

This looks OK for me.  The SMT_Tests are just synthetic, but there are 
many of them, and the SMT_Examples don't seem to add so much.  "ML 
conditioning" would introduce further confusion due to odd variance of the 
meaning of theory content.

So we leave it for now.  In 935988e2b35a I had already enabled isatest to 
work with it, and it seems to have been successful today.


>From my side, the SMT/Z3 thread can be closed for the purpose of the 
coming release.

If Sasche still wants to make some more refinements, e.g. to address

   Z3 proof parser (line 34): unknown function symbol: "S2!val!0"
   http://isabelle.in.tum.de/repos/isabelle/annotate/b1f4291eb916/src/HOL/SMT_Examples/SMT_Tests.thy#l122

there are still approx. 2 weeks left to do it.


 	Makarius