2008-10-15 wenzelm 2008-10-15 generic ATP manager based on threads (by Fabian Immler);
2008-10-15 wenzelm 2008-10-15 added sledgehammer etc.;
2008-10-15 wenzelm 2008-10-15 removed obsolete Complex sessions;
2008-10-15 haftmann 2008-10-15 figure for adaption
2008-10-15 ballarin 2008-10-15 Removed 'includes' (fixed).
2008-10-15 ballarin 2008-10-15 Removed 'includes'.
2008-10-15 kleing 2008-10-15 give more time to do inital loggin and settings read
2008-10-15 kleing 2008-10-15 log start of test session
2008-10-14 wenzelm 2008-10-14 tuned interfaces -- plain prover function, without thread; misc tuning and simplification; reduced NJ basis library stuff to bare minimum;
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 tuned AtpWrapper interfaces;
2008-10-14 haftmann 2008-10-14 continued codegen tutorial
2008-10-14 wenzelm 2008-10-14 renamed AtpThread to AtpWrapper;
2008-10-14 wenzelm 2008-10-14 adding preferences is now permissive;
2008-10-14 wenzelm 2008-10-14 tuned;
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 CRITICAL access to preferences; tuned some interfaces;
2008-10-14 wenzelm 2008-10-14 export generic_pref etc.; CRITICAL access to preferences; misc cleanup, more conventional indentation;
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 tuned comments;
2008-10-14 nipkow 2008-10-14 added lemma
2008-10-14 nipkow 2008-10-14 Added liveness analysis
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-14 wenzelm 2008-10-14 added min_elem, upto;
2008-10-14 wenzelm 2008-10-14 added value; simplified synchronized variable access;
2008-10-14 wenzelm 2008-10-14 simplified synchronized variable access; tuned;
2008-10-13 wenzelm 2008-10-13 State variables with synchronized access.
2008-10-13 wenzelm 2008-10-13 added generic combinator for synchronized evaluation (formerly in future.ML);
2008-10-13 wenzelm 2008-10-13 simplified implementation using Synchronized.var;
2008-10-13 wenzelm 2008-10-13 SimpleThread.synchronized;
2008-10-13 wenzelm 2008-10-13 added Concurrent/synchronized.ML;
2008-10-13 wenzelm 2008-10-13 ** Update from Fabian ** added remote prover functions;
2008-10-13 wenzelm 2008-10-13 ** Update from Fabian ** reset print mode when producing proof text;
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-13 wenzelm 2008-10-13 tuned output;
2008-10-13 haftmann 2008-10-13 tuned
2008-10-13 urbanc 2008-10-13 tuned
2008-10-11 kleing 2008-10-11 change DISTPREFIX to not use yet another filesystem
2008-10-10 haftmann 2008-10-10 tuned
2008-10-10 haftmann 2008-10-10 tuned
2008-10-10 haftmann 2008-10-10 tuned
2008-10-10 haftmann 2008-10-10 tuned
2008-10-10 haftmann 2008-10-10 `code func` now just `code`
2008-10-10 haftmann 2008-10-10 some adaption
2008-10-10 haftmann 2008-10-10 using tikz pictures
2008-10-10 haftmann 2008-10-10 tuned default rules of (dvd)
2008-10-09 wenzelm 2008-10-09 replaced str_of by general peek;
2008-10-09 wenzelm 2008-10-09 extra Poly/ML toplevel pretty printing in ML-Systems/install_pp_polyml.ML;
2008-10-09 wenzelm 2008-10-09 fixed spelling;
2008-10-09 wenzelm 2008-10-09 added enabled; removed pseudo-parallel version of profile -- CRITICAL prevents future join;
2008-10-09 wenzelm 2008-10-09 added enabled;
2008-10-09 wenzelm 2008-10-09 Multithreading.enabled;
2008-10-09 wenzelm 2008-10-09 moved future_scheduler flag to Concurrent/ROOT.ML;
2008-10-09 wenzelm 2008-10-09 added invalidate_group; SimpleThread.interrupt;
2008-10-09 wenzelm 2008-10-09 added fail-safe interrupt;
2008-10-09 wenzelm 2008-10-09 subject to Multithreading.enabled; raw_map: join sequentially, less overhead;
2008-10-09 wenzelm 2008-10-09 future result: Interrupt invalidates group, but pretends success otherwise;
2008-10-09 wenzelm 2008-10-09 added future_scheduler flag (tmp!), from skip_proofs.ML; added Concurrent/par_list_dummy.ML;
2008-10-09 wenzelm 2008-10-09 Dummy version of parallel list combinators -- plain sequential evaluation.
2008-10-09 wenzelm 2008-10-09 added Concurrent/par_list_dummy.ML;