From 89862486387a2a09028d389953757e087897696c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Sun, 19 Nov 2023 14:44:20 +0100 Subject: [PATCH] Split the Micromega library in two components. The first component is the part of the library used by csdpcert, which only relies on basic APIs from clib. The second one embarks all the Ltac-related code and corresponds to the previous micromega plugin. Since csdpcert only links the first one, its executable doesn't link findlib anymore, which prevents implicitly setting the -linkall flag. This was useless for csdpcert since this executable never performs any plugin dynlink. This reduces the size of the csdpcert binary from 32Mo to 6.5Mo on my machine. Maybe the barebone library should live in its own subdirectory but it was very annoying w.r.t. the other parts of Coq's build system so I left it there. --- .../18336-SkySkimmer-micromega-split-library.sh | 1 + lib/core_plugins_findlib_compat.ml | 1 + plugins/micromega/dune | 16 ++++++++++++---- plugins/micromega/micromega_core_plugin.mllib | 0 test-suite/micromega/witness_tactics.v | 1 + theories/micromega/Lia.v | 1 + theories/micromega/Lqa.v | 1 + theories/micromega/Lra.v | 1 + theories/micromega/Psatz.v | 1 + tools/dune_rule_gen/coq_rules.ml | 2 +- 10 files changed, 20 insertions(+), 5 deletions(-) create mode 100644 dev/ci/user-overlays/18336-SkySkimmer-micromega-split-library.sh create mode 100644 plugins/micromega/micromega_core_plugin.mllib diff --git a/dev/ci/user-overlays/18336-SkySkimmer-micromega-split-library.sh b/dev/ci/user-overlays/18336-SkySkimmer-micromega-split-library.sh new file mode 100644 index 000000000000..f0ddb5b0055c --- /dev/null +++ b/dev/ci/user-overlays/18336-SkySkimmer-micromega-split-library.sh @@ -0,0 +1 @@ +overlay smtcoq https://github.com/SkySkimmer/smtcoq micromega-split-library 18336 diff --git a/lib/core_plugins_findlib_compat.ml b/lib/core_plugins_findlib_compat.ml index 9201fc1ed7e7..f2637f16c7e2 100644 --- a/lib/core_plugins_findlib_compat.ml +++ b/lib/core_plugins_findlib_compat.ml @@ -13,6 +13,7 @@ let legacy_to_findlib = [ ("derive_plugin", ["plugins";"derive"]) ; ("firstorder_plugin", ["plugins";"firstorder"]) ; ("ltac_plugin", ["plugins";"ltac"]) ; + ("micromega_core_plugin", ["plugins";"micromega_core";]) ; ("micromega_plugin", ["plugins";"micromega"]) ; ("ring_plugin", ["plugins";"ring"]) ; ("ssr_plugin", ["plugins";"ssr"]) ; diff --git a/plugins/micromega/dune b/plugins/micromega/dune index 41f894bce341..f603d988bc93 100644 --- a/plugins/micromega/dune +++ b/plugins/micromega/dune @@ -1,18 +1,26 @@ +(library + (name micromega_core_plugin) + (public_name coq-core.plugins.micromega_core) + (modules micromega numCompat mutils sos_types sos_lib sos) + (synopsis "Coq's micromega core plugin") + (libraries zarith coq-core.clib)) + (library (name micromega_plugin) (public_name coq-core.plugins.micromega) ; be careful not to link the executable to the plugin! - (modules (:standard \ csdpcert g_zify zify)) + (modules (:standard \ micromega numCompat mutils sos_types sos_lib sos csdpcert g_zify zify)) + (flags :standard -open Micromega_core_plugin) (synopsis "Coq's micromega plugin") - (libraries coq-core.plugins.ltac)) + (libraries coq-core.plugins.ltac coq-core.plugins.micromega_core)) (executable (name csdpcert) (public_name csdpcert) (package coq-core) (modules csdpcert) - (flags :standard -open Micromega_plugin) - (libraries coq-core.plugins.micromega)) + (flags :standard -open Micromega_core_plugin) + (libraries coq-core.plugins.micromega_core)) (library (name zify_plugin) diff --git a/plugins/micromega/micromega_core_plugin.mllib b/plugins/micromega/micromega_core_plugin.mllib new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/test-suite/micromega/witness_tactics.v b/test-suite/micromega/witness_tactics.v index 364acafcc1fe..4051c4fdf12c 100644 --- a/test-suite/micromega/witness_tactics.v +++ b/test-suite/micromega/witness_tactics.v @@ -2,6 +2,7 @@ Require Import ZArith QArith. From Coq.micromega Require Import RingMicromega EnvRing Tauto. From Coq.micromega Require Import ZMicromega QMicromega. +Declare ML Module "micromega_core_plugin:coq-core.plugins.micromega_core". Declare ML Module "micromega_plugin:coq-core.plugins.micromega". Goal True. diff --git a/theories/micromega/Lia.v b/theories/micromega/Lia.v index 0f1c607b9519..543c73b7fdb9 100644 --- a/theories/micromega/Lia.v +++ b/theories/micromega/Lia.v @@ -17,6 +17,7 @@ Require Import ZMicromega RingMicromega VarMap DeclConstant. Require Import BinNums. Require Coq.micromega.Tauto. +Declare ML Module "micromega_core_plugin:coq-core.plugins.micromega_core". Declare ML Module "micromega_plugin:coq-core.plugins.micromega". Ltac zchecker := diff --git a/theories/micromega/Lqa.v b/theories/micromega/Lqa.v index 694041b36628..0252b66fd9b0 100644 --- a/theories/micromega/Lqa.v +++ b/theories/micromega/Lqa.v @@ -20,6 +20,7 @@ Require Import RingMicromega. Require Import VarMap. Require Import DeclConstant. Require Coq.micromega.Tauto. +Declare ML Module "micromega_core_plugin:coq-core.plugins.micromega_core". Declare ML Module "micromega_plugin:coq-core.plugins.micromega". Ltac rchange := diff --git a/theories/micromega/Lra.v b/theories/micromega/Lra.v index cd596043b153..ed4a13b0cee6 100644 --- a/theories/micromega/Lra.v +++ b/theories/micromega/Lra.v @@ -21,6 +21,7 @@ Require Import RingMicromega. Require Import VarMap. Require Coq.micromega.Tauto. Require Import Rregisternames. +Declare ML Module "micromega_core_plugin:coq-core.plugins.micromega_core". Declare ML Module "micromega_plugin:coq-core.plugins.micromega". Ltac rchange := diff --git a/theories/micromega/Psatz.v b/theories/micromega/Psatz.v index 67b7860c2f16..f49b6d791cb4 100644 --- a/theories/micromega/Psatz.v +++ b/theories/micromega/Psatz.v @@ -27,6 +27,7 @@ Require Lia. Require Lra. Require Lqa. +Declare ML Module "micromega_core_plugin:coq-core.plugins.micromega_core". Declare ML Module "micromega_plugin:coq-core.plugins.micromega". Ltac lia := Lia.lia. diff --git a/tools/dune_rule_gen/coq_rules.ml b/tools/dune_rule_gen/coq_rules.ml index 7fa81d44201a..e2cd32302cb9 100644 --- a/tools/dune_rule_gen/coq_rules.ml +++ b/tools/dune_rule_gen/coq_rules.ml @@ -36,7 +36,7 @@ module FlagUtil = struct |> Util.list_concat_map (fun p -> [Arg.A "-I"; Arg.Path p]) let findlib_plugin_fixup p = - ["number_string_notation"; "zify"; "tauto"; "ssreflect"] + ["number_string_notation"; "zify"; "tauto"; "ssreflect"; "micromega_core"] @ (List.filter (fun s -> not (String.equal s "syntax" || String.equal s "ssr")) p) (* This can also go when the -I flags are gone, by passing the meta