| Fri, 07 Jun 2024 23:53:31 +0200 |
wenzelm |
more accurate Thm_Name.T for PThm / Thm.name_derivation / Thm.derivation_name;
|
file |
diff |
annotate
|
| Mon, 25 Sep 2023 20:56:44 +0200 |
wenzelm |
tuned: prefer antiquotation for try-catch;
|
file |
diff |
annotate
|
| Tue, 18 Apr 2023 11:58:12 +0200 |
wenzelm |
backout 61f652dd955a;
|
file |
diff |
annotate
|
| Tue, 11 Apr 2023 20:32:04 +0200 |
wenzelm |
performance tuning: replace Ord_List by Table();
|
file |
diff |
annotate
|
| Mon, 27 Mar 2023 21:48:47 +0200 |
wenzelm |
performance tuning: prefer functor Set() over Table();
|
file |
diff |
annotate
|
| Sat, 17 Sep 2022 16:50:39 +0200 |
wenzelm |
proper file headers;
|
file |
diff |
annotate
|
| Wed, 16 Feb 2022 14:24:05 +0100 |
desharna |
Mirabelle now considers goals preceding "unfolding" and "using" commands
|
file |
diff |
annotate
|
| Sat, 22 Jan 2022 11:46:25 +0100 |
desharna |
renamed run_action to run in Mirabelle.action record
|
file |
diff |
annotate
|
| Fri, 21 Jan 2022 12:09:55 +0100 |
desharna |
used elapsed time instead of cpu time in Mirabelle because the latter contain cpu time of all threads
|
file |
diff |
annotate
|
| Thu, 20 Jan 2022 13:55:29 +0100 |
desharna |
added Mirabelle option "-y" for dry run
|
file |
diff |
annotate
|
| Wed, 19 Jan 2022 10:11:24 +0100 |
desharna |
added cpu time (in ms) to Mirabelle run_action output
|
file |
diff |
annotate
|
| Tue, 18 Jan 2022 17:55:20 +0100 |
desharna |
added Mirabelle option -r to randomize the goals before selection
|
file |
diff |
annotate
|
| Fri, 17 Dec 2021 09:51:37 +0100 |
desharna |
added support for initialization messages to Mirabelle
|
file |
diff |
annotate
|
| Wed, 10 Nov 2021 12:34:19 +0100 |
wenzelm |
revert temporary workaround 6d111935299c;
|
file |
diff |
annotate
|
| Sun, 24 Oct 2021 16:43:54 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 21 Oct 2021 18:10:51 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Wed, 20 Oct 2021 16:36:49 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 18 Oct 2021 11:11:22 +0200 |
desharna |
added error message on invalid Mirabelle action
|
file |
diff |
annotate
|
| Mon, 20 Sep 2021 10:30:56 +0200 |
desharna |
produced Mirabelle output directly in ML until Scala output gets fixed
|
file |
diff |
annotate
|
| Thu, 05 Aug 2021 13:44:33 +0200 |
desharna |
added option labels to Mirabelle actions
|
file |
diff |
annotate
|
| Wed, 28 Jul 2021 19:17:31 +0200 |
desharna |
changed Mirabelle_Sledgehammer keep option from path to boolean
|
file |
diff |
annotate
|
| Wed, 28 Jul 2021 14:16:19 +0200 |
desharna |
added automatic uniform stride option to Mirabelle
|
file |
diff |
annotate
|
| Tue, 27 Jul 2021 13:39:18 +0200 |
desharna |
tuned Mirabelle's theory selection
|
file |
diff |
annotate
|
| Thu, 17 Jun 2021 10:30:07 +0200 |
desharna |
changed Mirabelle's filter to use short theory names
|
file |
diff |
annotate
|
| Sat, 12 Jun 2021 15:37:25 +0200 |
desharna |
added support for unbounded max calls to Mirabelle
|
file |
diff |
annotate
|
| Sat, 12 Jun 2021 12:39:33 +0200 |
desharna |
added warnings when defining unamed or redefining Mirabelle action
|
file |
diff |
annotate
|
| Sat, 12 Jun 2021 12:16:19 +0200 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Fri, 11 Jun 2021 09:33:43 +0200 |
desharna |
tuned Mirabelle
|
file |
diff |
annotate
|
| Thu, 10 Jun 2021 11:54:14 +0200 |
desharna |
merged
|
file |
diff |
annotate
|
| Thu, 10 Jun 2021 11:21:57 +0200 |
desharna |
refactored Mirabelle to produce output in real time
|
file |
diff |
annotate
|
| Mon, 07 Jun 2021 09:27:01 +0200 |
wenzelm |
more robust within session "HOL";
|
file |
diff |
annotate
|
| Sun, 06 Jun 2021 21:17:23 +0200 |
wenzelm |
suppress theories from other sessions, unless explicitly specified via mirabelle_theories;
|
file |
diff |
annotate
|
| Sun, 06 Jun 2021 20:29:52 +0200 |
wenzelm |
clarified hook for Mirabelle: provide all loaded theories at once (for each 'theories' section within the session ROOT);
|
file |
diff |
annotate
|
| Sun, 06 Jun 2021 16:34:57 +0200 |
wenzelm |
refer to theory "segments" only, according to global Build.build_theories and Thy_Info.use_theories;
|
file |
diff |
annotate
|
| Fri, 04 Jun 2021 23:55:35 +0200 |
wenzelm |
tuned --- reduced source complexity;
|
file |
diff |
annotate
|
| Fri, 04 Jun 2021 23:03:12 +0200 |
desharna |
moved stride option from sledgehammer action to main mirabelle
|
file |
diff |
annotate
|
| Sat, 15 May 2021 22:06:05 +0200 |
wenzelm |
reactive "sledgehammer";
|
file |
diff |
annotate
|
| Sat, 15 May 2021 13:25:52 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 14 May 2021 21:32:11 +0200 |
wenzelm |
reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
|
file |
diff |
annotate
| base
|