src/Pure/goal.ML
Fri, 30 Oct 2015 17:14:30 +0100 wenzelm tuned signature -- clarified modules;
Fri, 23 Oct 2015 17:17:11 +0200 wenzelm clarified modules;
Sun, 16 Aug 2015 18:19:30 +0200 wenzelm prefer theory_id operations;
Tue, 28 Jul 2015 20:05:53 +0200 wenzelm proper context;
Tue, 14 Jul 2015 19:01:46 +0200 wenzelm more aggressive compaction of multi-goal proof terms (see also a8babbb6d5ea, 4dd0ba632e40);
Tue, 14 Jul 2015 11:29:43 +0200 wenzelm normalize proof before splitting conjunctions, according to Proof.conclude_goal (see also 4dd0ba632e40) -- may reduce general resource usage;
Wed, 08 Jul 2015 19:28:43 +0200 wenzelm Variable.focus etc.: optional bindings provided by user;
Sun, 05 Jul 2015 15:02:30 +0200 wenzelm simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
Fri, 06 Mar 2015 17:32:20 +0100 wenzelm clarified context;
Fri, 06 Mar 2015 15:58:56 +0100 wenzelm Thm.cterm_of and Thm.ctyp_of operate on local context;
Thu, 05 Mar 2015 13:28:04 +0100 wenzelm tuned -- more explicit use of context;
Wed, 04 Mar 2015 19:53:18 +0100 wenzelm tuned signature -- prefer qualified names;
Mon, 23 Feb 2015 14:50:30 +0100 wenzelm Goal.prove_multi is superseded by the fully general Goal.prove_common;
Tue, 10 Feb 2015 14:48:26 +0100 wenzelm proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
Mon, 10 Nov 2014 21:49:48 +0100 wenzelm proper context for assume_tac (atac remains as fall-back without context);
Sat, 08 Nov 2014 21:31:51 +0100 wenzelm optional proof context for unify operations, for the sake of proper local options;
Thu, 30 Oct 2014 16:20:46 +0100 wenzelm eliminated aliases;
Tue, 19 Aug 2014 18:11:04 +0200 wenzelm clarified modules;
Tue, 19 Aug 2014 17:00:44 +0200 wenzelm added PARALLEL_ALLGOALS convenience;
Fri, 21 Mar 2014 20:33:56 +0100 wenzelm more qualified names;
Tue, 18 Feb 2014 20:32:58 +0100 wenzelm tuned message;
Sat, 11 Jan 2014 21:39:21 +0100 wenzelm reactivate Thm.check_hyps, after adapting AFP/Datatype_Order_Generator (see AFP/b7e389b5765c);
Sat, 11 Jan 2014 20:06:31 +0100 wenzelm check_hyps for attribute application (still inactive, due to non-compliant tools);
Sat, 11 Jan 2014 17:05:03 +0100 wenzelm clarified context;
Fri, 10 Jan 2014 23:42:18 +0100 wenzelm disable Thm.check_hyps for now, due to remaining problems with AFP/Datatype_Order_Generator and AFP/Psi_Calculi (because of HOL-Nominal 'equivariance');
Fri, 10 Jan 2014 21:37:28 +0100 wenzelm more elementary management of declared hyps, below structure Assumption;
Fri, 10 Jan 2014 16:20:06 +0100 wenzelm explicit check of background theory;
Tue, 31 Dec 2013 14:29:16 +0100 wenzelm proper context for norm_hhf and derived operations;
Sat, 14 Dec 2013 17:28:05 +0100 wenzelm proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
Sat, 23 Nov 2013 17:15:44 +0100 wenzelm more uniform / rigid checking of Goal.prove_common vs. Proof.conclude_goal -- NB: Goal.prove_common cannot check hyps right now, e.g. due to undeclared Simplifier prems;
Sun, 25 Aug 2013 20:32:26 +0200 wenzelm maintain goal forks as part of global execution;
Sun, 25 Aug 2013 17:04:22 +0200 wenzelm simplified Goal.forked_proofs: status is determined via group instead of dummy future (see also Pure/PIDE/execution.ML);
Sun, 25 Aug 2013 16:03:12 +0200 wenzelm discontinued parallel_subproofs_saturation and related internal counters (superseded by parallel_subproofs_threshold and timing information);
Wed, 31 Jul 2013 13:00:42 +0200 wenzelm clarified priority of "skipped" proofs, which might take long but do not produce relevant information (potential conflict of quick interactive feedback vs. performance in batch mode);
Mon, 29 Jul 2013 18:59:58 +0200 wenzelm keep memo_exec execution running, which is important to cancel goal forks eventually;
Mon, 29 Jul 2013 14:18:57 +0200 wenzelm actually purge removed goal futures -- avoid memory leak;
Mon, 29 Jul 2013 13:43:43 +0200 wenzelm tuned -- less redundant data structure;
Mon, 29 Jul 2013 13:24:15 +0200 wenzelm discontinued notion of "stable" result -- running execution is never canceled;
Sat, 27 Jul 2013 20:27:25 +0200 wenzelm clarified Goal.stable_futures after 00170ef1dc39: running tasks are considered stable, without potentially blocking join;
Sat, 27 Jul 2013 16:35:51 +0200 wenzelm standardized aliases;
Fri, 19 Jul 2013 17:58:57 +0200 wenzelm just one option "skip_proofs", without direct access within the editor (it makes document processing stateful without strong reasons -- monotonic updates already handle goal forks smoothly);
Thu, 18 Jul 2013 13:12:54 +0200 wenzelm immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 -> 100000, JinjaThreads: 65000 -> 300000) -- minimal measurable impact on inference kernel performance;
Fri, 12 Jul 2013 12:04:16 +0200 wenzelm clarified execution: maintain running execs only, check "stable" separately via memo (again);
Tue, 02 Jul 2013 14:48:01 +0200 wenzelm clarified Proofterm.proofs vs. Goal.skip_proofs;
Thu, 27 Jun 2013 10:08:41 +0200 wenzelm more scalable PARALLEL_GOALS, using more elementary retrofit;
Wed, 26 Jun 2013 21:48:23 +0200 wenzelm less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
Wed, 26 Jun 2013 11:54:45 +0200 wenzelm tuned signature;
Wed, 29 May 2013 18:25:11 +0200 wenzelm tuned signature -- more explicit flags for low-level Thm.bicompose;
Tue, 21 May 2013 17:55:28 +0200 wenzelm proper options;
Fri, 17 May 2013 20:41:45 +0200 wenzelm proper option quick_and_dirty;
Mon, 13 May 2013 12:40:17 +0200 wenzelm retain goal display options when printing error messages, to avoid breakdown for huge goals;
Wed, 03 Apr 2013 22:30:25 +0200 wenzelm tuned;
Wed, 03 Apr 2013 22:05:24 +0200 wenzelm recover implicit thread position for status messages (cf. eca8acb42e4a);
Wed, 03 Apr 2013 21:30:32 +0200 wenzelm more explicit Goal.fork_params -- avoid implicit arguments via thread data;
Wed, 27 Mar 2013 16:38:25 +0100 wenzelm more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
Wed, 27 Mar 2013 14:50:30 +0100 wenzelm clarified Skip_Proof.cheat_tac: more standard tactic;
Wed, 27 Mar 2013 14:19:18 +0100 wenzelm tuned signature and module arrangement;
Wed, 13 Mar 2013 21:25:08 +0100 wenzelm clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
Mon, 25 Feb 2013 17:47:32 +0100 wenzelm more explicit Goal.shutdown_futures;
Tue, 19 Feb 2013 17:55:26 +0100 wenzelm improved scheduling of forked proofs, based on elapsed time estimate (from last run via session log file);
Thu, 14 Feb 2013 15:34:33 +0100 wenzelm tuned signature -- legacy packages might want to fork proofs as well;
Wed, 13 Feb 2013 21:53:02 +0100 wenzelm clarified default according to etc/options;
Sat, 19 Jan 2013 22:17:26 +0100 wenzelm always close derivation at the bottom of forked proofs (despite increased non-determinism of proof terms) -- improve parallel performance by avoiding dynamic dependency within large Isar proofs, e.g. Slicing/JinjaVM/SemanticsWF.thy in AFP/bf9b14cbc707;
Fri, 18 Jan 2013 16:20:09 +0100 wenzelm added "tasks_proof" statistics, via slighly odd global reference Future.forked_proofs (NB: Future.report_status is intertwined with scheduler thread);
Wed, 16 Jan 2013 20:41:29 +0100 wenzelm identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
Wed, 16 Jan 2013 16:26:36 +0100 wenzelm more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
Sun, 25 Nov 2012 19:49:24 +0100 wenzelm Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
Thu, 18 Oct 2012 19:58:30 +0200 wenzelm more basic Goal.reset_futures as snapshot of implicit state;
Wed, 17 Oct 2012 21:04:51 +0200 wenzelm more robust Session.finish (batch mode): use Goal.finish_futures to exhibit remaining failures of disconnected goal forks (e.g. from unnamed theorems) and Goal.cancel_futures the purge the persistent state;
Sat, 13 Oct 2012 19:53:04 +0200 wenzelm some attempts to unify/simplify pretty_goal;
Sat, 13 Oct 2012 16:19:16 +0200 wenzelm tuned signature;
Fri, 12 Oct 2012 13:55:13 +0200 wenzelm no special treatment of errors inside goal forks without transaction id, to avoid duplication in plain build with sequential log, for example;
Fri, 12 Oct 2012 13:46:41 +0200 wenzelm do not treat interrupt as error here, to avoid confusion in log etc.;
Sat, 01 Sep 2012 19:27:28 +0200 wenzelm central management of forked goals wrt. transaction id;
Fri, 31 Aug 2012 15:25:26 +0200 wenzelm more informative error message from failed goal forks (violating old-style TTY protocol!);
Fri, 31 Aug 2012 14:35:04 +0200 wenzelm more markup for failed goal forks, reusing "bad";
Fri, 31 Aug 2012 13:23:25 +0200 wenzelm further refinement of command status, to accomodate forked proofs;
Thu, 30 Aug 2012 21:23:04 +0200 wenzelm refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
Thu, 30 Aug 2012 15:26:37 +0200 wenzelm refined status of forked goals;
Wed, 29 Aug 2012 11:48:45 +0200 wenzelm renamed Position.str_of to Position.here;
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;
less more (0) -120 tip