src/Pure/goal.ML
2013-06-27 wenzelm 2013-06-27 more scalable PARALLEL_GOALS, using more elementary retrofit; tuned signature;
2013-06-26 wenzelm 2013-06-26 less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context; even less intrusive PREFER_GOAL (without structural goal marker), e.g. relevant for generic_simp_tac; adapted ZF proof that broke for unknown reasons (potentially slight change of Drule.size_of_thm);
2013-06-26 wenzelm 2013-06-26 tuned signature;
2013-05-29 wenzelm 2013-05-29 tuned signature -- more explicit flags for low-level Thm.bicompose;
2013-05-21 wenzelm 2013-05-21 proper options;
2013-05-17 wenzelm 2013-05-17 proper option quick_and_dirty;
2013-05-13 wenzelm 2013-05-13 retain goal display options when printing error messages, to avoid breakdown for huge goals;
2013-04-03 wenzelm 2013-04-03 tuned;
2013-04-03 wenzelm 2013-04-03 recover implicit thread position for status messages (cf. eca8acb42e4a);
2013-04-03 wenzelm 2013-04-03 more explicit Goal.fork_params -- avoid implicit arguments via thread data; actually fork terminal proofs in interactive mode (amending 8707df0b0255);
2013-03-27 wenzelm 2013-03-27 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);
2013-03-27 wenzelm 2013-03-27 clarified Skip_Proof.cheat_tac: more standard tactic; clarified Method.cheating: check quick_and_dirty when it is actually applied;
2013-03-27 wenzelm 2013-03-27 tuned signature and module arrangement;
2013-03-13 wenzelm 2013-03-13 clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate); clarified unknown timing vs. zero timing; tuned;
2013-02-25 wenzelm 2013-02-25 more explicit Goal.shutdown_futures;
2013-02-19 wenzelm 2013-02-19 improved scheduling of forked proofs, based on elapsed time estimate (from last run via session log file);
2013-02-14 wenzelm 2013-02-14 tuned signature -- legacy packages might want to fork proofs as well;
2013-02-13 wenzelm 2013-02-13 clarified default according to etc/options;
2013-01-19 wenzelm 2013-01-19 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;
2013-01-18 wenzelm 2013-01-18 added "tasks_proof" statistics, via slighly odd global reference Future.forked_proofs (NB: Future.report_status is intertwined with scheduler thread);
2013-01-16 wenzelm 2013-01-16 identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
2013-01-16 wenzelm 2013-01-16 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
2012-11-25 wenzelm 2012-11-25 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-10-18 wenzelm 2012-10-18 more basic Goal.reset_futures as snapshot of implicit state; more robust Session.finish_futures: do not cancel here, to allow later Future.map of persistent futures (notably proof terms);
2012-10-17 wenzelm 2012-10-17 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;
2012-10-13 wenzelm 2012-10-13 some attempts to unify/simplify pretty_goal;
2012-10-13 wenzelm 2012-10-13 tuned signature;
2012-10-12 wenzelm 2012-10-12 no special treatment of errors inside goal forks without transaction id, to avoid duplication in plain build with sequential log, for example;
2012-10-12 wenzelm 2012-10-12 do not treat interrupt as error here, to avoid confusion in log etc.;
2012-09-01 wenzelm 2012-09-01 central management of forked goals wrt. transaction id; clarified stable_exec_id: consider ragular failure as stable; more robust counting of forked proofs, with global reset after cancellation due to document editing;
2012-08-31 wenzelm 2012-08-31 more informative error message from failed goal forks (violating old-style TTY protocol!);
2012-08-31 wenzelm 2012-08-31 more markup for failed goal forks, reusing "bad";
2012-08-31 wenzelm 2012-08-31 further refinement of command status, to accomodate forked proofs;
2012-08-30 wenzelm 2012-08-30 refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390); stretched meaning of Goal.parallel_proofs to enable future_terminal_proofs in interactive document model, despite its lack for regular forking of proofs;
2012-08-30 wenzelm 2012-08-30 refined status of forked goals;
2012-08-29 wenzelm 2012-08-29 renamed Position.str_of to Position.here;
2012-04-10 wenzelm 2012-04-10 tuned future priorities: print 0, goal ~1, execute ~2;
2011-11-11 wenzelm 2011-11-11 depth-first proof forking for improved locality (wrt. cancellation and overall memory usage);
2011-11-05 wenzelm 2011-11-05 added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types; tuned;
2011-08-19 wenzelm 2011-08-19 tuned;
2011-08-10 wenzelm 2011-08-10 Goal.forked: clarified handling of interrupts;
2011-08-10 wenzelm 2011-08-10 future_job: explicit indication of interrupts;
2011-04-27 wenzelm 2011-04-27 clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;
2011-04-16 wenzelm 2011-04-16 enable PARALLEL_GOALS more liberally, unlike forked proofs (cf. 34b9652b2f45);
2011-04-16 wenzelm 2011-04-16 refined PARALLEL_GOALS;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-02-22 wenzelm 2011-02-22 scale parallel_proofs_threshold with max_threads_value to improve saturation of cores;
2011-02-18 wenzelm 2011-02-18 less verbose tracing;
2011-02-04 wenzelm 2011-02-04 parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
2011-02-02 wenzelm 2011-02-02 maintain Task_Queue.group within Task_Queue.task; Task_Queue.dummy_task: id = 0 in accordance to Document.no_id etc.; tuned signature;
2011-01-31 wenzelm 2011-01-31 more specific Goal.fork_name;
2011-01-31 wenzelm 2011-01-31 tuned signature; tuned vacous forks;
2011-01-31 wenzelm 2011-01-31 support named tasks, for improved tracing;
2010-12-17 wenzelm 2010-12-17 renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
2010-09-03 wenzelm 2010-09-03 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;
2010-08-30 wenzelm 2010-08-30 tuned messages: discontinued spurious full-stops (messages are occasionally composed unexpectedly);
2010-08-08 wenzelm 2010-08-08 explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
2010-08-06 wenzelm 2010-08-06 removed obsolete Goal.local_future_enforced: Toplevel.run_command is no longer interactive, so Goal.local_future_enabled is sufficient (cf. 349e9223c685 and e07dacec79e7);
2010-07-04 wenzelm 2010-07-04 general Future.report -- also for Toplevel.async_state;
2010-05-29 wenzelm 2010-05-29 explicit markup for forked goals, as indicated by Goal.fork; accumulate pending forks within command state and hilight accordingly; Isabelle_Process: enforce future_terminal_proof, which gives some impression of non-linear/parallel checking;