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