added MaSh to news

cached ancestor computation

minimal maxes + tuning

learn from SMT proofs when they can be minimized by Metis

clean up interesting constants a bit

convenience

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

MaSh docs

added "learn_from_atp" command to MaSh, for patient users

get rid of redundant "xxx_INSTALLED" environment variabl

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

more MaSh docs

mention MaSh in docs

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

renamed "iter" fact filter to "MePo" (Meng--Paulson)

handle local facts smoothly in MaSh

fixed explosion when computing accessibility

use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)

tuning

merged

further imitation of "usedir" shell script; Pure/build observes build_images option, unlike traditional version; tuned signature;

make nat_cancel_sums simprocs robust in the presence of schematic variables; add regression tests

export code relatively to master directory

require explicit initialization of options; more explicit Position operations;

tuned signature;

define build_options from command line;

some basic Isabelle options;

basic jEdit mode for Isabelle options;

basic support for stand-alone options with external string representation;

minimal build_job;

restrict to required sessions;

proper commas_quote;

tune;

simplified script to build Isabelle/ML;

added eq_file / copy_file corresponding to File.eq / File.copy in ML;

merged

removed ML module DSeq which was a part of the ancient code generator (cf. 58e33a125f32)

deactivating quickcheck narrowing examples to find out if this causes the system error on the current isatest

support for detached Bash_Job with some control operations;

allow catalog entries to be commented-out;

support external processes with explicit environment;

include COMPONENT/etc/sessions as catalog for more directories, for improved scalability with hundreds of entries (notably AFP); misc tuning and simplification;

less redundant data structures;

clarified topological ordering: preserve order of adjacency via reverse fold;

support Session.Queue with ordering and dependencies;

clarified signature;

more explicit treatment of initial Pure sessions;

more general support for Isabelle/Scala command line tools;

tuned width;

prefer general Properties.Value.Boolean;

more SHA1.digest operations;

tuned import;

tuned source structure;

allow explicit specification of additional session directories;

more errors;

some HOL sessions;

cumulate semantic Session_Info, based on syntactic Session_Entry; tuned errors;

more tight treatment of reset_name;

more informative errors;

added parser for Session_Info;

repair MaSh exporter

optimize parent computation in MaSh + remove temporary files

make the monomorphizer more predictable by making the cutoff independent on the number of facts

speed up MaSh queries

use better score function, based on previous evaluation (cf. Deduct 2011 slides)

attempt at meshing according to more meaningful factors

don't include hidden facts in relevance filter + tweak MaSh learning

removed debugging output

removed expensive HO check in MaSh

speed up tautology/metaness check

optimized MaSh output by chunking it

fixed MaSh state load code so it works even if the facts are read in disorder

learn from minimized ATP proofs

improved meshing of MaSh and Meng--Paulson if some MaSh suggestions are cut-off (the common case)

use async manager to manage MaSh learners to make sure they get killed cleanly

more consolidation of MaSh code

removed lie

drastic overhaul of MaSh data structures + fixed a few performance issues

fixed order of accessibles + other tweaks to MaSh

added option to control which fact filter is used

mesh facts by taking into consideration whether a fact is known to MeSh

implemented meshing of Iter and MaSh results

implemented MaSh QUERY operation

refactored MaSh ADD code so it can be used for SUGGEST as well

implemented low-level MaSh ADD operation

make tracing an option

cleaner handling of metacharacters + freshness of one-off facts

better zipping of MaSh facts

implemented MaSh learn theory function

more work on MaSh

improved MaSh string escaping and make more operations string-based

more implementation work on MaSh

started implementing MaSh client-side I/O

tweak output

centrally construct expensive data structures

more work on MaSh

compile

gracefully handle the case of empty theories when going up the accessibility chain

tuning

doc updates

renamed Sledgehammer options

more code rationalization in relevance filter

moved override out of iter filter

fixed bug introduced when moving code around

systematize lazy names in relevance filter

rationalize relevance filter, slowing moving code from Iter to MaSh

killed one file

dependency tuning

renaming

clean up dependencies

explicitly import Dlist theory into library