David E. Narváez (Mar 10 2023 at 17:26): David E. Narváez (Mar 10 2023 at 17:26):I am trying to figure out why auto_nitpick does not work in my system. I am pretty sure it used to and I am not sure what changed that it does not anymore. My guess is it has not worked since I started using Arch Linux (the (several) installations were copied from my previous distro and now auto_nitpick does not work in any version). Note that writing nitpick after a theorem does work so it is not an installation problem. I wonder if it has to do with ulimit, processes, threads, etc. How would I go about debugging this?
Mathias Fleury (Mar 13 2023 at 05:39):did you check that auto_nitpick is activated? (plugin options > isabelle > tick auto-nitpick)?
Mathias Fleury (Mar 13 2023 at 05:40):try attempts to do so many things in parallel, that the issue might a timeout here, more than anything else…
David E. Narváez (Mar 14 2023 at 15:40):Ah, nvm: the problem is the counterexample I was getting from nitpick is spurious and try will ignore those. Thanks for the help!
Last updated: Apr 26 2024 at 04:17 UTC