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

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

@@ -3568,6 +3568,7 @@ jobs:
     - mathcomp-order
     - mathcomp-fingroup
     - hierarchy-builder
+    - micromega-plugin
     runs-on: ubuntu-latest
     steps:
     - name: Determine which commit to initially checkout
@@ -3633,87 +3634,13 @@ jobs:
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
         "rocq-master" --argstr job "hierarchy-builder"
     - if: steps.stepCheck.outputs.status != 'fetched'
-      name: Building/fetching current CI target
+      name: 'Building/fetching previous CI target: micromega-plugin'
       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"
+        "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 
-        "rocq-master" --argstr job "mathcomp-algebra-tactics"
+        "rocq-master" --argstr job "mathcomp-algebra"
   mathcomp-analysis:
     needs:
     - coq
@@ -5839,6 +5766,65 @@ jobs:
       name: Building/fetching current CI target
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
         "rocq-master" --argstr job "metarocq-utils"
+  micromega-plugin:
+    needs:
+    - rocq-core
+    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 (micromega-plugin)
+      run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr bundle
+        \"rocq-master\" --argstr job \"micromega-plugin\" \\\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: 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 current CI target
+      run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle 
+        "rocq-master" --argstr job "micromega-plugin"
   mtac2:
     needs:
     - coq
@@ -7004,6 +6990,7 @@ jobs:
   stdlib:
     needs:
     - rocq-core
+    - micromega-plugin
     runs-on: ubuntu-latest
     steps:
     - name: Determine which commit to initially checkout
@@ -7056,6 +7043,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 
@@ -7064,6 +7055,7 @@ jobs:
     needs:
     - rocq-core
     - stdlib
+    - micromega-plugin
     runs-on: ubuntu-latest
     steps:
     - name: Determine which commit to initially checkout
@@ -7120,6 +7112,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 
@@ -7128,6 +7124,7 @@ jobs:
     needs:
     - rocq-core
     - stdlib
+    - micromega-plugin
     runs-on: ubuntu-latest
     steps:
     - name: Determine which commit to initially checkout
@@ -7184,6 +7181,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

@@ -156,7 +156,6 @@ with builtins; with (import <nixpkgs> {}).lib;
       "itree-io"
       "json"
       "kami"
-      "mathcomp-algebra-tactics"
       "mathcomp-analysis"
       "mathcomp-classical"
       "mathcomp-reals"
@@ -227,14 +226,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"
@@ -249,7 +252,7 @@ with builtins; with (import <nixpkgs> {}).lib;
     // listToAttrs (forEach main (p:
       { name = p; value.override.version = "main"; }))
     // {
-      coq-elpi.override.version = "master";
+      # coq-elpi.override.version = "master";
       coq-elpi.override.elpi-version = "3.6.2";
       tlc.override.version = "master-for-coq-ci";
       smtcoq-trakt.override.version = "with-trakt-coq-master";
@@ -258,6 +261,7 @@ with builtins; with (import <nixpkgs> {}).lib;
       iris-examples.job = false;  # Currently broken
       jasmin.job = false;  # Currently broken, c.f., https://github.com/rocq-prover/rocq/pull/20589
       CakeMLExtraction.job = false;  # not in Rocq CI
+      verified-extraction.job = false;  # not in Rocq CI
       ceres-bs.job = false;  # not in Rocq CI
       CertiRocq.job = false;  # not in Rocq CI
       ConCert.job = false;  # not in Rocq CI
@@ -280,12 +284,28 @@ 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>
+      micromega-plugin.override.version = "tify";
+      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";
@@ -311,7 +331,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";
@@ -321,11 +341,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:
@@ -346,21 +368,21 @@ 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
     } // listToAttrs (forEach lighten-released (p:

.nix/coq-nix-toolbox.nix

@@ -1 +1 @@
-"3b7baf61aa95441d62332d7fdad562a61a125f80"
+"e0b17bf483bcde5079722f9bc494063373ee098e"