src/HOL/Tools/ATP_Manager/atp_wrapper.ML
2010-04-20 blanchet 2010-04-20 added "explicit_apply" option to Sledgehammer, to control whether an explicit apply function should be used as much or as little as possible (replaces a previous global variable)
2010-04-19 blanchet 2010-04-19 get rid of "conjecture_pos", which is no longer necessary now that it's Metis's job, not Sledgehammer's, to report inconsistent contexts
2010-04-19 blanchet 2010-04-19 make Sledgehammer's minimizer also minimize Isar proofs
2010-04-19 blanchet 2010-04-19 don't use readable names if proof reconstruction is needed, because it uses the structure of names
2010-04-19 blanchet 2010-04-19 rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
2010-04-19 blanchet 2010-04-19 set SPASS option on the command-line, so that it doesn't vanish when moving to TPTP format
2010-04-17 blanchet 2010-04-17 added missing \n in output
2010-04-16 blanchet 2010-04-16 added timestamp to proof
2010-04-16 blanchet 2010-04-16 store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
2010-04-15 blanchet 2010-04-15 make Sledgehammer's output more debugging friendly
2010-04-14 blanchet 2010-04-14 added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture
2010-04-14 blanchet 2010-04-14 make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
2010-03-29 blanchet 2010-03-29 added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
2010-03-29 blanchet 2010-03-29 made "theory_const" a Sledgehammer option; by default, it's true for SPASS and false for the others. This eliminates the need for the "spass_no_tc" ATP, which can be obtained by passing "no_theory_const" instead.
2010-03-29 blanchet 2010-03-29 added "respect_no_atp" and "convergence" options to Sledgehammer; these were previously hard-coded in "sledgehammer_fact_filter.ML"
2010-03-28 wenzelm 2010-03-28 static defaults for configuration options;
2010-03-24 blanchet 2010-03-24 added support for Sledgehammer parameters; this change goes hand in hand with f8c738abaed8
2010-03-22 blanchet 2010-03-22 start work on direct proof reconstruction for Sledgehammer
2010-03-19 blanchet 2010-03-19 renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar"; "full" sounds like "full types" or something, not like a structured Isar proof -- at some point I hope to make this an option that's orthogonal to the prover
2010-03-19 blanchet 2010-03-19 move all ATP setup code into ATP_Wrapper
2010-03-19 blanchet 2010-03-19 more Sledgehammer refactoring
2010-03-17 blanchet 2010-03-17 renamed Sledgehammer structures
2010-03-04 wenzelm 2010-03-04 basic simplification of external_prover signature;
2010-02-06 wenzelm 2010-02-06 renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
2009-10-29 wenzelm 2009-10-29 modernized some structure names;
2009-10-27 boehmes 2009-10-27 measure runtime of ATPs only if requested
2009-10-23 boehmes 2009-10-23 ignore error messages produced by ATPs
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 clarified File.platform_path vs. File.shell_path; tuned;
2009-10-15 wenzelm 2009-10-15 misc tuning and recovery of Isabelle coding style;
2009-10-15 wenzelm 2009-10-15 eliminated extraneous wrapping of public records; tuned;
2009-10-14 wenzelm 2009-10-14 modernized structure names;
2009-10-04 boehmes 2009-10-04 recovered support for Spass: re-enabled writing problems in DFG format
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-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-09-17 boehmes 2009-09-17 undo changes from revision 719426c9e1eb: removed Perl script for ATP invocation, measuring time using Bash-builtin "time"; new "eproof" script written in Perl (hopefully more stable than the one coming with E)
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-03 boehmes 2009-09-03 added runtime information to sledgehammer
2009-08-31 boehmes 2009-08-31 sledgehammer's temporary files are removed properly (even in case of an exception occurs)
2009-08-29 boehmes 2009-08-29 propagate theorem names, in addition to generated return message
2009-08-04 wenzelm 2009-08-04 src/HOL/Tools/ATP_Manager as separate component, with (almost) everything in one place;