[isabelle-dev] NEWS

[Florian Haftmann]

Hi Jasmin,

> Congratulations on your heroic effort for reintroducing "set"!

heroism and foolhardiness are close together…

> 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.

Good news indeed.  Thanks for the patience.

>> 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.

Is there any reference to these details on some documentation (README,
manual, …)?  A grep for Kodkod over the sources did not look very
promising.  I do not have that e-mail at hand.

Cheers,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20120104/7f29a109/attachment.sig>