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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
