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

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

@@ -3629,84 +3629,6 @@ jobs:
       name: Building/fetching current CI target
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
         "rocq-master" --argstr job "mathcomp-algebra"
-  mathcomp-algebra-tactics:
-    needs:
-    - coq
-    - mathcomp-algebra
-    - coq-elpi
-    - mathcomp-zify
-    runs-on: ubuntu-latest
-    steps:
-    - name: Determine which commit to initially checkout
-      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"target_commit=${{
-        github.sha }}\" >> $GITHUB_ENV\nelse\n  echo \"target_commit=${{ github.event.pull_request.head.sha
-        }}\" >> $GITHUB_ENV\nfi\n"
-    - name: Git checkout
-      uses: actions/checkout@v6
-      with:
-        fetch-depth: 0
-        ref: ${{ env.target_commit }}
-    - name: Determine which commit to test
-      run: "if [ ${{ github.event_name }} = \"push\" ]; then\n  echo \"tested_commit=${{
-        github.sha }}\" >> $GITHUB_ENV\nelse\n  merge_commit=$(git ls-remote ${{ github.event.repository.html_url
-        }} refs/pull/${{ github.event.number }}/merge | cut -f1)\n  mergeable=$(git
-        merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
-        2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n  if [ -z \"$merge_commit\"\
-        \ -o \"x$mergeable\" != \"x0\" ]; then\n    echo \"tested_commit=${{ github.event.pull_request.head.sha
-        }}\" >> $GITHUB_ENV\n  else\n    echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
-        \  fi\nfi\n"
-    - name: Git checkout
-      uses: actions/checkout@v6
-      with:
-        fetch-depth: 0
-        ref: ${{ env.tested_commit }}
-    - name: Cachix install
-      uses: cachix/install-nix-action@v31
-      with:
-        nix_path: nixpkgs=channel:nixpkgs-unstable
-    - name: Cachix setup coq
-      uses: cachix/cachix-action@v16
-      with:
-        authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
-        extraPullNames: coq-community, math-comp
-        name: coq
-    - id: stepGetDerivation
-      name: Getting derivation for current job (mathcomp-algebra-tactics)
-      run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr bundle
-        \"rocq-master\" --argstr job \"mathcomp-algebra-tactics\" \\\n   --dry-run
-        2> err > out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo
-        \"Error: getting derivation failed\"; exit 1; fi\n"
-    - id: stepCheck
-      name: Checking presence of CI target for current job
-      run: "if $(cat out err | grep -q \"built:\") ; then\n  echo \"CI target needs
-        actual building\"\n  if $(cat out err | grep -q \"derivations will be built:\"\
-        ) ; then\n    echo \"waiting a bit for derivations that should be in cache\"\
-        \n    sleep 30\n  fi\nelse\n  echo \"CI target already built\"\n  echo \"\
-        status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
-    - if: steps.stepCheck.outputs.status != 'fetched'
-      name: 'Building/fetching previous CI target: coq'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
-        "rocq-master" --argstr job "coq"
-    - if: steps.stepCheck.outputs.status != 'fetched'
-      name: 'Building/fetching previous CI target: mathcomp-ssreflect'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
-        "rocq-master" --argstr job "mathcomp-ssreflect"
-    - if: steps.stepCheck.outputs.status != 'fetched'
-      name: 'Building/fetching previous CI target: mathcomp-algebra'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
-        "rocq-master" --argstr job "mathcomp-algebra"
-    - if: steps.stepCheck.outputs.status != 'fetched'
-      name: 'Building/fetching previous CI target: coq-elpi'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
-        "rocq-master" --argstr job "coq-elpi"
-    - if: steps.stepCheck.outputs.status != 'fetched'
-      name: 'Building/fetching previous CI target: mathcomp-zify'
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
-        "rocq-master" --argstr job "mathcomp-zify"
-    - if: steps.stepCheck.outputs.status != 'fetched'
-      name: Building/fetching current CI target
-      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
-        "rocq-master" --argstr job "mathcomp-algebra-tactics"
   mathcomp-analysis:
     needs:
     - coq
@@ -6618,6 +6540,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 
@@ -6677,6 +6603,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 
@@ -6741,6 +6671,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 
@@ -6805,6 +6739,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,14 +211,18 @@ 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-template-rocq"
       "metarocq-test"
+      "metarocq-translations"
+      "metarocq-utils"
       "rewriter"
       "riscvcoq"
       "rupicola"
@@ -282,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";
@@ -350,7 +370,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";
@@ -360,10 +380,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:
@@ -384,22 +407,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