src/Pure/goal.ML
Tue, 10 Apr 2012 20:42:17 +0200 wenzelm tuned future priorities: print 0, goal ~1, execute ~2;
Fri, 11 Nov 2011 16:25:32 +0100 wenzelm depth-first proof forking for improved locality (wrt. cancellation and overall memory usage);
Sat, 05 Nov 2011 15:00:49 +0100 wenzelm added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
Fri, 19 Aug 2011 18:01:23 +0200 wenzelm tuned;
Wed, 10 Aug 2011 16:24:39 +0200 wenzelm Goal.forked: clarified handling of interrupts;
Wed, 10 Aug 2011 16:05:14 +0200 wenzelm future_job: explicit indication of interrupts;
Wed, 27 Apr 2011 21:50:04 +0200 wenzelm clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;
Sat, 16 Apr 2011 23:38:25 +0200 wenzelm enable PARALLEL_GOALS more liberally, unlike forked proofs (cf. 34b9652b2f45);
Sat, 16 Apr 2011 22:21:34 +0200 wenzelm refined PARALLEL_GOALS;
Sat, 16 Apr 2011 15:47:52 +0200 wenzelm modernized structure Proof_Context;
Tue, 22 Feb 2011 19:44:15 +0100 wenzelm scale parallel_proofs_threshold with max_threads_value to improve saturation of cores;
Fri, 18 Feb 2011 16:11:58 +0100 wenzelm less verbose tracing;
Fri, 04 Feb 2011 17:11:00 +0100 wenzelm parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
Wed, 02 Feb 2011 15:04:09 +0100 wenzelm maintain Task_Queue.group within Task_Queue.task;
Mon, 31 Jan 2011 23:53:07 +0100 wenzelm more specific Goal.fork_name;
Mon, 31 Jan 2011 23:02:53 +0100 wenzelm tuned signature;
Mon, 31 Jan 2011 22:57:01 +0100 wenzelm support named tasks, for improved tracing;
Fri, 17 Dec 2010 17:08:56 +0100 wenzelm renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
Fri, 03 Sep 2010 21:13:53 +0200 wenzelm pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
Mon, 30 Aug 2010 15:19:39 +0200 wenzelm tuned messages: discontinued spurious full-stops (messages are occasionally composed unexpectedly);
Sun, 08 Aug 2010 19:36:31 +0200 wenzelm explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
Fri, 06 Aug 2010 14:35:04 +0200 wenzelm removed obsolete Goal.local_future_enforced: Toplevel.run_command is no longer interactive, so Goal.local_future_enabled is sufficient (cf. 349e9223c685 and e07dacec79e7);
Sun, 04 Jul 2010 21:01:22 +0200 wenzelm general Future.report -- also for Toplevel.async_state;
Sat, 29 May 2010 19:46:29 +0200 wenzelm explicit markup for forked goals, as indicated by Goal.fork;
Mon, 03 May 2010 15:34:55 +0200 wenzelm simplified primitive Thm.future: more direct theory check, do not hardwire strip_shyps here;
Mon, 03 May 2010 14:25:56 +0200 wenzelm renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
Sat, 20 Mar 2010 17:33:11 +0100 wenzelm renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
Sun, 07 Feb 2010 19:33:34 +0100 wenzelm renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
Thu, 19 Nov 2009 17:29:39 +0100 wenzelm future_result: purge flexflex pairs, which should normally be trivial anyway -- prevent Thm.future_result from complaining about tpairs;
Wed, 30 Sep 2009 22:26:47 +0200 wenzelm PARALLEL_GOALS: proper scope for exception FAILED, with dummy argument to prevent its interpretation as variable;
Tue, 29 Sep 2009 11:49:22 +0200 wenzelm explicit indication of Unsynchronized.ref;
Wed, 12 Aug 2009 00:26:01 +0200 wenzelm added PARALLEL_CHOICE, PARALLEL_GOALS;
Tue, 28 Jul 2009 16:30:23 +0200 wenzelm eliminated separate Future.enabled -- let Future.join fail explicitly in critical section, instead of entering sequential mode silently;
Sun, 26 Jul 2009 13:12:52 +0200 wenzelm Goal.finish: explicit context for printing;
Sat, 25 Jul 2009 10:31:27 +0200 wenzelm renamed structure Display_Goal to Goal_Display;
Thu, 23 Jul 2009 16:52:16 +0200 wenzelm clarified pretty_goals, pretty_thm_aux: plain context;
Mon, 20 Jul 2009 21:20:09 +0200 wenzelm moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
Mon, 20 Jul 2009 00:37:39 +0200 wenzelm Proof.future_proof: declare all assumptions as well;
Sun, 19 Jul 2009 19:24:04 +0200 wenzelm parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
Sun, 19 Jul 2009 18:02:40 +0200 wenzelm more abstract Future.is_worker;
Sun, 19 Jul 2009 14:15:47 +0200 wenzelm future_result: explicitly impose Variable.sorts_of again;
Thu, 12 Mar 2009 15:54:58 +0100 wenzelm Assumption.all_prems_of, Assumption.all_assms_of;
Sun, 11 Jan 2009 18:18:35 +0100 wenzelm added Goal.future_enabled abstraction -- now also checks that this is already
Sat, 10 Jan 2009 21:32:30 +0100 wenzelm added parallel_proofs flag (default true, cf. usedir option -Q), which can be disabled in low-memory situations;
Sun, 04 Jan 2009 15:28:40 +0100 wenzelm tuned protect, conclude: Drule.comp_no_flatten;
Sun, 04 Jan 2009 00:01:16 +0100 wenzelm future proofs: back to Future.fork_pri ~1 for improved parallelism;
Tue, 16 Dec 2008 18:04:16 +0100 wenzelm future proofs: Future.fork_pri 1 minimizes queue length and pending promises
Tue, 16 Dec 2008 16:25:19 +0100 wenzelm Future.fork_pri;
Fri, 12 Dec 2008 12:14:02 +0100 wenzelm future proofs: more robust check via Future.enabled;
Thu, 04 Dec 2008 23:00:58 +0100 wenzelm future proofs: pass actual futures to facilitate composite computations;
Thu, 16 Oct 2008 22:44:28 +0200 wenzelm prove_common: include all sorts from context into statement, check shyps of result;
Wed, 01 Oct 2008 12:18:18 +0200 wenzelm renamed promise to future, tuned related interfaces;
Thu, 25 Sep 2008 20:34:18 +0200 wenzelm simplified Thm.promise;
Thu, 25 Sep 2008 14:35:01 +0200 wenzelm prove: error with original thread position;
Tue, 23 Sep 2008 23:07:48 +0200 wenzelm prove_multi: immediate;
Tue, 23 Sep 2008 22:04:30 +0200 wenzelm added promise_result, prove_promise;
Sat, 14 Jun 2008 23:20:11 +0200 wenzelm prove: full Variable.declare_term, including constraints;
Sun, 18 May 2008 15:04:09 +0200 wenzelm moved global pretty/string_of functions from Sign to Syntax;
Thu, 17 Apr 2008 22:22:25 +0200 wenzelm prove_global: Variable.set_body true, pass context;
Sat, 12 Apr 2008 17:00:40 +0200 wenzelm replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
less more (0) -60 tip