clarified signature;

get rid of visibility in MaSh -- it slows it down more than it helps

isabelle update -u control_cartouches;

tuned signature: more operations;

tuned signature;

made MaSh faster and less likely to hang seemingly forever

optimized parent computation in MaSh

avoid loading MaSh file first time around for higher responsiveness of Sledgehammer

tuned MaSh's metacharacters to avoid needless decoding

optimization in MaSh parsing

killed final stops in Sledgehammer and friends

tuned signature;

prefer infix operations;

early warning when Sledgehammer finds a proof

clarified modules;
tuned signature;

removed tracing

more tracing in MaSh

speed up MaSh duplicate check

sped up MaSh nickname generation

speed up MaSh

further reduced dependency on legacy async thread manager

eliminated obsolete environment variable

proper platform_path;

prefer theory_id operations;
tuned signature;

more explicit use of context and elimination of Thm.theory_of_thm, although unclear (and untested?) situations remain;

clarified context;

tuned signature;

tuned signature;

tuned signature;

more standard Long_Name operations;

tuned;

Thm.cterm_of and Thm.ctyp_of operate on local context;

tuned signature -- prefer qualified names;

careful about visibility of facts that have the same 'theory' in optimization

less confusing constant

tuning

more explicit indication of Async_Manager_Legacy as Proof General legacy;

--HG--
rename : src/HOL/Tools/Sledgehammer/async_manager.ML => src/HOL/Tools/Sledgehammer/async_manager_legacy.ML

separate module Random;
proper Synchronized.var;

renamed "pairself" to "apply2", in accordance to @{apply 2};

prefer explicit Keyword.keywords;

discontinued obsolete Output.urgent_message;

don't needlessly regenerate entire file when the time stamps are equal

eliminated source of 'DUP's in MaSh

fixed sorting (broken since 9cc802a8ab06)

beware of duplicate fact names

made SML/NJ happier

made SML/NJ happier

record MaSh algorithm in spying data

also learn when 'fact_filter =' is set explicitly

no warning in case MaSh is disabled

no need for 'mash' subdirectory after removal of Python program

tuning

made SML/NJ happier

tuned terminology

improvements to the machine learning algos (due to Cezary K.)

changed default MaSh engine

removed needless code

speed up MaSh a bit

mix NB and kNN

tuned (reordered) code

tuning

killed Python version of MaSh, now that the SML version works adequately

correctly take weights into consideration

use right theory name for theorems in evaluation driver

killed dead code

reintroduced 'extra features' + only print message in verbose mode

got rid of hard-coded weights, now that we have TFIDF

tuning

tuning

reintroduced 'extra features' but with lower weight than before (to account for tfidf)

reintroduced MaSh hints, this time as persistent creatures

always expand all paths

tuned output

tuned output

right array indexing

incremental learning when learing several facts

tuning

more incremental learning of single fact

avoid needless (trivial) reordering on load

recompute learning data at learning time, not query time

imported patch killed_num_known_facts0

refactoring

renamed experimental learning engines

tuning

refactoring

removed experimental machine learning engine

store string-to-index tables in memory

disable 'extra' feature tainting for now

tuning

tuning

tuning

tuning

tuning

honor visible in SML naive Bayes

honor visibility in SML k-NN

got rid of a few experimental options

tuning

killed dead code

avoid subscripting array with ~1

killed dead data

new version of adaptive k-NN with TFIDF

refactoring

tuning

refactoring

adaptive k-NN

tuning

eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)

optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct)

minor table access optimization

optimize log

enable TF-IDF

added another experimental engine

tweaked experimental setup

use strings to communicate with external process, to ease debugging

added experimental MaSh engine

changed default MaSh parameters based on (in vitro) evaluation

more MaSh engine variations, for evaluations

split parameter into two

more generous formula -- there are lots of duplicates out there

automatically learn MaSh facts also in 'blocking' mode

add option to keep duplicates, for more precise evaluation of relevance filters

made 'Kuehlwein-style' be really like Python code, we now think

make SML code closer to Python code when 'nb_kuehlwein_style' is true

added sleep to give time for the server to shut down -- this is a hack, but it's only in experimental code that will hopefully soon go away

added another way of invoking Python code, for experiments

make SML naive Bayes closer to Python version

more work on exporter

extend exporter with new versions of MaSh

more generous max number of suggestions, for more safety

changed MaSh to use SML version instead of Python version of naive Bayes by default (i.e. if MASH=yes in the settings, or 'fact_filter=mash' with no other explicit setting)

export more ML functions, for experimentation

disabled IDF for now -- empirical evidence points the wrong way (as usual)

tuning

tuning

optimized computation

enabled IDF for naive Bayes ML

tuning

repaired subscript problem in SML kNN

tuning

always remove duplicates in meshing + use weights for Naive Bayes

updated naive Bayes

renamed 'MaSh' option

automatically reload state file when it changes on disk

avoid slow inspection of proof terms now that dependencies are stored in 'state'

properly mark relearns as dirty

disable weights that cause more harm than they help in kNN

add self dependency to naive Bayes

make MaSh Python the default when passing 'fact_filter = mash' without enabling the 'maSh' Isabelle system option

reverted '|' features in MaSh -- these sounded like a good idea but never really worked

until naive Bayes supports weights, don't incorporate 'extra' low-weight features

added comment

added naive Bayes ML implementation, due to Cezary Kaliszyk (like k-NN)

added Isabelle system option 'mash'

more flexible environment variable

tuning

implemented MaSh/SML hints

better way to take invisible facts into account than 'island' business

cleaner handling of learned proofs

implemented learning of single proofs in SML MaSh

take weights into consideration in knn

added SML implementation of MaSh

started work on MaSh/SML

tune

store all MaSh data on the Isabelle side, in preparation for replacing 'mash.py' with ML solution

hide more consts to beautify documentation

clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;

more antiquotations;

adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'

tuning

renamed many Sledgehammer ML files to clarify structure

--HG--
rename : src/HOL/Tools/Sledgehammer/sledgehammer_run.ML => src/HOL/Tools/Sledgehammer/sledgehammer.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_print.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar_print.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML => src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML => src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML

renamed ML file

--HG--
rename : src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML => src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML

made timeouts in Sledgehammer not be 'option's -- simplified lots of code

tuning

disable generalization in MaSh until it is shown to help

generate problems with type classes

more reasonable default weight

tuning

have MaSh support nameless facts (i.e. proofs) and use that support

make sure add: doesn't add duplicates, and works for [no_atp] facts

generate a comment storing the goal nickname in "learn_prover"

clarified message

choose facts to reprove more randomly, to avoid getting stuck with impossible problems at first

if slicing is disabled, don't enforce last slice's "max_facts", but rather the maximum "max_facts"

remove overloading of "max_facts" -- it already controls the number of facts passed to ATPs for 'learn_prover'

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

more prominent MaSh errors

repaired confusion between the stated and effective fact filter -- the mismatch could result in "Match" exceptions

simplify fudge factor code

parallelize MeSh

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)

optimized built-in const check

more tracing

more thorough spying

removed pointless special case

removed spurious save if nothing needs to bee learned

honor MaSh's zero-overhead policy -- no learning if the tool is disabled

provide a way to override MaSh's port from configuration file

reduce the number of emitted MaSh commands (among others to facilitate debugging)

MaSh tweaks to facilitate debugging

more robust approach to avoid Python byte code -- environment variables get inherited by subprocesses

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

minor fixes

invoke Python with "no bytecode" option to avoid litering Isabelle source directory with ".pyc" files (which can be problematic for a number of reasons)

reverted 6c5e7143e1f6; took a better look at evaluation data this time

tuned fudge factor in light of evaluation

repaired num_extra_feature_facts + tuning

minor MaSh fix

eliminated some needless MaSh features

tuned output

better tracing + honor blocking better

learn new facts on query if there aren't too many of them in MaSh

increase relevance of unknown proximate facts

fixed subtle bug with "take" + thread overlord through

have kill_all also kill MaSh server + be paranoid about reloading after clear_state, to allow for easier experimentation

take chained and proximate facts into consideration when computing MaSh features

pour extra features from proximate facts into goal, in exporter

tuning

improve weight computation for complex terms

improved support for MaSh server

get rid of some silly MaSh features

weight MaSh constants by frequency

only generate feature weights for queries -- they're not used elsewhere

take out dangerous feature, now that all updates are permanent

use new MaSh command-line arguments

shutdown MaSh server

adapted ML code to new version of MaSh tool

adapted to new MaSh syntax

tuning

learn MaSh facts on the fly

allow MaSh query to do some learning as well

treat frees as both consts and vars, for more hits

keep long names to stay on the safe side

MaSh tweaking: shorter names + killed (broken) SNoW

handle Bounds as well in MaSh features

add subtypes as well as features in MaSh

generate patterns for variables as well in MaSh (cf. HOL(y)Hammer)

generate deep type patterns in MaSh

explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it;

redid rac7830871177 to avoid duplicate fixed variable (e.g. lemma "P (a::nat)" proof - have "!!a::int. Q a" sledgehammer [e])

improved handling of free variables' types in Isar proofs

made "completish" mode a bit more complete

tuned signature -- emphasize thread creation here;

tuning -- renamed '_from_' to '_of_' in Sledgehammer

renamed Sledgehammer functions with 'for' in their names to 'of'

more uniform Markup.print_real;

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

reintroduced crucial sorting accidentally lost in 962190eab40d

compile

provide two modes for MaSh driver: linearized or real visibility

implement (more) accurate computation of parents

tuning

tuned code: factored out parent computation

tuned code

avoid crude/wrong theorem comparision

tuned code

more MaSh tracing

tuning

added option to use SNoW as machine learning algo

killed deadcode

drop needless .0s

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

removed spurious trimming

tuned data structure

more precise output of selected facts

thread fact triple (MeSh, MePo, MaSh) to allow different filters in different slices

eliminated needless speed optimization -- and simplified code quite a bit

distinguish raw and non-raw facts, using raw for 10 000s of facts and non-raw after selection of some hundreds

report (MeSh, MePo, MaSh) triple, to be able to use different filters in different slices

adapted to new MaSh interface

tuning

tuning

optimization -- evaluate conversion to table only once

use correct weights in MeSh driver

evaluate more cases (cf. paper)

updated MaSh

adjust weights -- sorts are prolific, so tone them down even more

don't learn theories -- this option is very slow and not very helpful

honor unknown chained in MaSh and a few other tweaks

remove obsolete MaSh files

cleaned up hint handling

better handlig of built-ins -- at the top-level, not in subterms

honor filtering out of arguments for built-in constants (e.g. representation of numerals)

new version of MaSh Python component

don't learn from the proof of "psimps" etc.

updated MaSh Python component

start using MaSh hints

always compare theorem using the same, weaker function

export MeSh data as well

get rid of spurious "Isar" proofs

also generate queries for goals with too many Isar dependencies

tuned message

tap after, not before command invocation

refined class handling, to prevent cycles in fact graph

tweaked nicknames

speed up generation of local theorem nicknames

tweaked fudge factor

tuning

tuned ML function name

slightly more elegant naming convention (to keep low-level and high-level APIs separated)

tuned ML function names

improved thm order hack, in case the default names are overridden

enable theory learning in MaSh

name tuning

better weight functions for MePo/MaSh etc.

updated MaSh serialization number (to reflect new weights)

contain exponential explosion of term patterns

tuned weights -- keep same relative values, but use 1.0 as the least weight

really honor pattern depth, and use 2 by default

tuning

thread no timeout properly

merge aliased theorems in MaSh dependencies, modulo symmetry of equality

adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)

generalized notion of active area, where sendback is just one application;
some support for graphview via active area;

--HG--
rename : src/Pure/PIDE/sendback.ML => src/Pure/PIDE/active.ML
rename : src/Tools/jEdit/src/sendback.scala => src/Tools/jEdit/src/active.scala

don't have MaSh pretend it knows facts it doesn't know

fixed embarrassing off-by-one bug in MaSh's Mesh

tweak MaSh fudge factors

more MaSh tweaking -- in particular, export the same facts in "MaSh_Export" as are later tried in "MaSh_Eval"

use proper entry point for MaSh in test driver

parse more liberal MaSh suggestion syntax (for the eval driver)

tweaked MaSh proximity

reduce max number of dependencies for MaSh to get rid of junk

more feature tweaks

prioritize chained facts

more MaSh feature tweaking

record free variables as a MaSh feature

expand type classes into their ancestors for MaSh

tweaked MaSh features, based on comments by Josef Urban

increase weight of local facts again (MaSh)

simplify code now that "mash.py" supports weights

tweaked order of theorems to avoid forward dependencies (MaSh)

more robustness in the face of MaSh format changes -- don't overwrite new versions with old versions

added feature weights in MaSh

promote local facts using a hack (for MaSh)

take proximity into account for MaSh + fix a debilitating bug in feature generation

tuning

turned off noisy MaSh features

simplify MaSh term patterns + add missing global facts if there aren't too many

MaSh improvements: deeper patterns + more respect for chained facts

tuned names

proper quoting of paths in MaSh shell script, take 2 (cf. b00eeb8e352e)

robust writing of MaSh state -- better drop learning data than cause other problems in Sledgehammer

tuned order of functions

proper quoting of paths in MaSh

simplify code slightly

moved MaSh's Python code into Isabelle

more abstract Sendback operations, with explicit id/exec_id properties;
purge result messages (again), cf. db58490a68ac, 7b61a539721e;

thread context correctly when printing backquoted facts

made MaSh more robust in the face of duplicate "nicknames" (which can happen e.g. if you have a lemma called foo(1) and another called foo_1 in the same theory)

optimized saving

remember ATP flops to avoid repeating them too quickly

remember which MaSh proofs were found using ATPs

rule out same "technical" theories for MePo as for MaSh

crank up max number of dependencies

cleaner temporary file cleanup for MaSh, based on tried-and-trusted code

don't export technical theorems for MaSh

cap the number of facts returned by MaSh

remove MaSh junk associated with size functions

identified "evil" theories for MaSh -- this is rather ad hoc, but so is MaSh anyway

removed MaSh junk arising from primrec definitions

distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh

faster "save" operation

include unknown local facts in MaSh

ensure all calls to "mash" program are synchronous

don't relearn old facts in Isar mode

tune Mesh filter

faster maximal node computation

honor suggested MaSh weights

relearn ATP proofs

don't store fresh names in fact graph, since these cannot be the parents of any other facts

cached ancestor computation

minimal maxes + tuning

learn from SMT proofs when they can be minimized by Metis

clean up interesting constants a bit

name tuning

learning should honor the fact override and the chained facts

fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully

added "learn_from_atp" command to MaSh, for patient users

add versioning to MaSh state + cleanup dead code

eliminated special handling of init case, now that "mash.py" has been optimized to handle sequences of add gracefully

use good old MePo filter for SMT solvers by default, since arithmetic is built-in for them

added locality as a MaSh feature

learn on explicit "min" command but do the learning in a thread, since it may take a couple of seconds

learn command in MaSh

added possibility of running external MaSh commands asynchronously

renamed ML structures

renamed ML files

--HG--
rename : src/HOL/Tools/Sledgehammer/sledgehammer_filter_mash.ML => src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
rename : src/HOL/Tools/Sledgehammer/sledgehammer_filter_iter.ML => src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML