| Tue, 19 Aug 2014 17:00:44 +0200 |
wenzelm |
added PARALLEL_ALLGOALS convenience;
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 20:33:56 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Tue, 18 Feb 2014 20:32:58 +0100 |
wenzelm |
tuned message;
|
file |
diff |
annotate
|
| Sat, 11 Jan 2014 21:39:21 +0100 |
wenzelm |
reactivate Thm.check_hyps, after adapting AFP/Datatype_Order_Generator (see AFP/b7e389b5765c);
|
file |
diff |
annotate
|
| Sat, 11 Jan 2014 20:06:31 +0100 |
wenzelm |
check_hyps for attribute application (still inactive, due to non-compliant tools);
|
file |
diff |
annotate
|
| Sat, 11 Jan 2014 17:05:03 +0100 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| 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');
|
file |
diff |
annotate
|
| Fri, 10 Jan 2014 21:37:28 +0100 |
wenzelm |
more elementary management of declared hyps, below structure Assumption;
|
file |
diff |
annotate
|
| Fri, 10 Jan 2014 16:20:06 +0100 |
wenzelm |
explicit check of background theory;
|
file |
diff |
annotate
|
| Tue, 31 Dec 2013 14:29:16 +0100 |
wenzelm |
proper context for norm_hhf and derived operations;
|
file |
diff |
annotate
|
| Sat, 14 Dec 2013 17:28:05 +0100 |
wenzelm |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Sun, 25 Aug 2013 20:32:26 +0200 |
wenzelm |
maintain goal forks as part of global execution;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Mon, 29 Jul 2013 18:59:58 +0200 |
wenzelm |
keep memo_exec execution running, which is important to cancel goal forks eventually;
|
file |
diff |
annotate
|
| Mon, 29 Jul 2013 14:18:57 +0200 |
wenzelm |
actually purge removed goal futures -- avoid memory leak;
|
file |
diff |
annotate
|
| Mon, 29 Jul 2013 13:43:43 +0200 |
wenzelm |
tuned -- less redundant data structure;
|
file |
diff |
annotate
|
| Mon, 29 Jul 2013 13:24:15 +0200 |
wenzelm |
discontinued notion of "stable" result -- running execution is never canceled;
|
file |
diff |
annotate
|
| Sat, 27 Jul 2013 20:27:25 +0200 |
wenzelm |
clarified Goal.stable_futures after 00170ef1dc39: running tasks are considered stable, without potentially blocking join;
|
file |
diff |
annotate
|
| Sat, 27 Jul 2013 16:35:51 +0200 |
wenzelm |
standardized aliases;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Fri, 12 Jul 2013 12:04:16 +0200 |
wenzelm |
clarified execution: maintain running execs only, check "stable" separately via memo (again);
|
file |
diff |
annotate
|
| Tue, 02 Jul 2013 14:48:01 +0200 |
wenzelm |
clarified Proofterm.proofs vs. Goal.skip_proofs;
|
file |
diff |
annotate
|
| Thu, 27 Jun 2013 10:08:41 +0200 |
wenzelm |
more scalable PARALLEL_GOALS, using more elementary retrofit;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Wed, 26 Jun 2013 11:54:45 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 29 May 2013 18:25:11 +0200 |
wenzelm |
tuned signature -- more explicit flags for low-level Thm.bicompose;
|
file |
diff |
annotate
|
| Tue, 21 May 2013 17:55:28 +0200 |
wenzelm |
proper options;
|
file |
diff |
annotate
|
| Fri, 17 May 2013 20:41:45 +0200 |
wenzelm |
proper option quick_and_dirty;
|
file |
diff |
annotate
|
| Mon, 13 May 2013 12:40:17 +0200 |
wenzelm |
retain goal display options when printing error messages, to avoid breakdown for huge goals;
|
file |
diff |
annotate
|
| Wed, 03 Apr 2013 22:30:25 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 03 Apr 2013 22:05:24 +0200 |
wenzelm |
recover implicit thread position for status messages (cf. eca8acb42e4a);
|
file |
diff |
annotate
|
| Wed, 03 Apr 2013 21:30:32 +0200 |
wenzelm |
more explicit Goal.fork_params -- avoid implicit arguments via thread data;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Wed, 27 Mar 2013 14:50:30 +0100 |
wenzelm |
clarified Skip_Proof.cheat_tac: more standard tactic;
|
file |
diff |
annotate
|
| Wed, 27 Mar 2013 14:19:18 +0100 |
wenzelm |
tuned signature and module arrangement;
|
file |
diff |
annotate
|
| Wed, 13 Mar 2013 21:25:08 +0100 |
wenzelm |
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
|
file |
diff |
annotate
|
| Mon, 25 Feb 2013 17:47:32 +0100 |
wenzelm |
more explicit Goal.shutdown_futures;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Thu, 14 Feb 2013 15:34:33 +0100 |
wenzelm |
tuned signature -- legacy packages might want to fork proofs as well;
|
file |
diff |
annotate
|
| Wed, 13 Feb 2013 21:53:02 +0100 |
wenzelm |
clarified default according to etc/options;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Wed, 16 Jan 2013 16:26:36 +0100 |
wenzelm |
more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
|
file |
diff |
annotate
|
| Sun, 25 Nov 2012 19:49:24 +0100 |
wenzelm |
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
|
file |
diff |
annotate
|
| Thu, 18 Oct 2012 19:58:30 +0200 |
wenzelm |
more basic Goal.reset_futures as snapshot of implicit state;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Sat, 13 Oct 2012 19:53:04 +0200 |
wenzelm |
some attempts to unify/simplify pretty_goal;
|
file |
diff |
annotate
|
| Sat, 13 Oct 2012 16:19:16 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Fri, 12 Oct 2012 13:46:41 +0200 |
wenzelm |
do not treat interrupt as error here, to avoid confusion in log etc.;
|
file |
diff |
annotate
|
| Sat, 01 Sep 2012 19:27:28 +0200 |
wenzelm |
central management of forked goals wrt. transaction id;
|
file |
diff |
annotate
|
| Fri, 31 Aug 2012 15:25:26 +0200 |
wenzelm |
more informative error message from failed goal forks (violating old-style TTY protocol!);
|
file |
diff |
annotate
|
| Fri, 31 Aug 2012 14:35:04 +0200 |
wenzelm |
more markup for failed goal forks, reusing "bad";
|
file |
diff |
annotate
|
| Fri, 31 Aug 2012 13:23:25 +0200 |
wenzelm |
further refinement of command status, to accomodate forked proofs;
|
file |
diff |
annotate
|
| Thu, 30 Aug 2012 21:23:04 +0200 |
wenzelm |
refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
|
file |
diff |
annotate
|