src/HOL/Tools/Nitpick/kodkod.ML
2016-10-18 wenzelm 2016-10-18 clarified modules;
2016-04-02 wenzelm 2016-04-02 prefer infix operations;
2016-03-07 wenzelm 2016-03-07 File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output; clarified treatment of whitespace in some bash scripts;
2014-03-03 blanchet 2014-03-03 tuned code
2014-03-03 blanchet 2014-03-03 removed nonstandard models from Nitpick
2013-12-19 blanchet 2013-12-19 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
2013-08-20 blanchet 2013-08-20 tuning
2012-12-12 blanchet 2012-12-12 use modern SAT solvers with modern Kodkod versions
2012-12-12 blanchet 2012-12-12 got rid of support for Kodkodi < 1.2.14
2012-08-30 blanchet 2012-08-30 updated Java-related error message
2012-04-16 wenzelm 2012-04-16 more precise handling of java failure, due to missing ISABELLE_JDK_HOME;
2011-07-16 wenzelm 2011-07-16 moved bash operations to Isabelle_System (cf. Scala version);
2011-05-31 blanchet 2011-05-31 first step in sharing more code between ATP and Metis translation
2011-02-21 blanchet 2011-02-21 tweaked Nitpick based on C++ memory model example
2010-11-27 wenzelm 2010-11-27 more explicit Isabelle_System operations;
2010-11-20 wenzelm 2010-11-20 renamed raw "explode" function to "raw_explode" to emphasize its meaning;
2010-11-07 blanchet 2010-11-07 removed explicit "Interrupt" handling for conformity with async model -- unfortunately the user loses the information about how many scopes were checked, but this needs to be retought with the new interface anyway
2010-11-05 wenzelm 2010-11-05 explicit indication of some remaining violations of the Isabelle/ML interrupt model;
2010-10-29 blanchet 2010-10-29 no need for setting up the kodkodi environment since Kodkodi 1.2.9
2010-09-16 blanchet 2010-09-16 tuning
2010-09-11 blanchet 2010-09-11 tuning
2010-08-18 blanchet 2010-08-18 gracefully handle the case where the JVM is too old in Nitpick
2010-08-05 blanchet 2010-08-05 rename internal functions
2010-08-03 blanchet 2010-08-03 tuning
2010-08-01 blanchet 2010-08-01 fix bug with Kodkodi < 1.2.14
2010-08-01 blanchet 2010-08-01 added manual symmetry breaking for datatypes
2010-07-27 blanchet 2010-07-27 complete renaming of "Sledgehammer_TPTP_Format" to "ATP_Problem"
2010-05-14 blanchet 2010-05-14 recognize new Kodkod error message syntax
2010-04-25 blanchet 2010-04-25 remove "show_skolems" option and change style of record declarations
2010-04-24 blanchet 2010-04-24 remove type annotations as comments; Nitpick is now 1136 lines shorter
2010-04-23 blanchet 2010-04-23 reuse timestamp function
2010-03-17 blanchet 2010-03-17 added one-entry cache around Kodkod invocation
2010-03-11 blanchet 2010-03-11 moved some Nitpick code around
2010-03-10 blanchet 2010-03-10 show nice error message in Nitpick when "java" is not available
2010-03-10 blanchet 2010-03-10 fixed soundness bug in Nitpick
2010-02-24 blanchet 2010-02-24 cosmetics
2010-02-23 blanchet 2010-02-23 distinguish between Kodkodi warnings and errors in Nitpick; will be needed starting with version 1.2.9 of Kodkodi
2010-02-23 blanchet 2010-02-23 catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
2010-02-22 blanchet 2010-02-22 fixed a few bugs in Nitpick and removed unreferenced variables
2010-02-17 blanchet 2010-02-17 don't destroy "Suc" in Nitpick and fix logic of Kodkod filtering (accidentally flipped in previous change)
2010-02-17 blanchet 2010-02-17 added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
2010-02-09 blanchet 2010-02-09 merged (manual for "nitpick_hol.ML" and "kodkod.ML")
2010-02-05 blanchet 2010-02-05 proper quoting of file paths when invoking Kodkodi from Nitpick
2010-02-06 wenzelm 2010-02-06 proper treatment of paths passed to the shell -- to allow spaces in file names as usual;
2010-02-06 wenzelm 2010-02-06 renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
2010-02-04 blanchet 2010-02-04 four changes to Nitpick: 1. avoid writing absolute paths in Kodkodi files for input/output files of external SAT solvers (e.g. MiniSat), to dodge Cygwin problems 2. do eta-contraction in the monotonicity check 3. improved quantifier massaging algorithms using ideas from Paradox 4. repaired "check_potential" and "check_genuine"
2010-02-02 blanchet 2010-02-02 added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
2010-01-20 blanchet 2010-01-20 some work on Nitpick's support for quotient types; quotient types are not yet in Isabelle, so for now I hardcoded "IntEx.my_int"
2009-12-17 blanchet 2009-12-17 added support for binary nat/int representation to Nitpick
2009-12-14 blanchet 2009-12-14 get rid of polymorphic equality in Nitpick's code + a few minor cleanups
2009-12-04 blanchet 2009-12-04 fixed paths in Nitpick's ML file headers
2009-11-17 blanchet 2009-11-17 invoke Kodkodi from Nitpick using new $KODKOD/bin/kodkodi script; this requires downloading Kodkodi 1.2.4, or writing a "kodkodi" script that invokes "java de.tum.in.isabelle.Kodkodi.Kodkodi $@"
2009-10-29 blanchet 2009-10-29 try very hard to remove temporary files generated by Nitpick in case of interruption
2009-10-27 blanchet 2009-10-27 added friendly error message when Kodkodi is not available
2009-10-27 blanchet 2009-10-27 internal renaming in Nitpick and fixed Kodkodi invokation on Linux; renamed Nitpick's ML structures from NitpickXxx to Nitpick_Xxx and added KODKODI_JAVA_LIBRARY_PATH to LD_LIBRARY_PATH before invoking Kodkodi
2009-10-26 blanchet 2009-10-26 made Nitpick aware of the KODKODI_JAVA_LIBRARY_PATH, for detecting and properly invoking JNI-based SAT solvers
2009-10-22 blanchet 2009-10-22 added Nitpick's theory and ML files to Isabelle/HOL; the examples and the documentation are on their way.