src/HOL/Tools/Nitpick/kodkod.ML
Sat, 28 Mar 2020 22:18:28 +0100 wenzelm more robust, notably wrt. interrupts;
Thu, 01 Feb 2018 15:12:57 +0100 wenzelm tuned signature: more operations;
Tue, 18 Oct 2016 16:03:30 +0200 wenzelm clarified modules;
Sat, 02 Apr 2016 23:29:05 +0200 wenzelm prefer infix operations;
Mon, 07 Mar 2016 21:09:28 +0100 wenzelm File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output;
Mon, 03 Mar 2014 22:33:22 +0100 blanchet tuned code
Mon, 03 Mar 2014 22:33:22 +0100 blanchet removed nonstandard models from Nitpick
Thu, 19 Dec 2013 13:43:21 +0100 blanchet made timeouts in Sledgehammer not be 'option's -- simplified lots of code
Tue, 20 Aug 2013 11:42:50 +0200 blanchet tuning
Wed, 12 Dec 2012 11:56:07 +0100 blanchet use modern SAT solvers with modern Kodkod versions
Wed, 12 Dec 2012 11:18:06 +0100 blanchet got rid of support for Kodkodi < 1.2.14
Thu, 30 Aug 2012 09:47:46 +0200 blanchet updated Java-related error message
Mon, 16 Apr 2012 15:09:47 +0200 wenzelm more precise handling of java failure, due to missing ISABELLE_JDK_HOME;
Sat, 16 Jul 2011 20:52:41 +0200 wenzelm moved bash operations to Isabelle_System (cf. Scala version);
Tue, 31 May 2011 16:38:36 +0200 blanchet first step in sharing more code between ATP and Metis translation
Mon, 21 Feb 2011 11:50:31 +0100 blanchet tweaked Nitpick based on C++ memory model example
Sat, 27 Nov 2010 15:28:00 +0100 wenzelm more explicit Isabelle_System operations;
Sat, 20 Nov 2010 00:53:26 +0100 wenzelm renamed raw "explode" function to "raw_explode" to emphasize its meaning;
Sun, 07 Nov 2010 13:29:59 +0100 blanchet 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
Fri, 05 Nov 2010 19:47:20 +0100 wenzelm explicit indication of some remaining violations of the Isabelle/ML interrupt model;
Fri, 29 Oct 2010 12:49:05 +0200 blanchet no need for setting up the kodkodi environment since Kodkodi 1.2.9
Thu, 16 Sep 2010 14:24:03 +0200 blanchet tuning
Sat, 11 Sep 2010 12:31:05 +0200 blanchet tuning
Wed, 18 Aug 2010 10:42:04 +0200 blanchet gracefully handle the case where the JVM is too old in Nitpick
Thu, 05 Aug 2010 09:49:46 +0200 blanchet rename internal functions
Tue, 03 Aug 2010 21:37:12 +0200 blanchet tuning
Sun, 01 Aug 2010 18:57:49 +0200 blanchet fix bug with Kodkodi < 1.2.14
Sun, 01 Aug 2010 15:51:25 +0200 blanchet added manual symmetry breaking for datatypes
Tue, 27 Jul 2010 17:43:11 +0200 blanchet complete renaming of "Sledgehammer_TPTP_Format" to "ATP_Problem"
Fri, 14 May 2010 15:02:38 +0200 blanchet recognize new Kodkod error message syntax
Sun, 25 Apr 2010 00:25:44 +0200 blanchet remove "show_skolems" option and change style of record declarations
Sat, 24 Apr 2010 16:33:01 +0200 blanchet remove type annotations as comments;
Fri, 23 Apr 2010 19:26:39 +0200 blanchet reuse timestamp function
Wed, 17 Mar 2010 17:23:45 +0100 blanchet added one-entry cache around Kodkod invocation
Thu, 11 Mar 2010 17:48:07 +0100 blanchet moved some Nitpick code around
Wed, 10 Mar 2010 15:06:40 +0100 blanchet show nice error message in Nitpick when "java" is not available
Wed, 10 Mar 2010 14:21:01 +0100 blanchet fixed soundness bug in Nitpick
Wed, 24 Feb 2010 09:18:31 +0100 blanchet cosmetics
Tue, 23 Feb 2010 15:56:13 +0100 blanchet distinguish between Kodkodi warnings and errors in Nitpick;
Tue, 23 Feb 2010 10:02:14 +0100 blanchet catch IO errors in Nitpick's "kodkodi" invocation + shorten execution time of "Manual_Nits" example
Mon, 22 Feb 2010 11:57:33 +0100 blanchet fixed a few bugs in Nitpick and removed unreferenced variables
Wed, 17 Feb 2010 13:38:02 +0100 blanchet don't destroy "Suc" in Nitpick and fix logic of Kodkod filtering (accidentally flipped in previous change)
Wed, 17 Feb 2010 12:14:08 +0100 blanchet added yet another hint to Nitpick's output, this time warning about problems for which nothing was effectively tested
Tue, 09 Feb 2010 17:06:05 +0100 blanchet merged (manual for "nitpick_hol.ML" and "kodkod.ML")
Fri, 05 Feb 2010 11:24:53 +0100 blanchet proper quoting of file paths when invoking Kodkodi from Nitpick
Sat, 06 Feb 2010 15:51:22 +0100 wenzelm proper treatment of paths passed to the shell -- to allow spaces in file names as usual;
Sat, 06 Feb 2010 14:50:55 +0100 wenzelm renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
Thu, 04 Feb 2010 13:36:52 +0100 blanchet four changes to Nitpick:
Tue, 02 Feb 2010 11:38:38 +0100 blanchet added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
Wed, 20 Jan 2010 10:38:06 +0100 blanchet some work on Nitpick's support for quotient types;
Thu, 17 Dec 2009 15:22:11 +0100 blanchet added support for binary nat/int representation to Nitpick
Mon, 14 Dec 2009 12:30:26 +0100 blanchet get rid of polymorphic equality in Nitpick's code + a few minor cleanups
Fri, 04 Dec 2009 17:19:59 +0100 blanchet fixed paths in Nitpick's ML file headers
Tue, 17 Nov 2009 13:50:46 +0100 blanchet invoke Kodkodi from Nitpick using new $KODKOD/bin/kodkodi script;
Thu, 29 Oct 2009 22:31:30 +0100 blanchet try very hard to remove temporary files generated by Nitpick in case of interruption
Tue, 27 Oct 2009 15:55:36 +0100 blanchet added friendly error message when Kodkodi is not available
Tue, 27 Oct 2009 14:40:24 +0100 blanchet internal renaming in Nitpick and fixed Kodkodi invokation on Linux;
Mon, 26 Oct 2009 18:52:16 +0100 blanchet made Nitpick aware of the KODKODI_JAVA_LIBRARY_PATH, for detecting and properly invoking JNI-based SAT solvers
Thu, 22 Oct 2009 14:51:47 +0200 blanchet added Nitpick's theory and ML files to Isabelle/HOL;
less more (0) tip