src/HOL/TPTP/MaSh_Export.thy
2016-05-26 wenzelm 2016-05-26 isabelle update_cartouches -c -t;
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 export a bit
2014-06-29 blanchet 2014-06-29 killed Python version of MaSh, now that the SML version works adequately
2014-06-02 blanchet 2014-06-02 add option to keep duplicates, for more precise evaluation of relevance filters
2014-05-30 blanchet 2014-05-30 more work on exporter
2014-05-30 blanchet 2014-05-30 got rid of 'linearize' option
2014-05-30 blanchet 2014-05-30 extend exporter with new versions of MaSh
2014-01-31 blanchet 2014-01-31 tuning
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-10-15 blanchet 2013-10-15 tweaked signature
2013-08-21 blanchet 2013-08-21 generate max suggestions in MaSh export driver
2013-02-19 blanchet 2013-02-19 provide two modes for MaSh driver: linearized or real visibility
2013-02-07 blanchet 2013-02-07 hide "ext" name, but keep "HOL.ext", to ensure consistency in naming when "ext" is used by LEO-II or Satallax implicitly
2013-01-17 blanchet 2013-01-17 MeSh prover generation
2013-01-17 blanchet 2013-01-17 use precomputed MaSh/MePo data whenever available
2013-01-17 blanchet 2013-01-17 added step to skip some queries
2013-01-17 blanchet 2013-01-17 tweaked defaults
2013-01-16 blanchet 2013-01-16 honor fact range for MePo as well
2013-01-10 blanchet 2013-01-10 removed debugging code
2013-01-10 blanchet 2013-01-10 export MeSh data as well
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-08 blanchet 2012-12-08 more MaSh tweaking -- in particular, export the same facts in "MaSh_Export" as are later tried in "MaSh_Eval"
2012-12-06 blanchet 2012-12-06 export ATP and Isar commands separately
2012-12-04 blanchet 2012-12-04 tuned MaSh exporter -- and don't make temp directories unless explicitly told so
2012-12-04 blanchet 2012-12-04 generalized MaSh exporter to sets of theories
2012-12-03 blanchet 2012-12-03 tweaked MaSh exporter
2012-08-22 wenzelm 2012-08-22 prefer ML_file over old uses;
2012-07-26 blanchet 2012-07-26 don't export technical theorems for MaSh
2012-07-26 blanchet 2012-07-26 generate fact name in queries again + use ATP dependencies when possible
2012-07-23 blanchet 2012-07-23 took out CVC3 again -- there seems to be issues with the server version of CVC3 + minor tweaks
2012-07-20 blanchet 2012-07-20 renamed "iter" fact filter to "MePo" (Meng--Paulson)
2012-07-18 blanchet 2012-07-18 repair MaSh exporter
2012-07-18 blanchet 2012-07-18 more work on MaSh
2012-07-18 blanchet 2012-07-18 started implementing MaSh client-side I/O
2012-07-18 blanchet 2012-07-18 centrally construct expensive data structures
2012-07-18 blanchet 2012-07-18 gracefully handle the case of empty theories when going up the accessibility chain
2012-07-18 blanchet 2012-07-18 dependency tuning
2012-07-11 blanchet 2012-07-11 moved most of MaSh exporter code to Sledgehammer
2012-07-11 blanchet 2012-07-11 further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
2012-07-11 blanchet 2012-07-11 add Isabelle dependencies to tweak relevance filter
2012-07-11 blanchet 2012-07-11 generate ATP dependencies
2012-07-10 blanchet 2012-07-10 generate Meng--Paulson facts for evaluation purposes
2012-07-10 blanchet 2012-07-10 MaSh evaluation driver
2012-07-10 blanchet 2012-07-10 moved MaSh into own files