Adapt to tify (https://github.com/rocq-community/micromega-plugin/pull/1)

.github/workflows/nix-action-rocq-master.yml

@@ -6456,6 +6456,10 @@ jobs:
       name: 'Building/fetching previous CI target: rocq-core'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
         "rocq-master" --argstr job "rocq-core"
+    - if: steps.stepCheck.outputs.status != 'fetched'
+      name: 'Building/fetching previous CI target: micromega-plugin'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
+        "rocq-master" --argstr job "micromega-plugin"
     - if: steps.stepCheck.outputs.status != 'fetched'
       name: Building/fetching current CI target
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
@@ -6515,6 +6519,10 @@ jobs:
       name: 'Building/fetching previous CI target: rocq-core'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
         "rocq-master" --argstr job "rocq-core"
+    - if: steps.stepCheck.outputs.status != 'fetched'
+      name: 'Building/fetching previous CI target: micromega-plugin'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
+        "rocq-master" --argstr job "micromega-plugin"
     - if: steps.stepCheck.outputs.status != 'fetched'
       name: Building/fetching current CI target
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
@@ -6579,6 +6587,10 @@ jobs:
       name: 'Building/fetching previous CI target: stdlib'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
         "rocq-master" --argstr job "stdlib"
+    - if: steps.stepCheck.outputs.status != 'fetched'
+      name: 'Building/fetching previous CI target: micromega-plugin'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
+        "rocq-master" --argstr job "micromega-plugin"
     - if: steps.stepCheck.outputs.status != 'fetched'
       name: Building/fetching current CI target
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
@@ -6643,6 +6655,10 @@ jobs:
       name: 'Building/fetching previous CI target: stdlib'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
         "rocq-master" --argstr job "stdlib"
+    - if: steps.stepCheck.outputs.status != 'fetched'
+      name: 'Building/fetching previous CI target: micromega-plugin'
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
+        "rocq-master" --argstr job "micromega-plugin"
     - if: steps.stepCheck.outputs.status != 'fetched'
       name: Building/fetching current CI target
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 

.gitignore

@@ -84,7 +84,6 @@ test-suite/coq-makefile/merlin1/.merlin
 test-suite/coqdoc/Coqdoc.*
 test-suite/coqdoc/index.html
 test-suite/coqdoc/coqdoc.css
-test-suite/output/MExtraction.out
 test-suite/output/*.out.real
 test-suite/oUnit-anon.cache
 test-suite/redirect_test.out

.nix/config.nix

@@ -143,7 +143,6 @@ with builtins; with (import <nixpkgs> {}).lib;
       "itree-io"
       "json"
       "kami"
-      "mathcomp-algebra-tactics"
       "mathcomp-analysis"
       "mathcomp-reals"
       "mathcomp-zify"
@@ -212,15 +211,17 @@ with builtins; with (import <nixpkgs> {}).lib;
       "metacoq-translations"
       "metacoq-utils"
       "metarocq"
+      "metarocq-common"
       "metarocq-erasure"
       "metarocq-erasure-plugin"
       "metarocq-pcuic"
       "metarocq-quotation"
       "metarocq-safechecker"
       "metarocq-safechecker-plugin"
       "metarocq-template-pcuic"
-      "metarocq-translations"
+      "metarocq-template-rocq"
       "metarocq-test"
+      "metarocq-utils"
       "rewriter"
       "riscvcoq"
       "rupicola"
@@ -284,20 +285,37 @@ with builtins; with (import <nixpkgs> {}).lib;
       #   for a complete list of Coq packages available in Nix
       # * <github_login>:<branch> is such that this will use the branch <branch>
       #   from https://github.com/<github_login>/<repository>
+      bedrock2.override.version = "proux01:stdlib251";
+      coq-elpi.override.version = "proux01:stdlib251";
+      coqutil.override.version = "proux01:stdlib251";
+      itauto.override.version = "proux01:stdlib251";
+      equations.override.version = "proux01:stdlib251";
+      equations-test.override.version = "proux01:stdlib251";
+      smtcoq.override.version = "proux01:stdlib251";
+      metarocq.override.version = "proux01:stdlib251";
+      metarocq-test.override.version = "proux01:stdlib251";
+      waterproof.override.version = "proux01:stdlib251";
       sf.job = false;  # temporarily disactivated in Rocq CI
       trakt.job = false;  # temporarily disactivated in Rocq CI
       smtcoq-trakt.job = false;  # temporarily disactivated in Rocq CI
     };
     common-bundles = listToAttrs (forEach rocq-master (p:
-      { name = p; value.override.version = "master"; }));
+      { name = p; value.override.version = "master"; }))
+    // {
+      micromega-plugin.override.version = "tify";
+      rocq-elpi.override.version = "proux01:stdlib251";
+      rocq-elpi-test.override.version = "proux01:stdlib251";
+    };
   in {
     "rocq-master" = { rocqPackages = common-bundles // {
       rocq-core.override.version = "master";
       stdlib-test.job = true;
       rocq-elpi.override.version = "master";
-      rocq-elpi-test.override.version = "master";
+      # rocq-elpi-test.override.version = "master";
+      rocq-elpi-test.override.version = "proux01:stdlib251";
       hierarchy-builder.override.version = "master";
-      micromega-plugin.override.version = "master";
+      # micromega-plugin.override.version = "master";
+      micromega-plugin.override.version = "tify";
       micromega-plugin.job = false;
       mathcomp.override.version = "master";
       mathcomp-bigenough.override.version = "master";
@@ -353,7 +371,7 @@ with builtins; with (import <nixpkgs> {}).lib;
       dpdgraph-test.override.version = "7a0fba21287dd8889c55e6611f8ba219d012b81b";
       coq-hammer.override.version = "1d581299c2a85af175b53bd35370ea074af922ec";
       coq-hammer-tactics.override.version = "1d581299c2a85af175b53bd35370ea074af922ec";
-      equations.override.version = "757662b9c875d7169a07b861d48e82157520ab1a";
+      equations.job = false;
       equations-test.job = false;
       fiat-parsers.job = false;  # broken
       metarocq.override.version = "e8f8078e756cc378b830eb5a8e4637df43d481af";
@@ -363,10 +381,13 @@ with builtins; with (import <nixpkgs> {}).lib;
       relation-algebra.override.version = "ba3db5783060d9e25d1db5e377fc9d71338a5160";
       rewriter.override.version = "dd37fb28ed7f01a3b7edc0675a86b95dd3eb1545";
       rocq-lean-import.override.version = "b8291b9dae4f5ed780112e95eea484e435199b46";
-      smtcoq.override.version = "cff0a8cdb7c73b6c59965a749a4304f3c4ac01bf";
+      # smtcoq.override.version = "cff0a8cdb7c73b6c59965a749a4304f3c4ac01bf";
+      smtcoq.job = false;
+      # smtcoq-trakt.override.version = "9392f7446a174b770110445c155a07b183cdca3d";
       stalmarck-tactic.override.version = "d32acd3c477c57b48dd92bdd96d53fb8fa628512";
       unicoq.override.version = "d52374ca86e3885197f114555e742420fa9bbe94";
-      waterproof.override.version = "99ad6ff78fa700c84ba0cb1d1bda27d8e0f11e1a";
+      # waterproof.override.version = "99ad6ff78fa700c84ba0cb1d1bda27d8e0f11e1a";
+      waterproof.job = false;
       compcert.job = false;  # broken
       VST.job = false;  # depends on compcert
     } // listToAttrs (forEach lighten-released (p:
@@ -387,22 +408,24 @@ with builtins; with (import <nixpkgs> {}).lib;
       dpdgraph-test.override.version = "7817def06d4e3abc2e54a2600cf6e29d63d58b8a";
       coq-hammer.override.version = "8649603dcbac5d92eaf1319a6b7cdfc65cdd804b";
       coq-hammer-tactics.override.version = "8649603dcbac5d92eaf1319a6b7cdfc65cdd804b";
-      equations.override.version = "2137c8e7081f2d47ab903de0cc09fd6a05bfab01";
+      equations.job = false;
       equations-test.job = false;
       fiat-parsers.job = false;  # broken
-      metarocq.override.version = "2995003b88f3812e5649cfdd0f9a4c44ceaf0700";
-      metarocq-test.override.version = "2995003b88f3812e5649cfdd0f9a4c44ceaf0700";
       mtac2.override.version = "bcbefa79406fc113f878eb5f89758de241d81433";
       paramcoq-test.override.version = "937537d416bc5f7b81937d4223d7783d0e687239";
       relation-algebra.override.version = "4db15229396abfd8913685be5ffda4f0fdb593d9";
       rewriter.override.version = "9496defb8b236f442d11372f6e0b5e48aa38acfc";
       rocq-lean-import.override.version = "c3546102f242aaa1e9af921c78bdb1132522e444";
-      smtcoq.override.version = "5c6033c906249fcf98a48b4112f6996053124514";
+      # smtcoq.override.version = "5c6033c906249fcf98a48b4112f6996053124514";
+      smtcoq.job = false;
+      # smtcoq-trakt.override.version = "9392f7446a174b770110445c155a07b183cdca3d";
       stalmarck-tactic.override.version = "d32acd3c477c57b48dd92bdd96d53fb8fa628512";
       unicoq.override.version = "28ec18aef35877829535316fc09825a25be8edf1";
-      waterproof.override.version = "dd712eb0b7f5c205870dbd156736a684d40eeb9a";
+      # waterproof.override.version = "dd712eb0b7f5c205870dbd156736a684d40eeb9a";
+      waterproof.job = false;
       compcert.job = false;  # broken
       VST.job = false;  # depends on compcert
+      mathcomp-algebra-tactics.job = false;
     } // listToAttrs (forEach lighten-released (p:
       { name = p; value.job = false; })); };
   };

.nix/coq-nix-toolbox.nix

@@ -1 +1 @@
-"175e68be5dcde92457dbb949ef905e771d765a68"
+"20731ec68fcf2772869a7d80da55b08723781827"

.nix/coq-overlays/itauto/default.nix

@@ -0,0 +1,67 @@
+{
+  lib,
+  callPackage,
+  mkCoqDerivation,
+  coq,
+  stdlib,
+  dune,
+  version ? null,
+}:
+
+(mkCoqDerivation {
+  pname = "itauto";
+  owner = "fbesson";
+  # domain = "gitlab.inria.fr";
+
+  release."8.20.0".sha256 = "sha256-LYKGbI3O6yw6CiTJNUGL11PT4q4o+gJK1kQgKQL0/Hk=";
+  release."8.19.0".sha256 = "sha256-xKWCF4dYvvlJUVGCZcR2RLCG55vlGzu2GN30MeRvVD4=";
+  release."8.18.0".sha256 = "sha256-4mDDnKTeYrf27uRMkydQxO7j2tfgTFXOREW474d40eo=";
+  release."8.17.0".sha256 = "sha256-fgdnKchNT1Hyrq14gU8KWYnlSfg3qlsSw5A4+RoA26w=";
+  release."8.16.0".sha256 = "sha256-4zAUYGlw/pBcLPv2GroIduIlvbfi1+Vy+TdY8KLCqO4=";
+  release."8.15.0".sha256 = "sha256:10qpv4nx1p0wm9sas47yzsg9z22dhvizszfa21yff08a8fr0igya";
+  release."8.14.0".sha256 = "sha256:1k6pqhv4dwpkwg81f2rlfg40wh070ks1gy9r0ravm2zhsbxqcfc9";
+  release."8.13+no".sha256 = "sha256-gXoxtLcHPoyjJkt7WqvzfCMCQlh6kL2KtCGe3N6RC/A=";
+  inherit version;
+  defaultVersion =
+    let
+      case = case: out: { inherit case out; };
+    in
+    with lib.versions;
+    lib.switch coq.coq-version [
+      (case (isEq "8.20") "8.20.0")
+      (case (isEq "8.19") "8.19.0")
+      (case (isEq "8.18") "8.18.0")
+      (case (isEq "8.17") "8.17.0")
+      (case (isEq "8.16") "8.16.0")
+      (case (isEq "8.15") "8.15.0")
+      (case (isEq "8.14") "8.14.0")
+      (case (isEq "8.13") "8.13+no")
+    ] null;
+
+  mlPlugin = true;
+  nativeBuildInputs = (with coq.ocamlPackages; [ ocamlbuild ]);
+  enableParallelBuilding = false;
+
+  passthru.tests.suite = callPackage ./test.nix { };
+
+  propagatedBuildInputs = [ stdlib ];
+
+  meta = {
+    description = "Reflexive SAT solver parameterised by a leaf tactic and Nelson-Oppen support";
+    maintainers = with lib.maintainers; [ siraben ];
+    license = lib.licenses.gpl3Plus;
+  };
+}).overrideAttrs
+  (
+    o:
+    lib.optionalAttrs (o.version == "dev" || lib.versionAtLeast o.version "8.16") {
+      propagatedBuildInputs = o.propagatedBuildInputs ++ [ coq.ocamlPackages.findlib ];
+    }
+    // lib.optionalAttrs (o.version == "dev" || lib.versionAtLeast o.version "8.18") {
+      nativeBuildInputs = with coq.ocamlPackages; [
+        ocaml
+        findlib
+        dune
+      ];
+    }
+  )

.nix/coq-overlays/itauto/test.nix

@@ -0,0 +1,38 @@
+{
+  stdenv,
+  lib,
+  coq,
+  itauto,
+}:
+
+let
+  excluded = lib.optionals (lib.versions.isEq "8.16" itauto.version) [
+    "arith.v"
+    "refl_bool.v"
+  ];
+in
+
+stdenv.mkDerivation {
+  pname = "coq${coq.coq-version}-itauto-test";
+  inherit (itauto) src version;
+
+  nativeCheckInputs = [
+    coq
+    itauto
+  ];
+
+  dontConfigure = true;
+  dontBuild = true;
+  doCheck = true;
+
+  checkPhase = ''
+    cd test-suite
+    for m in *.v
+    do
+      echo -n ${lib.concatStringsSep " " excluded} | grep --silent $m && continue
+      echo $m && coqc $m
+    done
+  '';
+
+  installPhase = "touch $out";
+}

.nix/rocq-overlays/stdlib-refman-html/default.nix

@@ -15,8 +15,12 @@ rocqPackages.lib.overrideRocqDerivation {
 
   useDune = true;
 
-  buildPhase = ''
+  configurePhase = ''
+    export COQPATH=''${ROCQPATH}
     patchShebangs dev/with-rocq-wrap.sh
+  '';
+
+  buildPhase = ''
     dev/with-rocq-wrap.sh dune build --root . --no-buffer @refman-html ''${enableParallelBuilding:+-j $NIX_BUILD_CORES}
   '';
 

default.nix

@@ -4,8 +4,8 @@
   bundle ? null, job ? null, inNixShell ? null, src ? ./.,
 }@args:
 let auto = fetchGit {
-  url = "https://github.com/rocq-community/coq-nix-toolbox.git";
-  ref = "master";
+  url = "https://github.com/proux01/coq-nix-toolbox.git";
+  ref = "micromega";
   rev = import .nix/coq-nix-toolbox.nix;
 };
 in

rocq-stdlib.opam

@@ -26,6 +26,7 @@ dev-repo: "git+https://github.com/coq/stdlib.git"
 depends: [
   "rocq-runtime"
   "rocq-core" {>= "9.1"}
+  "micromega-plugin" {= "dev"}
 ]
 build: [
   [make "-j" jobs]

subcomponents/corelib_wrapper.v

@@ -3,6 +3,7 @@ From Stdlib Require Array.PrimArray.
 From Stdlib Require BinNums.IntDef.
 From Stdlib Require BinNums.NatDef.
 From Stdlib Require BinNums.PosDef.
+From Stdlib Require BinNums.RatDef.
 From Stdlib Require Classes.CMorphisms.
 From Stdlib Require Classes.CRelationClasses.
 From Stdlib Require Classes.Equivalence.

subcomponents/field.v

@@ -1,2 +1,3 @@
 From subcomponents Require ring.
 From Stdlib Require setoid_ring.Field.
+From Stdlib Require setoid_ring.field_eval.

subcomponents/lia.v

@@ -1,11 +1,3 @@
 From subcomponents Require ring.
+From subcomponents Require tify.
 From Stdlib Require micromega.Lia.
-From Stdlib Require micromega.SatDivMod.
-From Stdlib Require micromega.Zify.
-From Stdlib Require micromega.ZifyBool.
-From Stdlib Require micromega.ZifyClasses.
-From Stdlib Require micromega.ZifyComparison.
-From Stdlib Require micromega.ZifyInst.
-From Stdlib Require micromega.ZifyN.
-From Stdlib Require micromega.ZifyNat.
-From Stdlib Require micromega.ZifyPow.

subcomponents/ring.v

@@ -18,6 +18,7 @@ From Stdlib Require setoid_ring.Ring_tac.
 From Stdlib Require setoid_ring.ArithRing.
 From Stdlib Require setoid_ring.NArithRing.
 From Stdlib Require setoid_ring.Ring_theory.
+From Stdlib Require setoid_ring.ring_eval.
 From Stdlib Require nsatz.NsatzTactic.
 From Stdlib Require nsatz.ENsatzTactic.
 From Stdlib Require micromega.VarMap.

subcomponents/tify.v

@@ -0,0 +1,12 @@
+From subcomponents Require integers.
+From subcomponents Require ring.
+From Stdlib Require micromega.Tify.
+From Stdlib Require micromega.Zify.
+From Stdlib Require micromega.SatDivMod.
+From Stdlib Require micromega.ZifyBool.
+From Stdlib Require micromega.ZifyClasses.
+From Stdlib Require micromega.ZifyComparison.
+From Stdlib Require micromega.ZifyInst.
+From Stdlib Require micromega.ZifyN.
+From Stdlib Require micromega.ZifyNat.
+From Stdlib Require micromega.ZifyPow.

test-suite/Makefile

@@ -136,7 +136,8 @@ PREREQUISITELOG = $(addsuffix .log,$(wildcard prerequisite/*.v)) .csdp.cache
 ifeq ($(COQLIB_NOT_FOUND),true)
 all:
 	@echo ""
-	@echo "Coq's standard library has not been installed; please run: "
+	@echo "The Stdlib library has not been installed; please run:"
+	@echo "  - cd .."
 	@echo "  - make"
 	@echo "  - make install"
 	@echo ""