| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
crude implementation of centralized slicing
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
take 'induction_rules' into consideration, as well as 'max_facts' even when 'only' is set
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
rationalize slicing format
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
thread slices through
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
rationalized output for forthcoming slicing model
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
use same default for FO and HO provers w.r.t. induction principles, based on evaluation -- this also simplifies the code
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
disable slicing within SMT (in preparation for factoring it out)
|
file |
diff |
annotate
|
| Sat, 22 Jan 2022 11:33:31 +0100 |
desharna |
added spying of fact filtering timing
|
file |
diff |
annotate
|
| Fri, 21 Jan 2022 16:17:42 +0100 |
desharna |
added syping of fact filtering time to sledgehammer
|
file |
diff |
annotate
|
| Sat, 18 Dec 2021 23:11:49 +0100 |
desharna |
tuned run_sledgehammer and called it directly from Mirabelle
|
file |
diff |
annotate
|
| Sat, 18 Dec 2021 14:30:13 +0100 |
desharna |
exported Sledgehammer.launch_prover and use it in Mirabelle
|
file |
diff |
annotate
|
| Sat, 18 Dec 2021 13:27:42 +0100 |
desharna |
proper filtering inf induction rules in Mirabelle
|
file |
diff |
annotate
|
| Fri, 17 Dec 2021 09:57:22 +0100 |
desharna |
added nearly_all_facts_of_context and uniformized its usage in Sledgehammer and Mirabelle
|
file |
diff |
annotate
|
| Tue, 13 Jul 2021 10:57:15 +0200 |
blanchet |
revisited ac28714b7478: more faithful preplaying with chained facts
|
file |
diff |
annotate
|
| Thu, 08 Jul 2021 17:23:01 +0200 |
desharna |
refactored Sledgehammer option "induction_rules"
|
file |
diff |
annotate
|
| Thu, 08 Jul 2021 15:25:30 +0200 |
desharna |
promoted "sledgehammer_instantiate_inducts" to proper option "induction_rules"
|
file |
diff |
annotate
|
| Fri, 05 Mar 2021 16:09:42 +0100 |
wenzelm |
clarified signature --- augment existing structure Time;
|
file |
diff |
annotate
|
| Thu, 22 Oct 2020 15:18:08 +0200 |
desharna |
Tuned isar_step datatype
|
file |
diff |
annotate
|
| Thu, 23 Apr 2020 16:52:14 +0200 |
blanchet |
avoid passing chained facts twice to preplay in Sledgehammer
|
file |
diff |
annotate
|
| Mon, 21 Jan 2019 22:29:41 +0100 |
blanchet |
get rid of visibility in MaSh -- it slows it down more than it helps
|
file |
diff |
annotate
|
| Sun, 14 Aug 2016 12:26:09 +0200 |
blanchet |
avoid loading MaSh file first time around for higher responsiveness of Sledgehammer
|
file |
diff |
annotate
|
| Sun, 14 Aug 2016 12:26:09 +0200 |
blanchet |
optimization in MaSh parsing
|
file |
diff |
annotate
|
| Sun, 14 Aug 2016 12:26:09 +0200 |
blanchet |
tuned ML
|
file |
diff |
annotate
|
| Sun, 14 Aug 2016 12:26:09 +0200 |
blanchet |
killed final stops in Sledgehammer and friends
|
file |
diff |
annotate
|
| Fri, 17 Jun 2016 12:40:18 +0200 |
blanchet |
be more careful before filtering out chained facts in Sledgehammer
|
file |
diff |
annotate
|
| Tue, 17 May 2016 08:40:24 +0200 |
blanchet |
proper consideration of chained facts in 'try0' minimization
|
file |
diff |
annotate
|
| Mon, 28 Mar 2016 12:05:47 +0200 |
blanchet |
a more generous hard timeout
|
file |
diff |
annotate
|
| Mon, 28 Mar 2016 12:05:47 +0200 |
blanchet |
early warning when Sledgehammer finds a proof
|
file |
diff |
annotate
|
| Sat, 05 Mar 2016 17:01:45 +0100 |
wenzelm |
tuned signature -- clarified modules;
|
file |
diff |
annotate
|
| Thu, 03 Mar 2016 15:23:02 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Mon, 01 Feb 2016 19:57:58 +0100 |
blanchet |
preplaying of 'smt' and 'metis' more in sync with actual method
|
file |
diff |
annotate
|
| Mon, 05 Oct 2015 23:03:50 +0200 |
blanchet |
further improved fine point w.r.t. replaying in the presence of chained facts and a non-empty meta-quantifier prefix + avoid printing internal names in backquotes
|
file |
diff |
annotate
|
| Fri, 02 Oct 2015 21:15:25 +0200 |
blanchet |
further reduced dependency on legacy async thread manager
|
file |
diff |
annotate
|
| Fri, 02 Oct 2015 21:06:32 +0200 |
blanchet |
removed legacy asynchronous mode in Sledgehammer
|
file |
diff |
annotate
|
| Mon, 21 Sep 2015 23:22:11 +0200 |
wenzelm |
clarified markup;
|
file |
diff |
annotate
|
| Mon, 29 Jun 2015 23:44:53 +0200 |
blanchet |
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
|
file |
diff |
annotate
|
| Mon, 22 Jun 2015 16:56:03 +0200 |
blanchet |
keep 'Pure.all' in goals when preplaying
|
file |
diff |
annotate
|
| Mon, 22 Jun 2015 16:56:03 +0200 |
blanchet |
use right context for preplay, to avoid errors in fact lookup
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Thu, 29 Jan 2015 16:35:29 +0100 |
wenzelm |
more explicit indication of Async_Manager_Legacy as Proof General legacy;
|
file |
diff |
annotate
|
| Tue, 23 Dec 2014 20:46:42 +0100 |
wenzelm |
explicit message channels for "state", "information";
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| Fri, 07 Nov 2014 16:36:55 +0100 |
wenzelm |
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
|
file |
diff |
annotate
|
| Thu, 06 Nov 2014 13:36:19 +0100 |
wenzelm |
prefer explicit Keyword.keywords;
|
file |
diff |
annotate
|
| Mon, 03 Nov 2014 14:31:15 +0100 |
wenzelm |
eliminated obsolete Proof.goal_message -- print outcome more directly;
|
file |
diff |
annotate
|
| Fri, 31 Oct 2014 11:36:41 +0100 |
wenzelm |
discontinued obsolete Output.urgent_message;
|
file |
diff |
annotate
|
| Tue, 30 Sep 2014 16:40:03 +0200 |
blanchet |
don't call 'hd' on a possibly empty list
|
file |
diff |
annotate
|
| Mon, 04 Aug 2014 13:06:24 +0200 |
blanchet |
default on 'metis' for ATPs if preplaying is disabled
|
file |
diff |
annotate
|
| Mon, 04 Aug 2014 12:52:48 +0200 |
blanchet |
more informative preplay failures
|
file |
diff |
annotate
|
| Mon, 04 Aug 2014 12:28:42 +0200 |
blanchet |
rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
|
file |
diff |
annotate
|
| Mon, 04 Aug 2014 11:43:19 +0200 |
blanchet |
honor 'dont_minimize' option when preplaying one-liner proof
|
file |
diff |
annotate
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
export ML function
|
file |
diff |
annotate
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
restored a bit of laziness
|
file |
diff |
annotate
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
further minimize one-liner
|
file |
diff |
annotate
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
eliminated needlessly complex message tail
|
file |
diff |
annotate
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
|
file |
diff |
annotate
|
| Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
rationalized preplaying by eliminating (now superfluous) laziness
|
file |
diff |
annotate
|
| Tue, 15 Jul 2014 00:21:32 +0200 |
blanchet |
record MaSh algorithm in spying data
|
file |
diff |
annotate
|
| Tue, 01 Jul 2014 16:47:10 +0200 |
blanchet |
tuned message
|
file |
diff |
annotate
|