[isabelle-dev] Status of HOL/SMT

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