[isabelle-dev] Getting Nitpick to run on your repository

[Jasmin Christian Blanchette]

Hi all,

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/ 
kodkodi-1.2.3")
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.

Jasmin

[*] 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.