On Wed, 8 Apr 2015, Jasmin Blanchette wrote:
- Z3 is now always enabled by default, now that it is fully open
source. The "z3_non_commercial" option is discontinued.
In addition, Z3 should now (again) be invoked by default by
Sledgehammer. Let me know if you see anything odd, e.g. odd problems
with binaries on Linux or Windows.
What is still not clear to me is how provers are determined. The
Sledgehammer panel uses the system option "sledgehammer_provers", after
many failed attempts in the past to cope with the ML heuristics. In
Isabelle/323feed18a92 I've tried to update this wrt. recent changes. Is
it true that E prover now has this low priority in the list? It was once
first, IIRC.
Moreover, in Isabelle/dda1e781c7b4 I've updated the NEWS to say explicitly
that the scheduling for provers managed by the Sledgehammer panel should
now work better wrt. ongoing edits. Despite such routine improvements,
many users will probably just stick to old habits from the TTY age, and
put the sledgehammer command into the text. (Are there remaining uses of
this ancient form? Or are there still pending problems with the current
Sledgehammer panel?)
BTW, the Sledgehammer manual still describes a situation before the
Sledgehammer panel came into existance in 2013. (It mentions the earlier
Auto Sledgehammer in PIDE, though.)
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
