| Mon, 19 Apr 2010 10:45:08 +0200 |
blanchet |
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
|
file |
diff |
annotate
|
| Mon, 19 Apr 2010 10:15:02 +0200 |
blanchet |
set SPASS option on the command-line, so that it doesn't vanish when moving to TPTP format
|
file |
diff |
annotate
|
| Sat, 17 Apr 2010 10:42:09 +0200 |
blanchet |
added missing \n in output
|
file |
diff |
annotate
|
| Fri, 16 Apr 2010 20:50:50 +0200 |
blanchet |
added timestamp to proof
|
file |
diff |
annotate
|
| Fri, 16 Apr 2010 14:48:34 +0200 |
blanchet |
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
|
file |
diff |
annotate
|
| Thu, 15 Apr 2010 13:49:46 +0200 |
blanchet |
make Sledgehammer's output more debugging friendly
|
file |
diff |
annotate
|
| Wed, 14 Apr 2010 21:22:13 +0200 |
blanchet |
added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture
|
file |
diff |
annotate
|
| Wed, 14 Apr 2010 18:23:51 +0200 |
blanchet |
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
|
file |
diff |
annotate
|
| Mon, 29 Mar 2010 19:49:57 +0200 |
blanchet |
added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
|
file |
diff |
annotate
|
| Mon, 29 Mar 2010 12:21:51 +0200 |
blanchet |
made "theory_const" a Sledgehammer option;
|
file |
diff |
annotate
|
| Mon, 29 Mar 2010 12:01:00 +0200 |
blanchet |
added "respect_no_atp" and "convergence" options to Sledgehammer;
|
file |
diff |
annotate
|
| Sun, 28 Mar 2010 16:59:06 +0200 |
wenzelm |
static defaults for configuration options;
|
file |
diff |
annotate
|
| Wed, 24 Mar 2010 14:49:32 +0100 |
blanchet |
added support for Sledgehammer parameters;
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 10:25:07 +0100 |
blanchet |
start work on direct proof reconstruction for Sledgehammer
|
file |
diff |
annotate
|
| Fri, 19 Mar 2010 16:04:15 +0100 |
blanchet |
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
|
file |
diff |
annotate
|
| Fri, 19 Mar 2010 15:33:18 +0100 |
blanchet |
move all ATP setup code into ATP_Wrapper
|
file |
diff |
annotate
|
| Fri, 19 Mar 2010 13:02:18 +0100 |
blanchet |
more Sledgehammer refactoring
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 19:26:05 +0100 |
blanchet |
renamed Sledgehammer structures
|
file |
diff |
annotate
|
| Thu, 04 Mar 2010 22:48:16 +0100 |
wenzelm |
basic simplification of external_prover signature;
|
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, 29 Oct 2009 16:59:12 +0100 |
wenzelm |
modernized some structure names;
|
file |
diff |
annotate
|
| Tue, 27 Oct 2009 18:00:50 +0100 |
boehmes |
measure runtime of ATPs only if requested
|
file |
diff |
annotate
|
| Fri, 23 Oct 2009 14:22:36 +0200 |
boehmes |
ignore error messages produced by ATPs
|
file |
diff |
annotate
|
| Thu, 15 Oct 2009 17:49:30 +0200 |
wenzelm |
natural argument order for prover;
|
file |
diff |
annotate
|
| Thu, 15 Oct 2009 15:53:33 +0200 |
wenzelm |
clarified File.platform_path vs. File.shell_path;
|
file |
diff |
annotate
|
| Thu, 15 Oct 2009 12:23:24 +0200 |
wenzelm |
misc tuning and recovery of Isabelle coding style;
|
file |
diff |
annotate
|
| Thu, 15 Oct 2009 11:49:27 +0200 |
wenzelm |
eliminated extraneous wrapping of public records;
|
file |
diff |
annotate
|
| Wed, 14 Oct 2009 23:44:37 +0200 |
wenzelm |
modernized structure names;
|
file |
diff |
annotate
|
| Sun, 04 Oct 2009 12:59:22 +0200 |
boehmes |
recovered support for Spass: re-enabled writing problems in DFG format
|
file |
diff |
annotate
|
| Sat, 03 Oct 2009 12:05:40 +0200 |
boehmes |
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 16:24:36 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Thu, 17 Sep 2009 11:57:36 +0200 |
boehmes |
undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time";
|
file |
diff |
annotate
|
| Tue, 15 Sep 2009 15:29:11 +0200 |
boehmes |
added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling);
|
file |
diff |
annotate
|
| Thu, 03 Sep 2009 17:55:31 +0200 |
boehmes |
added runtime information to sledgehammer
|
file |
diff |
annotate
|
| Mon, 31 Aug 2009 15:29:26 +0200 |
boehmes |
sledgehammer's temporary files are removed properly (even in case of an exception occurs)
|
file |
diff |
annotate
|
| Sat, 29 Aug 2009 21:57:06 +0200 |
boehmes |
propagate theorem names, in addition to generated return message
|
file |
diff |
annotate
|
| Tue, 04 Aug 2009 19:20:24 +0200 |
wenzelm |
src/HOL/Tools/ATP_Manager as separate component, with (almost) everything in one place;
|
file |
diff |
annotate
| base
|