Email Gateway (Aug 22 2022 at 19:18): Email Gateway (Aug 22 2022 at 19:18):From: Peter Lammich <lammich@in.tum.de>
Hi list,
nitpick is a great tool, as long as it does not refute provable lemmas,
as in the case below.
By the way, nunchaku chokes on this with an internal error.
Tested with Isabelle2018 and 9a7f94ab4df9, the result is the same.
Email Gateway (Aug 22 2022 at 19:20):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Dear Peter,
Thank you for your nitpicking! For Nitpick, I now have a few soundness bugs that I haven't investigated yet. It may be that it's the same issue.
Although Nitpick isn't in the "critical path", soundness bugs for Nitpick are really annoying, because it often takes 5-10 minutes to make sense of a counterexample, and if it's not correct, then that's really annoying.
I want to get rid of Nitpick anyway once Nunchaku is finished (or good enough). I haven't found a student to take over Nunchaku yet but I am hiring some new PhD students and one of them might take over the tool.
Cheers,
Jasmin
Last updated: Apr 24 2024 at 04:17 UTC