[isabelle-dev] NEWS: numeral representation

[Jasmin Christian Blanchette]

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