Re: [isabelle] Isabelle2021-1-RC3: verit errors



Hi Peter,

It is a global option, not a sledgehammer-only option, so:

supply [[smt_trace]]


Do you have any example with a failure?


Mathias


On 14/11/2021 13:54, Peter Lammich wrote:
I get a lot of verit errors from sledgehammer.

"verit": Prover error:
Solver "verit" failed -- enable tracing using the "smt_trace" option
for details

And there is no smt_trace option to sledgehammer, at least sledgehammer
[smt_trace] tells me so, and the sledgehammer manual does not contain
the string smt_trace!

--
   Peter


On Fri, 2021-11-12 at 21:26 +0100, Makarius wrote:
Dear Isabelle users,

please see https://isabelle.sketis.net/website-Isabelle2021-1-RC3 and
https://isabelle-dev.sketis.net/phame/post/view/53/release_candidates_for_isabelle2021-1
for further progress on the release process.

There is now a proper download for Linux (ARM), and the "isabelle
build_docker" tools works for it (relevant on Apple M1 hardware).

This is also the fork-point of the isabelle-dev repository, which
continues
for the time after this release:
https://isabelle.sketis.net/repos/isabelle/rev/4f1c1c7eb95f


Reminder: Any feedback about release candidates should be posted with
a meaningful
Subject (not just a clone of the announcement).

We have approx. 4 weeks left until final lift-off: afterwards there
will be no
more changes on this line.


	Makarius






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.