src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
Thu, 17 Oct 2013 20:20:53 +0200 blanchet clarified message
Thu, 17 Oct 2013 02:29:49 +0200 blanchet choose facts to reprove more randomly, to avoid getting stuck with impossible problems at first
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"
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'
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
Sun, 13 Oct 2013 21:36:26 +0200 blanchet more prominent MaSh errors
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
Thu, 10 Oct 2013 01:17:37 +0200 blanchet simplify fudge factor code
Wed, 09 Oct 2013 16:07:33 +0200 blanchet parallelize MeSh
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)
Wed, 09 Oct 2013 09:47:59 +0200 blanchet optimized built-in const check
Fri, 04 Oct 2013 17:00:35 +0200 blanchet more tracing
Fri, 04 Oct 2013 16:51:26 +0200 blanchet more thorough spying
Fri, 04 Oct 2013 12:59:18 +0200 blanchet removed pointless special case
Tue, 01 Oct 2013 15:02:12 +0200 blanchet removed spurious save if nothing needs to bee learned
Tue, 24 Sep 2013 12:11:53 +0200 blanchet honor MaSh's zero-overhead policy -- no learning if the tool is disabled
Mon, 23 Sep 2013 09:48:06 +0200 blanchet provide a way to override MaSh's port from configuration file
Fri, 20 Sep 2013 22:39:30 +0200 blanchet reduce the number of emitted MaSh commands (among others to facilitate debugging)
Fri, 20 Sep 2013 22:39:30 +0200 blanchet MaSh tweaks to facilitate debugging
Thu, 12 Sep 2013 15:14:54 +0200 blanchet more robust approach to avoid Python byte code -- environment variables get inherited by subprocesses
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
Thu, 12 Sep 2013 10:40:53 +0200 blanchet minor fixes
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)
Mon, 26 Aug 2013 12:14:40 +0200 blanchet reverted 6c5e7143e1f6; took a better look at evaluation data this time
Mon, 26 Aug 2013 09:07:32 +0200 blanchet tuned fudge factor in light of evaluation
Fri, 23 Aug 2013 16:51:53 +0200 blanchet repaired num_extra_feature_facts + tuning
Fri, 23 Aug 2013 15:49:27 +0200 blanchet minor MaSh fix
Fri, 23 Aug 2013 15:07:32 +0200 blanchet eliminated some needless MaSh features
Fri, 23 Aug 2013 14:19:57 +0200 blanchet tuned output
Fri, 23 Aug 2013 14:04:08 +0200 blanchet better tracing + honor blocking better
Fri, 23 Aug 2013 13:30:25 +0200 blanchet learn new facts on query if there aren't too many of them in MaSh
Thu, 22 Aug 2013 23:03:23 +0200 blanchet increase relevance of unknown proximate facts
Thu, 22 Aug 2013 23:03:21 +0200 blanchet fixed subtle bug with "take" + thread overlord through
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
Thu, 22 Aug 2013 12:16:56 +0200 blanchet take chained and proximate facts into consideration when computing MaSh features
Thu, 22 Aug 2013 12:12:52 +0200 blanchet pour extra features from proximate facts into goal, in exporter
Thu, 22 Aug 2013 08:42:27 +0200 blanchet tuning
Wed, 21 Aug 2013 16:21:37 +0200 blanchet improve weight computation for complex terms
Wed, 21 Aug 2013 15:34:51 +0200 blanchet improved support for MaSh server
Wed, 21 Aug 2013 15:18:06 +0200 blanchet get rid of some silly MaSh features
Wed, 21 Aug 2013 14:54:25 +0200 blanchet weight MaSh constants by frequency
Wed, 21 Aug 2013 09:25:40 +0200 blanchet only generate feature weights for queries -- they're not used elsewhere
Wed, 21 Aug 2013 09:25:40 +0200 blanchet take out dangerous feature, now that all updates are permanent
Wed, 21 Aug 2013 09:25:40 +0200 blanchet use new MaSh command-line arguments
Wed, 21 Aug 2013 09:25:40 +0200 blanchet shutdown MaSh server
Tue, 20 Aug 2013 14:36:22 +0200 blanchet adapted ML code to new version of MaSh tool
Tue, 20 Aug 2013 14:36:22 +0200 blanchet adapted to new MaSh syntax
Tue, 20 Aug 2013 14:36:22 +0200 blanchet tuning
Tue, 20 Aug 2013 11:42:52 +0200 blanchet learn MaSh facts on the fly
Tue, 20 Aug 2013 11:42:51 +0200 blanchet allow MaSh query to do some learning as well
Mon, 19 Aug 2013 23:22:04 +0200 blanchet treat frees as both consts and vars, for more hits
Mon, 19 Aug 2013 21:59:36 +0200 blanchet keep long names to stay on the safe side
Mon, 19 Aug 2013 18:50:45 +0200 blanchet MaSh tweaking: shorter names + killed (broken) SNoW
Mon, 19 Aug 2013 16:50:25 +0200 blanchet handle Bounds as well in MaSh features
Mon, 19 Aug 2013 14:47:47 +0200 blanchet add subtypes as well as features in MaSh
Mon, 19 Aug 2013 14:41:22 +0200 blanchet generate patterns for variables as well in MaSh (cf. HOL(y)Hammer)
Mon, 19 Aug 2013 14:26:59 +0200 blanchet generate deep type patterns in MaSh
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;
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])
Fri, 24 May 2013 16:43:37 +0200 blanchet improved handling of free variables' types in Isar proofs
less more (0) -100 -60 tip