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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
