[isabelle-dev] Getting Nitpick to run on your repository
Jasmin Christian Blanchette
jasmin.blanchette at gmail.com
Wed Oct 28 15:29:26 CET 2009
The Nitpick counterexample generator is now [*] part of Isabelle/HOL's
repository version. You can use it in any theory that imports Main.
Gotcha: You'll need to install Kodkodi (and make sure a Java
interpreter is installed).
1. Download http://www4.in.tum.de/~blanchet/kodkodi-1.2.3.tgz
2. Unzip and untar it
3. Put it somewhere you like (e.g., in "/home/nipkow/isabelle/contrib/
4. Add the path "/home/nipkow/isabelle/contrib/kodkodi-1.2.3" to the
bottom of the file "$ISABELLE_HOME/etc/components"
Next time you enter a putative lemma, you can type "nitpick" to search
for a counterexample. The manual is in "$ISABELLE_HOME/doc-src/
Nitpick"; just do "make pdf" there.
I'm currently working on an Auto Nitpick option, just like Auto
Quickcheck. Keep syncing.
Enjoy! And let me know if you run into problems or have other questions.
[*] Don't ask for the change set identifier because I couldn't tell
you even to save my life. I can tell you that it has been in for the
past several hours.
More information about the isabelle-dev