Hi Brian,
Good work!
> There are still a couple of loose ends to take care of, which are
> currently marked with "BROKEN" in the sources:
>
> * Nitpick_Examples/Integer_Nits.thy: A call to nitpick on a goal with
> negative numerals doesn't work. I expect the problem originates in
> Tools/Nitpick/nitpick_hol.ML, which I have adapted to handle positive
> numerals only; it needs a neg_numeral case.
Fixed in db5026631799.
> * SMT_Examples/SMT_{Examples,Tests}.thy: Some smt proofs don't work,
> because the .certs files need to be updated again.
Fixed in a4476e55a241.
Sascha has explained to me how to regenerate SMT certificates. I'll use this
opportunity to share this information with the mailing list.
First some context: The "smt" proof method a priori requires the external
program Z3 to be installed ("isabelle getenv Z3_SOLVER"). Since we cannot
expect every user of Isabelle to have it, proofs in formalizations included
with Isabelle or in the AFP should not require it. As a work around, "smt" can
cache the raw Z3 proofs from one run as "certificates" and reuse these the next
time. Certificates have priority over running Z3; if a certificate is
available, it will be used.
Once in a while, we change Isabelle or "smt" in such a way that the
certificates (i.e. the raw Z3 proofs) become obsolete. To regenerate them,
first ensure that
declare [[smt_fixed = false]]
This is the default but it's overwritten in a number of places, e.g.
"src/HOL/SMT_Examples/SMT_Examples.thy". ("Fixed" basically means "read-only".)
Now that you've enabled writing, rerun Isabelle on the theories, with Z3
installed on your machine. Finally submit the updated ".certs" files.
To install Z3 3.2 for Linux, Mac, or Windows, just download the package from
http://www21.in.tum.de/~blanchet/z3-3.2.tgz
Jasmin
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
