[isabelle-dev] NEWS

Jasmin Blanchette jasmin.blanchette at gmail.com
Wed Jan 4 21:56:34 CET 2012


Hi Florian,

Am 04.01.2012 um 21:10 schrieb Florian Haftmann:

> Is there any reference to these details on some documentation (README,
> manual, …)?

There used to be some documentation in the Nitpick manual  
(nitpick.pdf), but nowadays Kodkod(i) is shipped with Isabelle, so the  
problem only arises for adventurous people (i.e. developers). If you  
grep for MISSING in

http://isabelle.in.tum.de/repos/isabelle/file/edd50ec8d471/doc-src/Nitpick/nitpick.tex

you'll see some instructions.

And if you try running "nitpick" and Kodkodi isn't installed, you  
should get this message (from "nitpick.ML"):

    182 fun install_kodkodi_message () =
    183   "Nitpick requires the external Java program Kodkodi. To  
install it, download \
    184   \the package from Isabelle's web page and add the \"kodkodi- 
x.y.z\" \
    185   \directory's full path to " ^
    186   Path.print (Path.expand (Path.explode "$ISABELLE_HOME_USER/ 
etc/components")) ^
    187   " on a line of its own."

(from http://isabelle.in.tum.de/repos/isabelle/file/edd50ec8d471/src/HOL/Tools/Nitpick/nitpick.ML) 
. Now, Kodkodi doesn't seem to be available from the download page  
anymore, but you can get it from my home page or steal it from NFS.  
Version 1.2.16 works fine. (I really need to update the above message!)

>  A grep for Kodkod over the sources did not look very
> promising.

It should have caught the above message, though. ;)

Cheers,

Jasmin

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20120104/7f9e3588/attachment-0002.html>


More information about the isabelle-dev mailing list