On Tue, 4 Dec 2012, Gerwin Klein wrote:
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
On 05/12/2012, at 1:06 AM, Makarius 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 certif
more stable way. I'll need a bit
more time. Everything should be fixed by the end of the year.
Cheers,
Sascha
- Ursprüngliche Nachricht -
Von: Jasmin Christian Blanchette
Gesendet: 04.12.2012 15:07
An: Makarius
Cc: isabelle-dev Mailinglist; Sascha Boehme
Betreff: Re: [isabelle-dev] Sta
On Tue, 4 Dec 2012, Jasmin Blanchette wrote:
Am 04.12.2012 um 18:11 schrieb Johannes Hölzl:
I remove the SMT certificates in HOL-Multivariate_Analysis in
Isabelle/4b4fe0d5ee22.
Thanks! I didn't mean to apply pressure on you, though. ;)
Nobody does. It is more important to put issues on t
Am 04.12.2012 um 18:11 schrieb Johannes Hölzl:
> I remove the SMT certificates in HOL-Multivariate_Analysis in
> Isabelle/4b4fe0d5ee22.
Thanks! I didn't mean to apply pressure on you, though. ;)
Jasmin
___
isabelle-dev mailing list
isabelle-...@in.tu
Am Dienstag, den 04.12.2012, 15:13 +0100 schrieb Jasmin Blanchette:
> Am 04.12.2012 um 15:06 schrieb Makarius:
>
> > If you provide a state where the SMT_Examples session can reproduce its
> > proofs,
>
> I'll try to. Last time I regenerated the certificate, there were a couple of
> cases where
Am 04.12.2012 um 15:29 schrieb Makarius:
> The question which SMT/Z3 version to ship with the release basically has time
> until the new year.
I'm a big fan of "if it ain't broken don't fix it", so let's defaut on 3.2, and
in the unlikely event that both the parser issue with 4.0 and "rewr_conv
On Tue, 4 Dec 2012, Jasmin Blanchette wrote:
In general, we should try to reduce our exposure to SMT proofs in
Isabelle (and keep it to 0 in the AFP). That "SMT_Examples" use them is
fine, but any "smt" call that can be replaced by something else in other
places, e.g. "Multivariate_Analysis",
On Tue, 4 Dec 2012, Jasmin Christian Blanchette wrote:
Am 04.12.2012 um 14:52 schrieb Jasmin Christian Blanchette:
The real issue, at the end of the day, seems to be not so much Z3 4.0
in itself but rather the fact that our code often can't parse them.
I've looked into this and saw no quick f
Am 04.12.2012 um 15:06 schrieb Makarius:
> If you provide a state where the SMT_Examples session can reproduce its
> proofs,
I'll try to. Last time I regenerated the certificate, there were a couple of
cases where I was not successful with 3.2 (on my Mac) and had to use 4.0. But I
need to dig
Am 04.12.2012 um 14:52 schrieb Jasmin Christian Blanchette:
> The real issue, at the end of the day, seems to be not so much Z3 4.0 in
> itself but rather the fact that our code often can't parse them. I've looked
> into this and saw no quick fix [*].
Oh, Tobias just reminded me that a second i
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 solutio
Hi Makarius,
Sascha and I are responsible for SMT. Sascha still occasionally works on it,
but I bear the ultimate responsibility for it now.
> Then running some examples with the current z3-4.0 version produced a lot of
> errors, see the included change for SMT_Examples.thy and the resulting
>
Dear all,
since SMT and Z3 has been mentioned several times recently, I was curious
to see how it works at the moment -- also in preparation of the release.
This immediately lead to a problem with the external cache-access not
being thread-safe. It is addressed in Isabelle/4d1590544b91.
Th
14 matches
Mail list logo
