| 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
|
| Fri, 11 Jan 2013 16:30:56 +0100 |
blanchet |
start using MaSh hints
|
file |
diff |
annotate
|
| Thu, 10 Jan 2013 23:34:19 +0100 |
blanchet |
export MeSh data as well
|
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
|
| Thu, 27 Dec 2012 16:49:12 +0100 |
blanchet |
improved thm order hack, in case the default names are overridden
|
file |
diff |
annotate
|
| Fri, 21 Dec 2012 15:22:57 +0100 |
blanchet |
linearize eval driver, to work around horrible bug in previous implementation
|
file |
diff |
annotate
|
| Mon, 17 Dec 2012 22:06:28 +0100 |
blanchet |
tuned order to help debugging
|
file |
diff |
annotate
|
| Sun, 16 Dec 2012 12:07:37 +0100 |
blanchet |
added tracing to ATP exporter
|
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
|
| Thu, 13 Dec 2012 23:47:01 +0100 |
blanchet |
get rid of some junk facts in the MaSh evaluation driver
|
file |
diff |
annotate
|
| Thu, 13 Dec 2012 22:49:06 +0100 |
blanchet |
parallelized MaSh exporter
|
file |
diff |
annotate
|
| Thu, 13 Dec 2012 09:21:45 +0100 |
blanchet |
shared bad MaSh query detection between MePo and MaSh, so that the generated files mirror each other
|
file |
diff |
annotate
|
| Wed, 12 Dec 2012 21:48:29 +0100 |
blanchet |
don't query blacklisted theorems in evaluation driver
|
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:24:06 +0100 |
blanchet |
adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
|
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:50 +0100 |
blanchet |
more MaSh tweaking -- in particular, export the same facts in "MaSh_Export" as are later tried in "MaSh_Eval"
|
file |
diff |
annotate
|
| Thu, 06 Dec 2012 16:49:48 +0100 |
blanchet |
export ATP and Isar commands separately
|
file |
diff |
annotate
|
| Thu, 06 Dec 2012 16:07:09 +0100 |
blanchet |
use right names in MePo exporter
|
file |
diff |
annotate
|
| Tue, 04 Dec 2012 23:19:03 +0100 |
blanchet |
added feature weights in MaSh
|
file |
diff |
annotate
|
| Tue, 04 Dec 2012 18:12:29 +0100 |
blanchet |
generalized MaSh exporter to sets of theories
|
file |
diff |
annotate
|
| Fri, 03 Aug 2012 17:56:35 +0200 |
blanchet |
rule out same "technical" theories for MePo as for MaSh
|
file |
diff |
annotate
|
| Fri, 03 Aug 2012 17:56:35 +0200 |
blanchet |
don't generate queries for empty dependencies
|
file |
diff |
annotate
|
| Fri, 03 Aug 2012 17:56:35 +0200 |
blanchet |
crank up max number of dependencies
|
file |
diff |
annotate
|
| Thu, 26 Jul 2012 10:48:03 +0200 |
blanchet |
don't export technical theorems for MaSh
|
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
|
| Thu, 26 Jul 2012 10:48:03 +0200 |
blanchet |
generate fact name in queries again + use ATP dependencies when possible
|
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:46 +0200 |
blanchet |
added locality as a MaSh feature
|
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 |
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 |
more work on MaSh
|
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 |
more implementation work on MaSh
|
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 |
gracefully handle the case of empty theories when going up the accessibility chain
|
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, 11 Jul 2012 21:43:19 +0200 |
blanchet |
moved most of MaSh exporter code to Sledgehammer
|
file |
diff |
annotate
|
| Wed, 11 Jul 2012 21:43:19 +0200 |
blanchet |
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
|
file |
diff |
annotate
|
| Wed, 11 Jul 2012 21:43:19 +0200 |
blanchet |
add Isabelle dependencies to tweak relevance filter
|
file |
diff |
annotate
|
| Wed, 11 Jul 2012 21:43:19 +0200 |
blanchet |
generate ATP dependencies
|
file |
diff |
annotate
|
| Wed, 11 Jul 2012 11:28:27 +0200 |
blanchet |
comment
|
file |
diff |
annotate
|
| Wed, 11 Jul 2012 09:32:29 +0200 |
blanchet |
rationalized output
|
file |
diff |
annotate
|
| Tue, 10 Jul 2012 23:36:03 +0200 |
blanchet |
generate Meng--Paulson facts for evaluation purposes
|
file |
diff |
annotate
|
| Tue, 10 Jul 2012 23:36:03 +0200 |
blanchet |
MaSh evaluation driver
|
file |
diff |
annotate
|
| Tue, 10 Jul 2012 23:36:03 +0200 |
blanchet |
moved MaSh into own files
|
file |
diff |
annotate
|