[isabelle-dev] NEWS

Wed Jan 4 00:34:04 CET 2012

Hi Florian,

Congratulations on your heroic effort for reintroducing "set"!

I'm glad to report that Nitpick, Refute, Sledgehammer, and SMT_Example have now been ported to handle "set" properly, and that the commented out examples are live again. I've also reenabled Kodkod for Isatests and Mira.

> There is a failure in Nitpick_Examples which is neither reproducible on
> macbroy2 nor my local machine:
> http://isabelle.in.tum.de/reports/Isabelle/report/14fe4e1bd31f4a9fab112f57669a1de5

BTW "Nitpick_Examples" should have been failing all over the place. If they haven't, this indicates that neither of your two setups (macbroy2 and local machine) have Kodkod enabled. See my 21 June 2010 email to you for details on how to test "Nitpick_Examples". As a rule of thumb, "Nitpick_Examples" should take at least 5 minutes to run. If it takes much less than that, it must be skipping most of the tests, which points to a missing Kodkodi.

Cheers,

Jasmin