| Fri, 24 Jun 2022 23:38:41 +0200 |
wenzelm |
clarified signature: File.read_lines is based on scalable Bytes.T;
|
file |
diff |
annotate
|
| Fri, 24 Jun 2022 10:55:23 +0200 |
wenzelm |
prefer scalable Bytes.T;
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
compile HOL-TPTP
|
file |
diff |
annotate
|
| Tue, 11 Jan 2022 22:07:04 +0100 |
desharna |
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
|
file |
diff |
annotate
|
| Wed, 14 Jul 2021 15:18:11 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 09 Jul 2021 17:58:17 +0200 |
desharna |
fixed HOL-TPTP following f58108b7a60c
|
file |
diff |
annotate
|
| Sun, 14 Aug 2016 12:26:09 +0200 |
blanchet |
killed final stops in Sledgehammer and friends
|
file |
diff |
annotate
|
| Sun, 04 Oct 2015 17:41:52 +0200 |
blanchet |
sped up MaSh nickname generation
|
file |
diff |
annotate
|
| Fri, 03 Jul 2015 16:19:45 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| Thu, 06 Nov 2014 15:42:34 +0100 |
wenzelm |
proper Keyword.keywords (cf. 82a71046dce8);
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 13:56:27 +0200 |
blanchet |
added missing 'transpose'
|
file |
diff |
annotate
|
| Thu, 28 Aug 2014 00:40:38 +0200 |
blanchet |
renamed new SMT module from 'SMT2' to 'SMT'
|
file |
diff |
annotate
|
| Tue, 01 Jul 2014 16:47:10 +0200 |
blanchet |
clean up MaSh evaluation driver
|
file |
diff |
annotate
|
| Sun, 29 Jun 2014 18:30:24 +0200 |
blanchet |
use SMT2
|
file |
diff |
annotate
|
| Sun, 29 Jun 2014 18:28:27 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Sun, 29 Jun 2014 18:28:27 +0200 |
blanchet |
killed Python version of MaSh, now that the SML version works adequately
|
file |
diff |
annotate
|
| Fri, 27 Jun 2014 17:05:22 +0200 |
blanchet |
killed dead code
|
file |
diff |
annotate
|
| Tue, 24 Jun 2014 15:08:19 +0200 |
blanchet |
optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct)
|
file |
diff |
annotate
|
| Mon, 02 Jun 2014 11:59:50 +0200 |
blanchet |
add option to keep duplicates, for more precise evaluation of relevance filters
|
file |
diff |
annotate
|
| Fri, 30 May 2014 12:27:51 +0200 |
blanchet |
added another way of invoking Python code, for experiments
|
file |
diff |
annotate
|
| Wed, 28 May 2014 17:42:36 +0200 |
blanchet |
more generous max number of suggestions, for more safety
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 16:10:39 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 12:30:54 +0100 |
blanchet |
refactor large ML file
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 10:23:32 +0100 |
blanchet |
renamed ML file
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 10:23:32 +0100 |
blanchet |
tuned ML file name
|
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
|
| Thu, 17 Oct 2013 20:49:19 +0200 |
blanchet |
generate a comment storing the goal nickname in "learn_prover"
|
file |
diff |
annotate
|
| Sun, 29 Sep 2013 12:21:11 +0200 |
wenzelm |
made SML/NJ happy (NB: toplevel ML environment is unmanaged);
|
file |
diff |
annotate
|
| Thu, 22 Aug 2013 12:12:51 +0200 |
blanchet |
cleanup old duplicated functionality
|
file |
diff |
annotate
|
| Tue, 28 May 2013 08:52:41 +0200 |
blanchet |
redid rac7830871177 to avoid duplicate fixed variable (e.g. lemma "P (a::nat)" proof - have "!!a::int. Q a" sledgehammer [e])
|
file |
diff |
annotate
|
| Fri, 24 May 2013 16:43:37 +0200 |
blanchet |
improved handling of free variables' types in Isar proofs
|
file |
diff |
annotate
|
| Thu, 16 May 2013 13:34:13 +0200 |
blanchet |
tuning -- renamed '_from_' to '_of_' in Sledgehammer
|
file |
diff |
annotate
|
| Wed, 20 Feb 2013 13:04:03 +0100 |
blanchet |
honor linearization option also in the evaluation driver
|
file |
diff |
annotate
|
| Tue, 19 Feb 2013 13:21:49 +0100 |
blanchet |
provide two modes for MaSh driver: linearized or real visibility
|
file |
diff |
annotate
|
| Fri, 15 Feb 2013 09:17:20 +0100 |
blanchet |
tuned code
|
file |
diff |
annotate
|
| Fri, 15 Feb 2013 09:17:20 +0100 |
blanchet |
more MaSh tracing
|
file |
diff |
annotate
|
| Thu, 07 Feb 2013 14:05:33 +0100 |
blanchet |
more robustness w.r.t. 0
|
file |
diff |
annotate
|
| Thu, 31 Jan 2013 18:04:19 +0100 |
blanchet |
compile
|
file |
diff |
annotate
|
| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
more precise output of selected facts
|
file |
diff |
annotate
|
| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
distinguish raw and non-raw facts, using raw for 10 000s of facts and non-raw after selection of some hundreds
|
file |
diff |
annotate
|
| Fri, 18 Jan 2013 00:18:11 +0100 |
blanchet |
optimization -- evaluate conversion to table only once
|
file |
diff |
annotate
|
| Thu, 17 Jan 2013 23:29:22 +0100 |
blanchet |
use correct weights in MeSh driver
|
file |
diff |
annotate
|
| Thu, 17 Jan 2013 23:29:17 +0100 |
blanchet |
use precomputed MaSh/MePo data whenever available
|
file |
diff |
annotate
|
| Thu, 17 Jan 2013 18:53:13 +0100 |
blanchet |
provide a means to skip a method
|
file |
diff |
annotate
|
| Thu, 17 Jan 2013 18:43:59 +0100 |
blanchet |
evaluate more cases (cf. paper)
|
file |
diff |
annotate
|
| Fri, 11 Jan 2013 16:30:56 +0100 |
blanchet |
start using MaSh hints
|
file |
diff |
annotate
|
| Fri, 11 Jan 2013 16:30:56 +0100 |
blanchet |
always compare theorem using the same, weaker function
|
file |
diff |
annotate
|
| Thu, 10 Jan 2013 23:34:19 +0100 |
blanchet |
export MeSh data as well
|
file |
diff |
annotate
|
| Tue, 08 Jan 2013 13:16:39 +0100 |
blanchet |
tuned output
|
file |
diff |
annotate
|
| Sun, 06 Jan 2013 17:38:29 +0100 |
blanchet |
also generate queries for goals with too many Isar dependencies
|
file |
diff |
annotate
|
| Fri, 04 Jan 2013 21:56:20 +0100 |
blanchet |
refined class handling, to prevent cycles in fact graph
|
file |
diff |
annotate
|
| Fri, 28 Dec 2012 23:31:51 +0100 |
blanchet |
tuned ML function name
|
file |
diff |
annotate
|
| Thu, 27 Dec 2012 16:49:12 +0100 |
blanchet |
improved thm order hack, in case the default names are overridden
|
file |
diff |
annotate
|
| Thu, 27 Dec 2012 10:21:21 +0100 |
blanchet |
fixed total
|
file |
diff |
annotate
|
| Tue, 18 Dec 2012 02:19:14 +0100 |
blanchet |
avoid references altogether
|
file |
diff |
annotate
|
| Tue, 18 Dec 2012 00:17:37 +0100 |
blanchet |
no need for tracing
|
file |
diff |
annotate
|
| Mon, 17 Dec 2012 22:06:28 +0100 |
blanchet |
synchronize access to shared reference and print proper total
|
file |
diff |
annotate
|
| Sun, 16 Dec 2012 14:19:08 +0100 |
blanchet |
escape nicknames
|
file |
diff |
annotate
|
| Sun, 16 Dec 2012 12:07:56 +0100 |
blanchet |
generate proper nicks also for instantiated induction rules
|
file |
diff |
annotate
|
| Sat, 15 Dec 2012 21:34:32 +0100 |
blanchet |
MaSh exporter can now export subsets of the facts, as consecutive ranges
|
file |
diff |
annotate
|
| Sat, 15 Dec 2012 19:57:12 +0100 |
blanchet |
thread no timeout properly
|
file |
diff |
annotate
|
| Sat, 15 Dec 2012 18:48:58 +0100 |
blanchet |
proper escaping in file name
|
file |
diff |
annotate
|
| Sat, 15 Dec 2012 18:26:37 +0100 |
blanchet |
encode lemma name in file name
|
file |
diff |
annotate
|
| Thu, 13 Dec 2012 22:49:07 +0100 |
blanchet |
use MaSh nicknames in ATP problem files to facilitate gathering of statistics
|
file |
diff |
annotate
|
| Wed, 12 Dec 2012 02:47:45 +0100 |
blanchet |
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
|
file |
diff |
annotate
|
| Wed, 12 Dec 2012 00:14:58 +0100 |
blanchet |
better name for SMT solver files
|
file |
diff |
annotate
|
| Mon, 10 Dec 2012 13:33:06 +0100 |
blanchet |
changed capitalization of MeSh filter
|
file |
diff |
annotate
|
| Mon, 10 Dec 2012 13:02:56 +0100 |
blanchet |
(re)introduce (even more) aggressive parallelism, for the benefit of those users with dozens of CPU cores
|
file |
diff |
annotate
|
| Mon, 10 Dec 2012 10:29:52 +0100 |
blanchet |
have MaSh evaluator keep all raw problem/solution files in a directory
|
file |
diff |
annotate
|
| Sat, 08 Dec 2012 21:54:28 +0100 |
blanchet |
don't blacklist "case" theorems -- this causes problems in MaSh later
|
file |
diff |
annotate
|
| Sat, 08 Dec 2012 00:48:51 +0100 |
blanchet |
don't have MaSh pretend it knows facts it doesn't know
|
file |
diff |
annotate
|
| Sat, 08 Dec 2012 00:48:51 +0100 |
blanchet |
reverted parallel map idea -- appears to make success rate of ATPs less stable (might even lead to bias in favor of MePo)
|
file |
diff |
annotate
|
| Sat, 08 Dec 2012 00:48:50 +0100 |
blanchet |
store evaluation output in a file
|
file |
diff |
annotate
|
| Sat, 08 Dec 2012 00:48:50 +0100 |
blanchet |
use parallel map
|
file |
diff |
annotate
|
| Thu, 06 Dec 2012 17:48:04 +0100 |
blanchet |
use proper entry point for MaSh in test driver
|
file |
diff |
annotate
|
| Wed, 05 Dec 2012 13:25:06 +0100 |
blanchet |
take proximity into account for MaSh + fix a debilitating bug in feature generation
|
file |
diff |
annotate
|
| Tue, 04 Dec 2012 23:50:36 +0100 |
blanchet |
rationalized MaSh evaluation harness
|
file |
diff |
annotate
|
| Tue, 31 Jul 2012 14:42:03 +0200 |
wenzelm |
made SML/NJ happy;
|
file |
diff |
annotate
|
| Thu, 26 Jul 2012 10:48:03 +0200 |
blanchet |
repaired accessibility chains generated by MaSh exporter + tuned one function out
|
file |
diff |
annotate
|
| Mon, 23 Jul 2012 15:32:30 +0200 |
blanchet |
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
|
file |
diff |
annotate
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
honor suggested MaSh weights
|
file |
diff |
annotate
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
relearn ATP proofs
|
file |
diff |
annotate
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
|
file |
diff |
annotate
|
| Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
added "learn_from_atp" command to MaSh, for patient users
|
file |
diff |
annotate
|
| Fri, 20 Jul 2012 22:19:45 +0200 |
blanchet |
renamed ML structures
|
file |
diff |
annotate
|
| Fri, 20 Jul 2012 22:19:45 +0200 |
blanchet |
renamed "iter" fact filter to "MePo" (Meng--Paulson)
|
file |
diff |
annotate
|
| Fri, 20 Jul 2012 22:19:45 +0200 |
blanchet |
handle local facts smoothly in MaSh
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:05 +0200 |
blanchet |
repair MaSh exporter
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
speed up tautology/metaness check
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
learn from minimized ATP proofs
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case)
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
more consolidation of MaSh code
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
drastic overhaul of MaSh data structures + fixed a few performance issues
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
fixed order of accessibles + other tweaks to MaSh
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
mesh facts by taking into consideration whether a fact is known to MeSh
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
implemented meshing of Iter and MaSh results
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
implemented MaSh QUERY operation
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
cleaner handling of metacharacters + freshness of one-off facts
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
improved MaSh string escaping and make more operations string-based
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
tweak output
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
centrally construct expensive data structures
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
more work on MaSh
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
renamed Sledgehammer options
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
more code rationalization in relevance filter
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
systematize lazy names in relevance filter
|
file |
diff |
annotate
|
| Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
renaming
|
file |
diff |
annotate
| base
|