src/HOL/TPTP/MaSh_Eval.thy
2016-05-26 wenzelm 2016-05-26 isabelle update_cartouches -c -t;
2016-04-09 wenzelm 2016-04-09 tuned signature;
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-09-08 blanchet 2014-09-08 refactored MaSh files to avoid regenerating exports on each eval
2014-07-01 blanchet 2014-07-01 clean up MaSh evaluation driver
2014-06-29 blanchet 2014-06-29 use SMT2
2014-06-27 blanchet 2014-06-27 tweaking
2014-01-31 blanchet 2014-01-31 compile
2014-01-31 blanchet 2014-01-31 tuned ML file name
2013-12-11 wenzelm 2013-12-11 support for polml-5.5.2; support Thread.numPhysicalProcessors of polyml-5.5.2 (according to SVN 1890); clarified max_threads: store plain value internally, reproduce result only on startup, and thus avoid potential system overhead;
2013-02-19 blanchet 2013-02-19 provide two modes for MaSh driver: linearized or real visibility
2013-01-17 blanchet 2013-01-17 use precomputed MaSh/MePo data whenever available
2013-01-17 blanchet 2013-01-17 provide a means to skip a method
2013-01-17 blanchet 2013-01-17 evaluate more cases (cf. paper)
2013-01-17 blanchet 2013-01-17 tweaked defaults
2012-12-15 blanchet 2012-12-15 MaSh exporter can now export subsets of the facts, as consecutive ranges
2012-12-13 blanchet 2012-12-13 parallelized MaSh exporter
2012-12-12 blanchet 2012-12-12 tuning
2012-12-12 blanchet 2012-12-12 adopt the neutral "prover" terminology for MaSh rather than the ambiguous/wrong ATP terminology (which sometimes excludes SMT solvers)
2012-12-10 blanchet 2012-12-10 (re)introduce (even more) aggressive parallelism, for the benefit of those users with dozens of CPU cores
2012-12-10 blanchet 2012-12-10 have MaSh evaluator keep all raw problem/solution files in a directory
2012-12-08 blanchet 2012-12-08 store evaluation output in a file
2012-12-06 blanchet 2012-12-06 use right names in MePo exporter
2012-12-04 blanchet 2012-12-04 rationalized MaSh evaluation harness
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-07-18 blanchet 2012-07-18 repair MaSh exporter
2012-07-18 blanchet 2012-07-18 fixed MaSh state load code so it works even if the facts are read in disorder
2012-07-18 blanchet 2012-07-18 started implementing MaSh client-side I/O
2012-07-18 blanchet 2012-07-18 renaming