| Wed, 23 Nov 2016 20:55:58 +0100 |
blanchet |
made MaSh faster and less likely to hang seemingly forever
|
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:48:34 +0200 |
blanchet |
speed up MaSh duplicate check
|
file |
diff |
annotate
|
| Sun, 04 Oct 2015 17:41:52 +0200 |
blanchet |
sped up MaSh nickname generation
|
file |
diff |
annotate
|
| Sun, 05 Jul 2015 22:32:14 +0200 |
wenzelm |
more explicit use of context and elimination of Thm.theory_of_thm, although unclear (and untested?) situations remain;
|
file |
diff |
annotate
|
| Fri, 03 Jul 2015 16:19:45 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Fri, 03 Jul 2015 14:51:43 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 03 Jul 2015 14:32:55 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
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
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
reverted 83a8570b44bc, which was a misunderstanding
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 13:56:27 +0200 |
blanchet |
the kind is now always the empty string -- can no longer distinguish between user theorems and package theorems in a semi-reliable way
|
file |
diff |
annotate
|
| Wed, 09 Jul 2014 11:35:52 +0200 |
blanchet |
tuned terminology
|
file |
diff |
annotate
|
| Tue, 01 Jul 2014 16:47:10 +0200 |
blanchet |
clean up MaSh export a bit
|
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:18:30 +0200 |
blanchet |
use right theory name for theorems in evaluation driver
|
file |
diff |
annotate
|
| Fri, 27 Jun 2014 17:05:22 +0200 |
blanchet |
killed dead code
|
file |
diff |
annotate
|
| Thu, 26 Jun 2014 20:49:34 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Thu, 26 Jun 2014 13:33:02 +0200 |
blanchet |
avoid parallelism, since it confuses the global state and leads to cheating (with 'sml_xxx' engines)
|
file |
diff |
annotate
|
| Thu, 26 Jun 2014 13:32:56 +0200 |
blanchet |
generate right dependencies in MaSh driver
|
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
|
| Tue, 24 Jun 2014 08:20:00 +0200 |
blanchet |
changed order of facts so that 'name_tabs' has the same order everywhere (which affects unaliasing)
|
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
|
| Fri, 30 May 2014 12:27:51 +0200 |
blanchet |
more work on exporter
|
file |
diff |
annotate
|
| Fri, 30 May 2014 12:27:51 +0200 |
blanchet |
got rid of 'linearize' option
|
file |
diff |
annotate
|
| Fri, 30 May 2014 12:27:51 +0200 |
blanchet |
extend exporter with new versions of MaSh
|
file |
diff |
annotate
|
| Fri, 23 May 2014 14:12:21 +0200 |
blanchet |
fixed semantics of 'linearize'
|
file |
diff |
annotate
|
| Thu, 22 May 2014 04:12:06 +0200 |
blanchet |
reverted '|' features in MaSh -- these sounded like a good idea but never really worked
|
file |
diff |
annotate
|
| Mon, 19 May 2014 23:43:53 +0200 |
blanchet |
store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 16:10:39 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 10:23:32 +0100 |
blanchet |
renamed ML file
|
file |
diff |
annotate
|
| Mon, 09 Dec 2013 04:03:30 +0100 |
blanchet |
generate problems with type classes
|
file |
diff |
annotate
|
| Fri, 18 Oct 2013 00:05:31 +0200 |
blanchet |
make sure add: doesn't add duplicates, and works for [no_atp] facts
|
file |
diff |
annotate
|
| Tue, 15 Oct 2013 23:00:46 +0200 |
blanchet |
tweaked signature
|
file |
diff |
annotate
|
| Thu, 10 Oct 2013 01:17:37 +0200 |
blanchet |
simplify fudge factor code
|
file |
diff |
annotate
|
| Wed, 09 Oct 2013 15:39:34 +0200 |
blanchet |
use same relevance filter for ATP and SMT solvers -- attempting to filter out certain ground instances of polymorphic symbols like + and 0 has unexpected side-effects that lead to incompletenesses (relevant facts not being selected)
|
file |
diff |
annotate
|
| Wed, 09 Oct 2013 09:47:59 +0200 |
blanchet |
optimized built-in const check
|
file |
diff |
annotate
|
| Fri, 23 Aug 2013 16:51:53 +0200 |
blanchet |
repaired num_extra_feature_facts + tuning
|
file |
diff |
annotate
|
| Thu, 22 Aug 2013 12:16:56 +0200 |
blanchet |
take chained and proximate facts into consideration when computing MaSh features
|
file |
diff |
annotate
|
| Thu, 22 Aug 2013 12:12:52 +0200 |
blanchet |
pour extra features from proximate facts into goal, in exporter
|
file |
diff |
annotate
|
| Wed, 21 Aug 2013 14:54:25 +0200 |
blanchet |
weight MaSh constants by frequency
|
file |
diff |
annotate
|
| Wed, 21 Aug 2013 09:25:40 +0200 |
blanchet |
only generate feature weights for queries -- they're not used elsewhere
|
file |
diff |
annotate
|
| Wed, 21 Aug 2013 09:25:40 +0200 |
blanchet |
generate max suggestions in MaSh export driver
|
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
|
| Tue, 19 Feb 2013 13:21:49 +0100 |
blanchet |
provide two modes for MaSh driver: linearized or real visibility
|
file |
diff |
annotate
|
| Mon, 18 Feb 2013 11:33:43 +0100 |
blanchet |
tuned code: factored out parent computation
|
file |
diff |
annotate
|
| Fri, 15 Feb 2013 09:17:20 +0100 |
blanchet |
tuned code
|
file |
diff |
annotate
|
| Fri, 08 Feb 2013 16:41:04 +0100 |
blanchet |
distinguish one more kind of proofs
|
file |
diff |
annotate
|
| Fri, 08 Feb 2013 15:38:33 +0100 |
blanchet |
added markers in proofs identifying origin of proofs, in eval driver
|
file |
diff |
annotate
|
| Tue, 05 Feb 2013 17:19:13 +0100 |
blanchet |
removed spurious trimming
|
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 19:20:56 +0100 |
blanchet |
added step to skip some queries
|
file |
diff |
annotate
|
| Wed, 16 Jan 2013 12:55:29 +0100 |
blanchet |
graceful failure
|
file |
diff |
annotate
|
| Wed, 16 Jan 2013 12:46:11 +0100 |
blanchet |
honor fact range for MePo as well
|
file |
diff |
annotate
|
| Sun, 13 Jan 2013 12:28:20 +0100 |
blanchet |
don't generate queries with empty dependency list
|
file |
diff |
annotate
|
| Fri, 11 Jan 2013 16:30:56 +0100 |
blanchet |
fixed escaping for MeSh encoder
|
file |
diff |
annotate
|