2010-04-23 blanchet 2010-04-23 move the Sledgehammer menu options to "sledgehammer_isar.ML"
2010-04-23 blanchet 2010-04-23 centralized ATP-specific error handling in "atp_wrapper.ML"
2010-04-23 blanchet 2010-04-23 handle ATP proof delimiters in a cleaner, more extensible fashion
2010-04-22 blanchet 2010-04-22 set "atps" reference's default value to "(remote_)e (remote_)spass (remote_)vampire", based on what is installed
2010-04-22 blanchet 2010-04-22 if Isar proof reconstruction is not supported, tell the user so they don't wonder why their "isar_proof" option did nothing
2010-04-22 blanchet 2010-04-22 "remote_e" and "remote_vampire" support TSTP proof output + fix "overlord" mode ATP output postprocessing
2010-04-22 blanchet 2010-04-22 postprocess ATP output in "overlord" mode to make it more readable
2010-04-21 blanchet 2010-04-21 failure of reconstructing the Isar proof (e.g., exception) should not prevent Sledgehammer from showing the short one-liner proof -- but in "debug" mode we do want to know what the exception is
2010-04-21 blanchet 2010-04-21 generate command-line in addition to timestamp in ATP output file, for debugging purposes
2010-04-21 blanchet 2010-04-21 pass relevant options from "sledgehammer" to "sledgehammer minimize"; one nice side effect of this change is that the "sledgehammer minimize" syntax now only occurs in "sledgehammer_isar.ML", instead of being spread across two files
2010-04-21 blanchet 2010-04-21 distinguish between the different ATP errors in the user interface; in particular, tell users to upgrade their SPASS if they try to run "spass_tptp" with an old SPASS version with no TPTP support
2010-04-21 blanchet 2010-04-21 added "spass_tptp" prover, which requires SPASS x.y > 3.0; once users have upgraded their SPASS and we have determined that "spass_tptp" works well, we can make "spass_tptp" the one and only "spass"
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;