src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
2013-11-19 ago tuning
2013-11-14 ago have MaSh support nameless facts (i.e. proofs) and use that support
2013-10-18 ago make sure add: doesn't add duplicates, and works for [no_atp] facts
2013-10-17 ago generate a comment storing the goal nickname in "learn_prover"
2013-10-17 ago clarified message
2013-10-17 ago choose facts to reprove more randomly, to avoid getting stuck with impossible problems at first
2013-10-17 ago if slicing is disabled, don't enforce last slice's "max_facts", but rather the maximum "max_facts"
2013-10-17 ago remove overloading of "max_facts" -- it already controls the number of facts passed to ATPs for 'learn_prover'
2013-10-15 ago 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
2013-10-13 ago more prominent MaSh errors
2013-10-10 ago repaired confusion between the stated and effective fact filter -- the mismatch could result in "Match" exceptions
2013-10-10 ago simplify fudge factor code
2013-10-09 ago parallelize MeSh
2013-10-09 ago 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)
2013-10-09 ago optimized built-in const check
2013-10-04 ago more tracing
2013-10-04 ago more thorough spying
2013-10-04 ago removed pointless special case
2013-10-01 ago removed spurious save if nothing needs to bee learned
2013-09-24 ago honor MaSh's zero-overhead policy -- no learning if the tool is disabled
2013-09-23 ago provide a way to override MaSh's port from configuration file
2013-09-20 ago reduce the number of emitted MaSh commands (among others to facilitate debugging)
2013-09-20 ago MaSh tweaks to facilitate debugging
2013-09-12 ago more robust approach to avoid Python byte code -- environment variables get inherited by subprocesses
2013-09-12 ago 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
2013-09-12 ago minor fixes
2013-09-12 ago invoke Python with "no bytecode" option to avoid litering Isabelle source directory with ".pyc" files (which can be problematic for a number of reasons)
2013-08-26 ago reverted 6c5e7143e1f6; took a better look at evaluation data this time
2013-08-26 ago tuned fudge factor in light of evaluation
2013-08-23 ago repaired num_extra_feature_facts + tuning
2013-08-23 ago minor MaSh fix
2013-08-23 ago eliminated some needless MaSh features
2013-08-23 ago tuned output
2013-08-23 ago better tracing + honor blocking better
2013-08-23 ago learn new facts on query if there aren't too many of them in MaSh
2013-08-22 ago increase relevance of unknown proximate facts
2013-08-22 ago fixed subtle bug with "take" + thread overlord through
2013-08-22 ago have kill_all also kill MaSh server + be paranoid about reloading after clear_state, to allow for easier experimentation
2013-08-22 ago take chained and proximate facts into consideration when computing MaSh features
2013-08-22 ago pour extra features from proximate facts into goal, in exporter
2013-08-22 ago tuning
2013-08-21 ago improve weight computation for complex terms
2013-08-21 ago improved support for MaSh server
2013-08-21 ago get rid of some silly MaSh features
2013-08-21 ago weight MaSh constants by frequency
2013-08-21 ago only generate feature weights for queries -- they're not used elsewhere
2013-08-21 ago take out dangerous feature, now that all updates are permanent
2013-08-21 ago use new MaSh command-line arguments
2013-08-21 ago shutdown MaSh server
2013-08-20 ago adapted ML code to new version of MaSh tool
2013-08-20 ago adapted to new MaSh syntax
2013-08-20 ago tuning
2013-08-20 ago learn MaSh facts on the fly
2013-08-20 ago allow MaSh query to do some learning as well
2013-08-19 ago treat frees as both consts and vars, for more hits
2013-08-19 ago keep long names to stay on the safe side
2013-08-19 ago MaSh tweaking: shorter names + killed (broken) SNoW
2013-08-19 ago handle Bounds as well in MaSh features
2013-08-19 ago add subtypes as well as features in MaSh
2013-08-19 ago generate patterns for variables as well in MaSh (cf. HOL(y)Hammer)