src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
2013-11-19 ago tuning
2013-10-17 ago generate a comment storing the goal nickname in "learn_prover"
2013-10-17 ago if slicing is disabled, pick the maximum number of facts, not the number of facts in the last slice
2013-10-09 ago run relevance filter only once for ATPs and SMT solvers, since it should now yield the same results anyway
2013-10-04 ago more thorough spying
2013-10-04 ago more Sledgehammer spying -- record fact indices
2013-10-04 ago more parallelism in blocking mode
2013-09-24 ago encode goal digest in spying log (to detect duplicates)
2013-09-24 ago made SML/NJ happy
2013-09-23 ago tuned spying
2013-09-23 ago added "spy" option to Sledgehammer
2013-09-11 ago tuning
2013-08-23 ago eliminated some needless MaSh features
2013-08-17 ago sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications -- old-style in-line replacement is superseded by auto mode or panel;
2013-08-17 ago more direct sledgehammer configuration via mode = Normal_Result and output_result;
2013-08-13 ago added flag for jEdit/PIDE asynchronous mode
2013-08-08 ago dockable window for Sledgehammer, based on asynchronous/parallel query operation;
2013-07-13 ago more explicit Markup.information for messages produced by "auto" tools;
2013-07-09 ago moved code -> easier debugging
2013-05-28 ago redid rac7830871177 to avoid duplicate fixed variable (e.g. lemma "P (a::nat)" proof - have "!!a::int. Q a" sledgehammer [e])
2013-05-24 ago improved handling of free variables' types in Isar proofs
2013-05-17 ago tuned signature -- emphasize thread creation here;
2013-05-15 ago renamed Sledgehammer functions with 'for' in their names to 'of'
2013-04-23 ago tuning
2013-02-19 ago 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
2013-01-31 ago tuned data structure
2013-01-31 ago thread through fact triple component from which used facts come, for accurate index output
2013-01-31 ago more precise output of selected facts
2013-01-31 ago thread fact triple (MeSh, MePo, MaSh) to allow different filters in different slices
2013-01-31 ago simplified SMT solver code in Sledgehammer
2013-01-31 ago eliminated needless speed optimization -- and simplified code quite a bit
2013-01-31 ago distinguish raw and non-raw facts, using raw for 10 000s of facts and non-raw after selection of some hundreds
2013-01-31 ago report (MeSh, MePo, MaSh) triple, to be able to use different filters in different slices
2013-01-15 ago tuned whitespace
2013-01-14 ago run Sledgehammer provers in parallel in "try"
2013-01-13 ago tuned message
2013-01-05 ago increased hard timeout -- minimization can take time
2013-01-02 ago use "Lazy" to simplify control flow a bit and guarantee single evaluation (at most)
2013-01-02 ago tuning
2012-12-15 ago thread no timeout properly
2012-11-25 ago Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-10-18 ago refactor code
2012-09-14 ago clarified markup names;
2012-08-14 ago be less aggressive at kicking out chained facts
2012-07-20 ago faster maximal node computation
2012-07-20 ago learn from SMT proofs when they can be minimized by Metis
2012-07-20 ago name tuning
2012-07-20 ago fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
2012-07-20 ago learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds
2012-07-20 ago renamed ML structures
2012-07-18 ago learn from minimized ATP proofs
2012-07-18 ago use async manager to manage MaSh learners to make sure they get killed cleanly
2012-07-18 ago centrally construct expensive data structures
2012-07-18 ago renamed Sledgehammer options
2012-07-18 ago more code rationalization in relevance filter
2012-07-18 ago systematize lazy names in relevance filter
2012-07-18 ago rationalize relevance filter, slowing moving code from Iter to MaSh
2012-07-11 ago further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
2012-05-10 ago distinguish between instantiated and uninstantiated inductions -- the latter are OK for first-order provers
2012-04-18 ago get rid of minor optimization that caused strange problems and was hard to debug (and apparently saved less than 100 ms on a 30 s run)