| Tue, 20 May 2014 16:11:37 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 20 May 2014 09:57:10 +0200 |
blanchet |
implemented MaSh/SML hints
|
file |
diff |
annotate
|
| Tue, 20 May 2014 09:38:39 +0200 |
blanchet |
better way to take invisible facts into account than 'island' business
|
file |
diff |
annotate
|
| Tue, 20 May 2014 02:47:23 +0200 |
blanchet |
cleaner handling of learned proofs
|
file |
diff |
annotate
|
| Tue, 20 May 2014 00:13:31 +0200 |
blanchet |
implemented learning of single proofs in SML MaSh
|
file |
diff |
annotate
|
| Mon, 19 May 2014 23:43:53 +0200 |
blanchet |
take weights into consideration in knn
|
file |
diff |
annotate
|
| Mon, 19 May 2014 23:43:53 +0200 |
blanchet |
added SML implementation of MaSh
|
file |
diff |
annotate
|
| Mon, 19 May 2014 23:43:53 +0200 |
blanchet |
started work on MaSh/SML
|
file |
diff |
annotate
|
| Mon, 19 May 2014 23:43:53 +0200 |
blanchet |
tune
|
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
|
| Mon, 19 May 2014 13:53:58 +0200 |
blanchet |
hide more consts to beautify documentation
|
file |
diff |
annotate
|
| Thu, 27 Mar 2014 17:12:40 +0100 |
wenzelm |
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
|
file |
diff |
annotate
|
| Sat, 22 Mar 2014 18:19:57 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Fri, 21 Feb 2014 00:09:56 +0100 |
blanchet |
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
|
file |
diff |
annotate
|
| Mon, 03 Feb 2014 15:33:18 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 10:23:32 +0100 |
blanchet |
renamed many Sledgehammer ML files to clarify structure
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 10:23:32 +0100 |
blanchet |
renamed ML file
|
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
|
| Wed, 18 Dec 2013 16:50:14 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 09 Dec 2013 04:44:59 +0100 |
blanchet |
disable generalization in MaSh until it is shown to help
|
file |
diff |
annotate
|
| Mon, 09 Dec 2013 04:03:30 +0100 |
blanchet |
generate problems with type classes
|
file |
diff |
annotate
|
| Mon, 09 Dec 2013 04:03:30 +0100 |
blanchet |
more reasonable default weight
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 18:34:04 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Thu, 14 Nov 2013 15:57:48 +0100 |
blanchet |
have MaSh support nameless facts (i.e. proofs) and use that support
|
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
|
| Thu, 17 Oct 2013 20:49:19 +0200 |
blanchet |
generate a comment storing the goal nickname in "learn_prover"
|
file |
diff |
annotate
|
| Thu, 17 Oct 2013 20:20:53 +0200 |
blanchet |
clarified message
|
file |
diff |
annotate
|
| Thu, 17 Oct 2013 02:29:49 +0200 |
blanchet |
choose facts to reprove more randomly, to avoid getting stuck with impossible problems at first
|
file |
diff |
annotate
|
| Thu, 17 Oct 2013 01:04:00 +0200 |
blanchet |
if slicing is disabled, don't enforce last slice's "max_facts", but rather the maximum "max_facts"
|
file |
diff |
annotate
|
| Thu, 17 Oct 2013 01:03:59 +0200 |
blanchet |
remove overloading of "max_facts" -- it already controls the number of facts passed to ATPs for 'learn_prover'
|
file |
diff |
annotate
|
| Tue, 15 Oct 2013 16:14:52 +0200 |
blanchet |
improved duplicate detection in "build_name_tables" by ensuring that the earliest occurrence of a duplicate (if it exists) gets picked as the canonical instance
|
file |
diff |
annotate
|
| Sun, 13 Oct 2013 21:36:26 +0200 |
blanchet |
more prominent MaSh errors
|
file |
diff |
annotate
|
| Thu, 10 Oct 2013 08:23:57 +0200 |
blanchet |
repaired confusion between the stated and effective fact filter -- the mismatch could result in "Match" exceptions
|
file |
diff |
annotate
|
| Thu, 10 Oct 2013 01:17:37 +0200 |
blanchet |
simplify fudge factor code
|
file |
diff |
annotate
|
| Wed, 09 Oct 2013 16:07:33 +0200 |
blanchet |
parallelize MeSh
|
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, 04 Oct 2013 17:00:35 +0200 |
blanchet |
more tracing
|
file |
diff |
annotate
|
| Fri, 04 Oct 2013 16:51:26 +0200 |
blanchet |
more thorough spying
|
file |
diff |
annotate
|
| Fri, 04 Oct 2013 12:59:18 +0200 |
blanchet |
removed pointless special case
|
file |
diff |
annotate
|
| Tue, 01 Oct 2013 15:02:12 +0200 |
blanchet |
removed spurious save if nothing needs to bee learned
|
file |
diff |
annotate
|
| Tue, 24 Sep 2013 12:11:53 +0200 |
blanchet |
honor MaSh's zero-overhead policy -- no learning if the tool is disabled
|
file |
diff |
annotate
|
| Mon, 23 Sep 2013 09:48:06 +0200 |
blanchet |
provide a way to override MaSh's port from configuration file
|
file |
diff |
annotate
|
| Fri, 20 Sep 2013 22:39:30 +0200 |
blanchet |
reduce the number of emitted MaSh commands (among others to facilitate debugging)
|
file |
diff |
annotate
|
| Fri, 20 Sep 2013 22:39:30 +0200 |
blanchet |
MaSh tweaks to facilitate debugging
|
file |
diff |
annotate
|
| Thu, 12 Sep 2013 15:14:54 +0200 |
blanchet |
more robust approach to avoid Python byte code -- environment variables get inherited by subprocesses
|
file |
diff |
annotate
|
| Thu, 12 Sep 2013 11:05:19 +0200 |
blanchet |
when pouring in extra features into the goal, only consider facts from the current theory -- the bottom 10 facts of the last import might be completely unrelated
|
file |
diff |
annotate
|
| Thu, 12 Sep 2013 10:40:53 +0200 |
blanchet |
minor fixes
|
file |
diff |
annotate
|
| Thu, 12 Sep 2013 10:05:10 +0200 |
blanchet |
invoke Python with "no bytecode" option to avoid litering Isabelle source directory with ".pyc" files (which can be problematic for a number of reasons)
|
file |
diff |
annotate
|
| Mon, 26 Aug 2013 12:14:40 +0200 |
blanchet |
reverted 6c5e7143e1f6; took a better look at evaluation data this time
|
file |
diff |
annotate
|
| Mon, 26 Aug 2013 09:07:32 +0200 |
blanchet |
tuned fudge factor in light of evaluation
|
file |
diff |
annotate
|
| Fri, 23 Aug 2013 16:51:53 +0200 |
blanchet |
repaired num_extra_feature_facts + tuning
|
file |
diff |
annotate
|
| Fri, 23 Aug 2013 15:49:27 +0200 |
blanchet |
minor MaSh fix
|
file |
diff |
annotate
|
| Fri, 23 Aug 2013 15:07:32 +0200 |
blanchet |
eliminated some needless MaSh features
|
file |
diff |
annotate
|
| Fri, 23 Aug 2013 14:19:57 +0200 |
blanchet |
tuned output
|
file |
diff |
annotate
|
| Fri, 23 Aug 2013 14:04:08 +0200 |
blanchet |
better tracing + honor blocking better
|
file |
diff |
annotate
|
| Fri, 23 Aug 2013 13:30:25 +0200 |
blanchet |
learn new facts on query if there aren't too many of them in MaSh
|
file |
diff |
annotate
|
| Thu, 22 Aug 2013 23:03:23 +0200 |
blanchet |
increase relevance of unknown proximate facts
|
file |
diff |
annotate
|
| Thu, 22 Aug 2013 23:03:21 +0200 |
blanchet |
fixed subtle bug with "take" + thread overlord through
|
file |
diff |
annotate
|
| Thu, 22 Aug 2013 16:03:13 +0200 |
blanchet |
have kill_all also kill MaSh server + be paranoid about reloading after clear_state, to allow for easier experimentation
|
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
|
| Thu, 22 Aug 2013 08:42:27 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Wed, 21 Aug 2013 16:21:37 +0200 |
blanchet |
improve weight computation for complex terms
|
file |
diff |
annotate
|
| Wed, 21 Aug 2013 15:34:51 +0200 |
blanchet |
improved support for MaSh server
|
file |
diff |
annotate
|
| Wed, 21 Aug 2013 15:18:06 +0200 |
blanchet |
get rid of some silly MaSh features
|
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 |
take out dangerous feature, now that all updates are permanent
|
file |
diff |
annotate
|
| Wed, 21 Aug 2013 09:25:40 +0200 |
blanchet |
use new MaSh command-line arguments
|
file |
diff |
annotate
|
| Wed, 21 Aug 2013 09:25:40 +0200 |
blanchet |
shutdown MaSh server
|
file |
diff |
annotate
|
| Tue, 20 Aug 2013 14:36:22 +0200 |
blanchet |
adapted ML code to new version of MaSh tool
|
file |
diff |
annotate
|
| Tue, 20 Aug 2013 14:36:22 +0200 |
blanchet |
adapted to new MaSh syntax
|
file |
diff |
annotate
|
| Tue, 20 Aug 2013 14:36:22 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 20 Aug 2013 11:42:52 +0200 |
blanchet |
learn MaSh facts on the fly
|
file |
diff |
annotate
|
| Tue, 20 Aug 2013 11:42:51 +0200 |
blanchet |
allow MaSh query to do some learning as well
|
file |
diff |
annotate
|
| Mon, 19 Aug 2013 23:22:04 +0200 |
blanchet |
treat frees as both consts and vars, for more hits
|
file |
diff |
annotate
|
| Mon, 19 Aug 2013 21:59:36 +0200 |
blanchet |
keep long names to stay on the safe side
|
file |
diff |
annotate
|
| Mon, 19 Aug 2013 18:50:45 +0200 |
blanchet |
MaSh tweaking: shorter names + killed (broken) SNoW
|
file |
diff |
annotate
|
| Mon, 19 Aug 2013 16:50:25 +0200 |
blanchet |
handle Bounds as well in MaSh features
|
file |
diff |
annotate
|
| Mon, 19 Aug 2013 14:47:47 +0200 |
blanchet |
add subtypes as well as features in MaSh
|
file |
diff |
annotate
|
| Mon, 19 Aug 2013 14:41:22 +0200 |
blanchet |
generate patterns for variables as well in MaSh (cf. HOL(y)Hammer)
|
file |
diff |
annotate
|
| Mon, 19 Aug 2013 14:26:59 +0200 |
blanchet |
generate deep type patterns in MaSh
|
file |
diff |
annotate
|
| Thu, 18 Jul 2013 20:53:22 +0200 |
wenzelm |
explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it;
|
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
|
| Sun, 19 May 2013 20:41:19 +0200 |
blanchet |
made "completish" mode a bit more complete
|
file |
diff |
annotate
|
| Fri, 17 May 2013 11:35:52 +0200 |
wenzelm |
tuned signature -- emphasize thread creation here;
|
file |
diff |
annotate
|
| Thu, 16 May 2013 13:34:13 +0200 |
blanchet |
tuning -- renamed '_from_' to '_of_' in Sledgehammer
|
file |
diff |
annotate
|
| Wed, 15 May 2013 17:43:42 +0200 |
blanchet |
renamed Sledgehammer functions with 'for' in their names to 'of'
|
file |
diff |
annotate
|
| Tue, 14 May 2013 20:46:09 +0200 |
wenzelm |
more uniform Markup.print_real;
|
file |
diff |
annotate
|
| Tue, 19 Feb 2013 17:01:06 +0100 |
blanchet |
avoid using "smt" for minimization -- better use the prover itself, since then Sledgehammer gets to try metis again and gives the opportunity to output an Isar proof -- and show Isar proof as fallback for SMT proofs
|
file |
diff |
annotate
|
| Tue, 19 Feb 2013 13:37:07 +0100 |
blanchet |
reintroduced crucial sorting accidentally lost in 962190eab40d
|
file |
diff |
annotate
|
| Tue, 19 Feb 2013 13:27:33 +0100 |
blanchet |
compile
|
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 18:34:55 +0100 |
blanchet |
implement (more) accurate computation of parents
|
file |
diff |
annotate
|
| Mon, 18 Feb 2013 18:34:54 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 18 Feb 2013 11:33:43 +0100 |
blanchet |
tuned code: factored out parent computation
|
file |
diff |
annotate
|
| Mon, 18 Feb 2013 10:43:36 +0100 |
blanchet |
tuned code
|
file |
diff |
annotate
|
| Fri, 15 Feb 2013 09:17:20 +0100 |
blanchet |
avoid crude/wrong theorem comparision
|
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
|
| Fri, 15 Feb 2013 09:17:20 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 08 Feb 2013 12:22:37 +0100 |
blanchet |
added option to use SNoW as machine learning algo
|
file |
diff |
annotate
|
| Thu, 07 Feb 2013 14:05:33 +0100 |
blanchet |
killed deadcode
|
file |
diff |
annotate
|
| Thu, 07 Feb 2013 14:05:32 +0100 |
blanchet |
drop needless .0s
|
file |
diff |
annotate
|
| Thu, 07 Feb 2013 14:05:32 +0100 |
blanchet |
distinguish MeSh and smart -- with smart, allow combinations of MaSh, MeSh, and MePo in different slices -- and use MaSh also with SMT solvers, based on evaluation
|
file |
diff |
annotate
|
| Tue, 05 Feb 2013 17:19:13 +0100 |
blanchet |
removed spurious trimming
|
file |
diff |
annotate
|
| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
tuned data structure
|
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 |
thread fact triple (MeSh, MePo, MaSh) to allow different filters in different slices
|
file |
diff |
annotate
|
| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
eliminated needless speed optimization -- and simplified code quite a bit
|
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
|
| Thu, 31 Jan 2013 17:54:05 +0100 |
blanchet |
report (MeSh, MePo, MaSh) triple, to be able to use different filters in different slices
|
file |
diff |
annotate
|
| Thu, 31 Jan 2013 12:09:07 +0100 |
blanchet |
adapted to new MaSh interface
|
file |
diff |
annotate
|
| Sat, 19 Jan 2013 17:42:12 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 18 Jan 2013 16:06:45 +0100 |
blanchet |
tuning
|
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 18:43:59 +0100 |
blanchet |
evaluate more cases (cf. paper)
|
file |
diff |
annotate
|