src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
2010-03-19 blanchet 2010-03-19 move the Sledgehammer Isar commands together into one file; this will make easier to add options and reorganize them later
2010-03-18 blanchet 2010-03-18 fix Mirabelle after renaming Sledgehammer structures
2010-03-05 wenzelm 2010-03-05 use regular Proof.goal (which is what methods usually see) and prevent sledgehammer from crashing;
2009-12-10 boehmes 2009-12-10 only invoke metisFT if metis failed
2009-12-08 boehmes 2009-12-08 also consider the fully-typed version of metis for Mirabelle measurements
2009-10-29 wenzelm 2009-10-29 modernized some structure names;
2009-10-28 wenzelm 2009-10-28 renamed raw Proof.get_goal to Proof.raw_goal;
2009-10-27 boehmes 2009-10-27 measure runtime of ATPs only if requested
2009-10-20 boehmes 2009-10-20 proper exceptions instead of unhandled partiality
2009-10-18 nipkow 2009-10-18 merged
2009-10-18 nipkow 2009-10-18 added sums of squares for standard deviation
2009-10-17 wenzelm 2009-10-17 made SML/NJ happy;
2009-10-15 wenzelm 2009-10-15 natural argument order for prover; renamed atp_problem to problem; standard naming convention for the_system;
2009-10-15 wenzelm 2009-10-15 ATP_Manager.get_prover: canonical argument order; eliminated various aliases of existing operations, notably Output channels; tuned messages; misc tuning and clarification;
2009-10-15 wenzelm 2009-10-15 eliminated extraneous wrapping of public records; tuned;
2009-10-15 wenzelm 2009-10-15 structure ATP_Manager: eliminated slightly odd get/set operations in favour of Unsynchronized.ref; uniform interpretation of ATP_Manager.atps via ATP_Manager.get_atps;
2009-10-14 wenzelm 2009-10-14 modernized structure names;
2009-10-04 boehmes 2009-10-04 avoid exception Option: only apply "the" if needed
2009-10-03 boehmes 2009-10-03 re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values, eliminated unused provers, turned references into configuration values
2009-10-01 nipkow 2009-10-01 resolved conflict
2009-10-01 nipkow 2009-10-01 record max lemmas used
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-09-24 nipkow 2009-09-24 record how many "proof"s are solved by s/h
2009-09-19 nipkow 2009-09-19 restructured code
2009-09-18 nipkow 2009-09-18 modified minimization log
2009-09-18 nipkow 2009-09-18 skip &&& goals
2009-09-17 nipkow 2009-09-17 removed misleading log line
2009-09-16 nipkow 2009-09-16 revised lemma counting
2009-09-15 boehmes 2009-09-15 added hard timeout for sledgehammer based on elapsed time (no need to trust ATP's timeout handling); separate Perl script to invoke local ATPs and measure their user time, with proper setup of process groups required by E
2009-09-14 nipkow 2009-09-14 count number of iterations required for minimization (and fixed bug: minimization was always called)
2009-09-13 wenzelm 2009-09-13 explicitly export type abbreviations (as usual in SML97); explicit type constraints for record patterns -- SML does not support record polymorphism; observe max. line length (80-100);
2009-09-12 wenzelm 2009-09-12 standard headers and text sections;
2009-09-10 nipkow 2009-09-10 position information is now passed to all actions; mirabele_s/h logs all proved positions.
2009-09-10 nipkow 2009-09-10 logging number of metis lemmas
2009-09-09 nipkow 2009-09-09 minimization: comparing w/ and w/o.
2009-09-08 boehmes 2009-09-08 timeout option for ATPs
2009-09-07 nipkow 2009-09-07 tuned stats
2009-09-07 nipkow 2009-09-07 tuned stats
2009-09-07 nipkow 2009-09-07 enabled metis permanently, tuned stats
2009-09-05 boehmes 2009-09-05 added signature ATP_MINIMAL, fixed AtpMinimal.minimalize for the trivial case, Mirabelle: added an option to minimize a theorem set found by sledgehammer, use timeout of sledgehammer instead of additional timeLimit
2009-09-05 boehmes 2009-09-05 separate output of ATP user time and sledgehammer (ML code) user time
2009-09-05 boehmes 2009-09-05 added initialization and cleanup of actions, added option to suppress Isabelle output, sledgehammer action produces its own report (no need for additional perl script)
2009-09-04 boehmes 2009-09-04 tuned
2009-09-03 boehmes 2009-09-03 Mirabelle: actions are responsible for catching exceptions and producing suitable log messages (makes log message uniform), removed PolyML.makestring (no strict dependency on PolyML anymore)
2009-09-03 boehmes 2009-09-03 added option full_typed for sledgehammer action
2009-09-03 boehmes 2009-09-03 added runtime information to sledgehammer
2009-09-03 boehmes 2009-09-03 Mirabelle: logging of exceptions (works only for PolyML)
2009-09-02 boehmes 2009-09-02 Mirabelle: actions are responsible for handling exceptions, Mirabelle core logs only structural information, measuring running times for sledgehammer and subsequent metis invocation, Mirabelle produces reports for every theory (only for sledgehammer at the moment)
2009-09-02 boehmes 2009-09-02 moved Mirabelle from HOL/Tools to HOL, added session HOL-Mirabelle