Re: [isabelle] Nitpick counterexample for true statement



Dear Peter,

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

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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.