merged

NEWS

library theories for debugging and parallel computing using code generation towards Isabelle/ML

also consider current working directory (cf. 3a5a5a992519)

parallel scheduling of jobs; misc tuning;

tuned;

maintain set of source digests, including relevant parts of session entry;

determine source dependencies, relatively to preloaded theories; tuned signature;

propagate defined options; misc tuning;

disallow quotes in path specifications -- extra paranoia;

save image for inner nodes only; misc tuning and simplification;

some actual build function on ML side; further imitation of "usedir" shell script;

tuned -- no dependency on exit function;

more ML_System operations;

restricting Quickcheck_Examples' root file to one basic theory to see if the system error on isatest still occurs

handling partiality in the case where the equality optimisation is applied

merged

updated File.find_files;

more abstract file system operations in Scala, corresponding to ML version;

eliminated obsolete session_manager.scala;

more explicit java.io.{File => JFile};

tune Mesh filter

faster maximal node computation

honor suggested MaSh weights

use CVC3 and Yices by default if they are available and there are enough cores

relearn ATP proofs

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

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