[isabelle-dev] Status of HOL/SMT

[Johannes Hölzl]

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 I was not successful with 3.2 (on my Mac) and had to use 4.0. But I need to dig down into this again. It's on my radar, but probably not before February.
> 
> 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", should be done in the long term. It's something where the Sledgehammer Isar proof generation framework should help at some point (e.g. in one year from now) -- once we're done with the ATP side we'll see what can be done with SMT proofs.

I remove the SMT certificates in HOL-Multivariate_Analysis in
Isabelle/4b4fe0d5ee22.

> > I should be able to wire up some alternative session run with [condition=ISABELLE_FULL_TEST].
> 
> Be aware that
> 
>     declare [[smt_read_only_certificates = true]]
> 
> is hard-coded in those files, and this flags basically says: "use the certificates, and if they're not there, fail". (You're free, of course, to rethink the entire mechanism.)
> 
> Jasmin
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev