From e3fe550abb2b330e4e7e0d4e59ca69c7742ad066 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 20 Feb 2026 16:17:40 +0100 Subject: [PATCH] Drop support for Coq 8.20 --- ....20-2.4.0.yml => nix-action-9.0-2.4.0.yml} | 311 ++++++++++++++---- .nix/config.nix | 12 +- INSTALL.md | 22 +- Makefile.common | 2 +- Makefile.coq.local | 8 - README.md | 2 +- coq-mathcomp-classical.opam | 3 +- 7 files changed, 265 insertions(+), 95 deletions(-) rename .github/workflows/{nix-action-8.20-2.4.0.yml => nix-action-9.0-2.4.0.yml} (74%) delete mode 100644 Makefile.coq.local diff --git a/.github/workflows/nix-action-8.20-2.4.0.yml b/.github/workflows/nix-action-9.0-2.4.0.yml similarity index 74% rename from .github/workflows/nix-action-8.20-2.4.0.yml rename to .github/workflows/nix-action-9.0-2.4.0.yml index 80cd4e4333..9a055ed3a0 100644 --- a/.github/workflows/nix-action-8.20-2.4.0.yml +++ b/.github/workflows/nix-action-9.0-2.4.0.yml @@ -1,6 +1,7 @@ jobs: coq: - needs: [] + needs: + - rocq-core runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -39,7 +40,7 @@ jobs: - id: stepGetDerivation name: Getting derivation for current job (coq) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.20-2.4.0\" --argstr job \"coq\" \\\n --dry-run 2> err > out || (touch + \"9.0-2.4.0\" --argstr job \"coq\" \\\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 @@ -49,9 +50,13 @@ jobs: ) ; 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 "9.0-2.4.0" + --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 "8.20-2.4.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" --argstr job "coq" mathcomp: needs: @@ -94,9 +99,9 @@ jobs: - id: stepGetDerivation name: Getting derivation for current job (mathcomp) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.20-2.4.0\" --argstr job \"mathcomp\" \\\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" + \"9.0-2.4.0\" --argstr job \"mathcomp\" \\\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 @@ -106,15 +111,19 @@ jobs: 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 "8.20-2.4.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" --argstr job "coq" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-character' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.4.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" --argstr job "mathcomp-character" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: hierarchy-builder' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" + --argstr job "hierarchy-builder" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.4.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" --argstr job "mathcomp" mathcomp-analysis: needs: @@ -158,8 +167,8 @@ jobs: - id: stepGetDerivation name: Getting derivation for current job (mathcomp-analysis) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.20-2.4.0\" --argstr job \"mathcomp-analysis\" \\\n --dry-run 2> err - > out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: + \"9.0-2.4.0\" --argstr job \"mathcomp-analysis\" \\\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 @@ -170,23 +179,27 @@ jobs: 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 "8.20-2.4.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" --argstr job "coq" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-reals' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.4.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" --argstr job "mathcomp-reals" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.4.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" --argstr job "mathcomp-field" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-bigenough' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.4.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" --argstr job "mathcomp-bigenough" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: hierarchy-builder' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" + --argstr job "hierarchy-builder" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.4.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" --argstr job "mathcomp-analysis" mathcomp-analysis-single: needs: @@ -229,9 +242,9 @@ jobs: - id: stepGetDerivation name: Getting derivation for current job (mathcomp-analysis-single) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.20-2.4.0\" --argstr job \"mathcomp-analysis-single\" \\\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" + \"9.0-2.4.0\" --argstr job \"mathcomp-analysis-single\" \\\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 @@ -241,35 +254,43 @@ jobs: 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 "8.20-2.4.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" --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 "8.20-2.4.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" --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 "8.20-2.4.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" --argstr job "mathcomp-algebra" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-finmap' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.4.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" --argstr job "mathcomp-finmap" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-bigenough' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.4.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" --argstr job "mathcomp-bigenough" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.4.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" --argstr job "mathcomp-field" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-bigenough' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.4.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" --argstr job "mathcomp-bigenough" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: stdlib' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" + --argstr job "stdlib" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: hierarchy-builder' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" + --argstr job "hierarchy-builder" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.4.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" --argstr job "mathcomp-analysis-single" mathcomp-analysis-stdlib: needs: @@ -314,9 +335,9 @@ jobs: - id: stepGetDerivation name: Getting derivation for current job (mathcomp-analysis-stdlib) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.20-2.4.0\" --argstr job \"mathcomp-analysis-stdlib\" \\\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" + \"9.0-2.4.0\" --argstr job \"mathcomp-analysis-stdlib\" \\\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 @@ -326,19 +347,27 @@ jobs: 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 "8.20-2.4.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" --argstr job "coq" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-analysis' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.4.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" --argstr job "mathcomp-analysis" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-reals-stdlib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.4.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" --argstr job "mathcomp-reals-stdlib" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: stdlib' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" + --argstr job "stdlib" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: hierarchy-builder' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" + --argstr job "hierarchy-builder" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.4.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" --argstr job "mathcomp-analysis-stdlib" mathcomp-classical: needs: @@ -381,7 +410,7 @@ jobs: - id: stepGetDerivation name: Getting derivation for current job (mathcomp-classical) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.20-2.4.0\" --argstr job \"mathcomp-classical\" \\\n --dry-run 2> err + \"9.0-2.4.0\" --argstr job \"mathcomp-classical\" \\\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 @@ -393,23 +422,27 @@ jobs: 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 "8.20-2.4.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" --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 "8.20-2.4.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" --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 "8.20-2.4.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" --argstr job "mathcomp-algebra" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-finmap' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.4.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" --argstr job "mathcomp-finmap" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: hierarchy-builder' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" + --argstr job "hierarchy-builder" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.4.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" --argstr job "mathcomp-classical" mathcomp-experimental-reals: needs: @@ -453,7 +486,7 @@ jobs: - id: stepGetDerivation name: Getting derivation for current job (mathcomp-experimental-reals) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.20-2.4.0\" --argstr job \"mathcomp-experimental-reals\" \\\n --dry-run + \"9.0-2.4.0\" --argstr job \"mathcomp-experimental-reals\" \\\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 @@ -465,20 +498,96 @@ jobs: 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 "8.20-2.4.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" --argstr job "coq" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-reals' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.4.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" --argstr job "mathcomp-reals" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-bigenough' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.4.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" --argstr job "mathcomp-bigenough" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: hierarchy-builder' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" + --argstr job "hierarchy-builder" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.4.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" --argstr job "mathcomp-experimental-reals" + mathcomp-infotheo: + needs: + - coq + - mathcomp-analysis-stdlib + 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@v4 + 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@v4 + 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 math-comp + uses: cachix/cachix-action@v16 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepGetDerivation + name: Getting derivation for current job (mathcomp-infotheo) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"9.0-2.4.0\" --argstr job \"mathcomp-infotheo\" \\\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 "9.0-2.4.0" + --argstr job "coq" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-analysis-stdlib' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" + --argstr job "mathcomp-analysis-stdlib" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-algebra-tactics' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" + --argstr job "mathcomp-algebra-tactics" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: interval' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" + --argstr job "interval" + - if: steps.stepCheck.outputs.status != 'fetched' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" + --argstr job "mathcomp-infotheo" mathcomp-reals: needs: - coq @@ -521,7 +630,7 @@ jobs: - id: stepGetDerivation name: Getting derivation for current job (mathcomp-reals) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.20-2.4.0\" --argstr job \"mathcomp-reals\" \\\n --dry-run 2> err > out + \"9.0-2.4.0\" --argstr job \"mathcomp-reals\" \\\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 @@ -533,15 +642,19 @@ jobs: 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 "8.20-2.4.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" --argstr job "coq" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-classical' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.4.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" --argstr job "mathcomp-classical" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: hierarchy-builder' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" + --argstr job "hierarchy-builder" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.4.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" --argstr job "mathcomp-reals" mathcomp-reals-stdlib: needs: @@ -585,9 +698,9 @@ jobs: - id: stepGetDerivation name: Getting derivation for current job (mathcomp-reals-stdlib) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.20-2.4.0\" --argstr job \"mathcomp-reals-stdlib\" \\\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" + \"9.0-2.4.0\" --argstr job \"mathcomp-reals-stdlib\" \\\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 @@ -597,16 +710,78 @@ jobs: 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 "8.20-2.4.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" --argstr job "coq" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-reals' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.4.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" --argstr job "mathcomp-reals" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: stdlib' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" + --argstr job "stdlib" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: hierarchy-builder' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" + --argstr job "hierarchy-builder" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.4.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" --argstr job "mathcomp-reals-stdlib" + rocq-core: + needs: [] + 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@v4 + 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@v4 + 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 math-comp + uses: cachix/cachix-action@v16 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepGetDerivation + name: Getting derivation for current job (rocq-core) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"9.0-2.4.0\" --argstr job \"rocq-core\" \\\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 current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" + --argstr job "rocq-core" ssprove: needs: - coq @@ -650,7 +825,7 @@ jobs: - id: stepGetDerivation name: Getting derivation for current job (ssprove) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.20-2.4.0\" --argstr job \"ssprove\" \\\n --dry-run 2> err > out || (touch + \"9.0-2.4.0\" --argstr job \"ssprove\" \\\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 @@ -662,48 +837,48 @@ jobs: 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 "8.20-2.4.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" --argstr job "coq" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: equations' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.4.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" --argstr job "equations" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-boot' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.4.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" --argstr job "mathcomp-boot" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-analysis' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.4.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" --argstr job "mathcomp-analysis" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-experimental-reals' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.4.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" --argstr job "mathcomp-experimental-reals" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: extructures' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.4.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" --argstr job "extructures" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: deriving' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.4.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" --argstr job "deriving" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-word' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.4.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" --argstr job "mathcomp-word" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20-2.4.0" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-2.4.0" --argstr job "ssprove" -name: Nix CI for bundle 8.20-2.4.0 +name: Nix CI for bundle 9.0-2.4.0 on: pull_request: paths: - - .github/workflows/nix-action-8.20-2.4.0.yml + - .github/workflows/nix-action-9.0-2.4.0.yml pull_request_target: paths-ignore: - - .github/workflows/nix-action-8.20-2.4.0.yml + - .github/workflows/nix-action-9.0-2.4.0.yml types: - opened - synchronize diff --git a/.nix/config.nix b/.nix/config.nix index 954ad8a4ab..9d0d25acf9 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -53,10 +53,14 @@ in { ## When generating GitHub Action CI, one workflow file ## will be created per bundle - bundles."8.20-2.4.0".coqPackages = common-bundle // { - coq.override.version = "8.20"; - mathcomp.override.version = "2.4.0"; - mathcomp-infotheo.job = false; + bundles."9.0-2.4.0" = { + rocqPackages = { + rocq-core.override.version = "9.0"; + }; + coqPackages = common-bundle // { + coq.override.version = "9.0"; + mathcomp.override.version = "2.4.0"; + }; }; bundles."9.0" = { diff --git a/INSTALL.md b/INSTALL.md index 4c69982950..8a1fef4c56 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -2,7 +2,7 @@ ## Requirements -- [The Coq Proof Assistant version ≥ 8.20 / Rocq Prover version ≥ 9.0](https://rocq-prover.org) +- [The Rocq Prover version ≥ 9.0](https://rocq-prover.org) - [Mathematical Components version ≥ 2.4.0](https://github.com/math-comp/math-comp) - [Finmap library version ≥ 2.1.0](https://github.com/math-comp/finmap) - [Hierarchy builder version ≥ 1.8.0](https://github.com/math-comp/hierarchy-builder) @@ -73,28 +73,28 @@ using [proof general for emacs](https://github.com/ProofGeneral/PG) ## Break-down of phase 3 of the installation procedure step by step -With the example of Coq 8.20.1 and MathComp 2.4.0. For other versions, update the +With the example of Coq 9.1.1 and MathComp 2.5.0. For other versions, update the version numbers accordingly. -1. Install Coq 8.20.1 +1. Install Rocq 9.1.1 ``` -$ opam install coq.8.20.1 +$ opam install rocq-core.9.1.1 ``` 2. Install the Mathematical Components ``` -$ opam install coq-mathcomp-ssreflect.2.4.0 -$ opam install coq-mathcomp-fingroup.2.4.0 -$ opam install coq-mathcomp-algebra.2.4.0 -$ opam install coq-mathcomp-solvable.2.4.0 -$ opam install coq-mathcomp-field.2.4.0 +$ opam install rocq-mathcomp-ssreflect.2.5.0 +$ opam install rocq-mathcomp-fingroup.2.5.0 +$ opam install rocq-mathcomp-algebra.2.5.0 +$ opam install rocq-mathcomp-solvable.2.5.0 +$ opam install rocq-mathcomp-field.2.5.0 ``` 3. Install the Finite maps library ``` -$ opam install coq-mathcomp-finmap.2.2.0 +$ opam install rocq-mathcomp-finmap.2.2.0 ``` 4. Install the Hierarchy Builder ``` -$ opam install coq-hierarchy-builder.1.8.0 +$ opam install rocq-hierarchy-builder.1.10.2 ``` 5. Download and compile `coq-mathcomp-analysis` without installing ``` diff --git a/Makefile.common b/Makefile.common index 4f0bdbd824..2de024d68a 100644 --- a/Makefile.common +++ b/Makefile.common @@ -123,7 +123,7 @@ html: build $(DOCDIR)/dependency_graph.dot -Q reals_stdlib mathcomp.reals_stdlib \ -Q experimental_reals mathcomp.experimental_reals \ -Q analysis_stdlib mathcomp.analysis_stdlib \ - -coqlib https://rocq-prover.org/doc/V8.20.1/stdlib/ \ + -coqlib https://rocq-prover.org/doc/V9.0.0/stdlib/ \ -dependency-graph $(DOCDIR)/dependency_graph.dot \ -hierarchy-graph $(DOCDIR)/hierarchy_graph.dot \ -index-blacklist etc/rocqnavi_index-blacklist \ diff --git a/Makefile.coq.local b/Makefile.coq.local deleted file mode 100644 index b757c395c1..0000000000 --- a/Makefile.coq.local +++ /dev/null @@ -1,8 +0,0 @@ -pre-all:: - if command -v coqc > /dev/null && (coqc --version | grep -q '8.20') ; then \ - for f in $(shell grep "From Corelib" $$(find . -name "*.v") | cut -d: -f1) ; do \ - sed -i.bak 's/From Corelib/From Coq/' $${f} ; \ - sed -i.bak 's/PosDef/PArith/' $${f} ; \ - $(RM) $${f}.bak ; \ - done ; \ - fi diff --git a/README.md b/README.md index fe9a7c3787..94c512bd5e 100644 --- a/README.md +++ b/README.md @@ -24,7 +24,7 @@ In terms of [opam](https://opam.ocaml.org/doc/Install.html), it comes as the fol - [Authors](AUTHORS.md) - License: [CeCILL-C](LICENSE) -- Compatible Rocq versions: Coq 8.20, Rocq 9.0 (or dev) +- Compatible Rocq versions: Rocq 9.0 and 9.1 (or dev) - Additional dependencies: - [MathComp ssreflect 2.4.0 or later](https://math-comp.github.io) - [MathComp fingroup 2.4.0 or later](https://math-comp.github.io) diff --git a/coq-mathcomp-classical.opam b/coq-mathcomp-classical.opam index dd58126243..a8f231f6a3 100644 --- a/coq-mathcomp-classical.opam +++ b/coq-mathcomp-classical.opam @@ -15,8 +15,7 @@ the Coq proof-assistant and using the Mathematical Components library.""" build: [make "-C" "classical" "-j%{jobs}%"] install: [make "-C" "classical" "install"] depends: [ - ("coq" {>= "8.20" & < "8.21~"} - | "coq-core" { (>= "9.0" & < "9.2~") | (= "dev") }) + "coq-core" { (>= "9.0" & < "9.2~") | (= "dev") } "coq-mathcomp-ssreflect" { (>= "2.4.0" & < "2.6~") | (= "dev") } "coq-mathcomp-fingroup" "coq-mathcomp-algebra"