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