Merge PR coq#18336: Split the Micromega library in two components.

Reviewed-by: ejgallego Ack-by: SkySkimmer Co-authored-by: ejgallego <[email protected]>
Villetaneuse · Jan 3, 2024 · 0e4d060 · 0e4d060
2 parents 0aab3e0 + 8986248
commit 0e4d060
Show file tree

Hide file tree

Showing 10 changed files with 20 additions and 5 deletions.
diff --git a/dev/ci/user-overlays/18336-SkySkimmer-micromega-split-library.sh 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
@@ -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
@@ -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
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		overlay smtcoq https://github.com/SkySkimmer/smtcoq micromega-split-library 18336