[isabelle-dev] Status of HOL/SMT

[Gerwin Klein]

On 05/12/2012, at 1:06 AM, Makarius <makarius at sketis.net> wrote:

> On Tue, 4 Dec 2012, Jasmin Christian Blanchette wrote:
>
>>> What is also strange is that there seems to be no isatest/mira run that actually invokes Z3 again on these example theories.
>>
>> ... nor can there be, with the way in which the certification is hard-coded in them. I don't have a quick solutions for this; problems that Sascha hasn't addressed in four years aren't going to vanish automagically by my putting one lost hour here and there.
>
> If you provide a state where the SMT_Examples session can reproduce its proofs, I should be able to wire up some alternative session run with [condition=ISABELLE_FULL_TEST].
>
> I've done this recently for several other sessions where that was "forgotten", e.g. Sum_of_Squares and the skip_proofs flag.  (For WWW_Find I don't know how to do that, so it remains untested and broken for now.)

Tim is looking at WWW_Find, but he's in the process of moving to France, so there might be a few delays.

WWW_Find is not a session as such, though, so I'm not sure why it becomes relevant here. It should just work from an existing image and not do any proofs itself on top.

Cheers,
Gerwin


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.