| Tue, 29 Sep 2020 13:20:27 +0200 |
wenzelm |
more reactive kodkod execution: avoid confusion about timeout/deadline;
|
file |
diff |
annotate
|
| Tue, 29 Sep 2020 12:01:30 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 29 Sep 2020 11:59:59 +0200 |
wenzelm |
obsolete --- Java is always present via component;
|
file |
diff |
annotate
|
| Tue, 29 Sep 2020 11:35:21 +0200 |
wenzelm |
obsolete --- KODKODI is always present via component;
|
file |
diff |
annotate
|
| Tue, 25 Aug 2020 14:54:41 +0200 |
wenzelm |
removed pointless version checks: Isabelle component integration does the job already;
|
file |
diff |
annotate
|
| Mon, 24 Aug 2020 22:30:34 +0200 |
wenzelm |
suppress odd warning for context.exit();
|
file |
diff |
annotate
|
| Mon, 24 Aug 2020 21:47:21 +0200 |
wenzelm |
more explicit treatment of interrupt;
|
file |
diff |
annotate
|
| Mon, 24 Aug 2020 17:58:04 +0200 |
wenzelm |
more flexible default for max_threads;
|
file |
diff |
annotate
|
| Sat, 22 Aug 2020 23:22:25 +0200 |
wenzelm |
invoke Nitpick/Kodkod via Isabelle/Scala (instead of external process);
|
file |
diff |
annotate
|
| Sat, 22 Aug 2020 14:56:33 +0200 |
wenzelm |
proper treatment of timeout: <= 0 means already timed out, but for $KODKODI/bin/kodkodi it would mean NO timeout;
|
file |
diff |
annotate
|
| 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
|