[isabelle-dev] The coming release of Isabelle2017

[Blanchette, J.C.]

Hi Makarius,

> Is there anything else to take into account for this late-summer release
> process?

Simon Cruanes (cc:) and I are still working on Nunchaku, which we intend to become Nitpick's successor. I have some patches locally that move the current "Nunchaku.thy" to Main (it's not much code and doesn't slow up building Main noticeably), but we're also working on the "nunchaku" component itself, which we will repack and update. We'll also add an "smbc" component, for another OCaml tool also developed by Simon Cruanes [*], which provides a "SAT solver + narrowing" backend to the "nunchaku" tool.

I will also update the "Nitpick_Examples" to also perform regression tests on Nunchaku.

I'm aiming at doing all the necessary changes by the end of August at the latest.

Jasmin

[*] https://cedeela.fr/~simon/files/cade_17_paper.pdf