src/HOL/Tools/atp_manager.ML
2009-06-24 nipkow 2009-06-24 New ATP option: full types
2009-06-22 immler 2009-06-22 use results of relevance-filter to determine additional clauses; (needed for minimize to be able to prove the same problems as sledgehammer)
2009-06-03 immler 2009-06-03 split preparing clauses and writing problemfile; included results of count_constants in return-type of prover; optionally pass counted constants to prover; removed unused external_prover from signature
2009-06-02 wenzelm 2009-06-02 made SML/NJ happy;
2009-05-04 immler 2009-05-04 added Philipp Meyer's implementation of AtpMinimal together with related changes in the sledgehammer-interface: adapted type of prover, optional relevance filtering, public get_prover for registered atps in AtpManager, included atp_minimize in s/h response;
2009-04-25 wenzelm 2009-04-25 use predefined preferences categories;
2009-03-31 immler 2009-03-31 included managing_thread in state of AtpManager: synchronized termination and check for running managing_thread
2009-03-30 wenzelm 2009-03-30 tuned spacing and formatting;
2009-03-30 immler 2009-03-30 terminate watching thread
2009-03-14 immler 2009-03-14 use goal instead of Proof State
2009-02-03 immler 2009-02-03 changed default timeout
2009-01-23 immler 2009-01-23 moved all output to watcher-thread
2009-01-21 immler 2009-01-21 2 provers
2009-01-20 immler 2009-01-20 do not interrupt successful thread
2009-01-20 immler 2009-01-20 cancel whole group
2009-01-20 immler 2009-01-20 pass timeout to prover; especially to remote-script
2009-01-20 immler 2009-01-20 typo
2009-01-20 immler 2009-01-20 modified remote script; modified handling of errors
2008-12-22 wenzelm 2008-12-22 unregister: refrain from cancelling self, which sometimes caused sledghammer to fail just before printing the result; tuned;
2008-12-15 wenzelm 2008-12-15 tuned messages;
2008-12-15 wenzelm 2008-12-15 added 'atp_messages' command, which displays recent messages synchronously;
2008-11-18 wenzelm 2008-11-18 changes by Fabian Immler: improved handling of prover errors; explicit treatment of clauses that are too trivial for resolution;
2008-10-14 wenzelm 2008-10-14 add_prover: plain prover function, without thread; removed obsolete atp_thread interface; moved kill_excessive into main thread manager loop -- avoids race condition wrt. register/unregister; start_prover: register/unregister self -- avoids race condition;
2008-10-14 wenzelm 2008-10-14 adding preferences is now permissive, no error handling here; tuned messages;
2008-10-14 wenzelm 2008-10-14 renamed kill_all to kill, in conformance with atp_kill command; simplified/unified treatment of preferences; check_thread_manager: CRITICAL due to global ref; goal addressing via Thm.cprem_of; reduced NJ basis library stuff to bare minimum;
2008-10-14 wenzelm 2008-10-14 info: back to plain printing; maintain state as Synchronized.var (cf. Pure/Concurrent/synchronized.ML); turned start into check_thread_manager, which forks the managing thread on demand; simplified heap operations; default preferences: only include e prover, which is most likely to be installed; misc simplifcation and tuning;
2008-10-13 wenzelm 2008-10-13 ** Update from Fabian ** preferences/provers: separated by white space, avoid low-level char type; sledgehammer command accepts prover list as well; avoid I/O in critical section of AtpManager.info; more systematic synchronization using higher-order combinators; more descriptive errors when atp fails; keep explicitly requested problem files; added remote prover functions; simplified treatment of prover name in diagnostic output; misc tuning and cleanup;
2008-10-09 wenzelm 2008-10-09 SimpleThread.interrupt;
2008-10-03 wenzelm 2008-10-03 do not handle Error (which matches arbitrary exceptions!), but ERROR _;
2008-10-03 wenzelm 2008-10-03 misc simplifcation and tuning; no export of structure Provers; added add_provers, print_provers; operate on Proof.state, not Toplevel.state; use Time.+ etc. to make SML/XL of NJ happy; explicit Isar commands 'atp_kill', 'atp_info', 'print_atps';
2008-10-03 wenzelm 2008-10-03 simplified thread creation via SimpleThread; managing_thread: option type (fork of inactive thread assumes threads are available in the first place);
2008-10-03 wenzelm 2008-10-03 version of sledgehammer using threads instead of processes, misc cleanup; (by Fabian Immler);