From abbb269cc187c8345b9e184e1f7d48b1ecd8e154 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Mon, 15 Jan 2024 17:09:43 +0100 Subject: [PATCH 1/2] Drop Coq 8.14 and MC 1.15 and 1.16 support --- .github/workflows/docker-action.yml | 5 +- .github/workflows/nix-action-8.14.yml | 201 -------------------------- .nix/config.nix | 1 - INSTALL.md | 10 +- README.md | 2 +- coq-mathcomp-analysis.opam | 2 +- coq-mathcomp-classical.opam | 4 +- 7 files changed, 10 insertions(+), 215 deletions(-) delete mode 100644 .github/workflows/nix-action-8.14.yml diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index efe7aa0b9..4b0c9b7a0 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -15,13 +15,10 @@ jobs: strategy: matrix: image: - - 'mathcomp/mathcomp:1.15.0-coq-8.14' - - 'mathcomp/mathcomp:1.15.0-coq-8.15' - - 'mathcomp/mathcomp:1.15.0-coq-8.16' - - 'mathcomp/mathcomp:1.16.0-coq-8.14' - 'mathcomp/mathcomp:1.17.0-coq-8.15' - 'mathcomp/mathcomp:1.17.0-coq-8.16' - 'mathcomp/mathcomp:1.17.0-coq-8.17' + - 'mathcomp/mathcomp:1.18.0-coq-8.18' fail-fast: false steps: - uses: actions/checkout@v2 diff --git a/.github/workflows/nix-action-8.14.yml b/.github/workflows/nix-action-8.14.yml deleted file mode 100644 index fc1f56e3d..000000000 --- a/.github/workflows/nix-action-8.14.yml +++ /dev/null @@ -1,201 +0,0 @@ -jobs: - coq: - 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@v3 - 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@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target coq - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.14\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ - s/.*/built/\") >> $GITHUB_OUTPUT\n" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.14" --argstr - job "coq" - mathcomp-analysis: - needs: - - coq - 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@v3 - 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@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target mathcomp-analysis - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.14\" --argstr job \"mathcomp-analysis\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\ - built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.14" --argstr - job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-classical' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.14" --argstr - job "mathcomp-classical" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.14" --argstr - job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-bigenough' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.14" --argstr - job "mathcomp-bigenough" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: hierarchy-builder' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.14" --argstr - job "hierarchy-builder" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.14" --argstr - job "mathcomp-analysis" - mathcomp-analysis-single: - needs: - - coq - 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@v3 - 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@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v20 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v12 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target mathcomp-analysis-single - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.14\" --argstr job \"mathcomp-analysis-single\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.14" --argstr - job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.14" --argstr - job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-finmap' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.14" --argstr - job "mathcomp-finmap" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.14" --argstr - job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-bigenough' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.14" --argstr - job "mathcomp-bigenough" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: hierarchy-builder' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.14" --argstr - job "hierarchy-builder" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.14" --argstr - job "mathcomp-analysis-single" -name: Nix CI for bundle 8.14 -'on': - pull_request: - paths: - - .github/workflows/** - pull_request_target: - types: - - opened - - synchronize - - reopened - push: - branches: - - master diff --git a/.nix/config.nix b/.nix/config.nix index cc858f180..45cbfaf14 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -37,7 +37,6 @@ ## alternative configuration ## When generating GitHub Action CI, one workflow file ## will be created per bundle - bundles."8.14".coqPackages.coq.override.version = "8.14"; bundles."8.15".coqPackages.coq.override.version = "8.15"; bundles."8.16".push-branches = [ "master" "hierarchy-builder" ]; bundles."8.16".coqPackages.coq.override.version = "8.16"; diff --git a/INSTALL.md b/INSTALL.md index fb7ee64fb..000e07ad1 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -2,9 +2,9 @@ ## Requirements -- [The Coq Proof Assistant version ≥ 8.14](https://coq.inria.fr) +- [The Coq Proof Assistant version ≥ 8.15](https://coq.inria.fr) - [Mathematical Components version ≥ 1.13.0](https://github.com/math-comp/math-comp) - + except `coq-mathcomp-solvable` ≥ 1.15.0 + + except `coq-mathcomp-solvable` ≥ 1.17.0 - [Finmap library version ≥ 1.5.1](https://github.com/math-comp/finmap) - [Hierarchy builder version >= 1.2.0](https://github.com/math-comp/hierarchy-builder) @@ -71,12 +71,12 @@ 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.14.0 and MathComp 1.13.0. For other versions, update the +With the example of Coq 8.15.0 and MathComp 1.13.0. For other versions, update the version numbers accordingly. -1. Install Coq 8.14.0 +1. Install Coq 8.15.0 ``` -$ opam install coq.8.14.0 +$ opam install coq.8.15.0 ``` 2. Install the Mathematical Components ``` diff --git a/README.md b/README.md index a7dbff5d4..2278a5a77 100644 --- a/README.md +++ b/README.md @@ -33,7 +33,7 @@ the Coq proof-assistant and using the Mathematical Components library. - Pierre-Yves Strub (initial) - Laurent Théry - License: [CeCILL-C](LICENSE) -- Compatible Coq versions: Coq 8.14 to 8.18 (or dev) +- Compatible Coq versions: Coq 8.15 to 8.18 (or dev) - Additional dependencies: - [MathComp ssreflect 1.13 or later](https://math-comp.github.io) - [MathComp fingroup 1.13 or later](https://math-comp.github.io) diff --git a/coq-mathcomp-analysis.opam b/coq-mathcomp-analysis.opam index cdba4bd54..7bc0a0325 100644 --- a/coq-mathcomp-analysis.opam +++ b/coq-mathcomp-analysis.opam @@ -19,7 +19,7 @@ build: [make "-C" "theories" "-j%{jobs}%"] install: [make "-C" "theories" "install"] depends: [ "coq-mathcomp-classical" { = version} - "coq-mathcomp-solvable" { (>= "1.15.0" & < "1.19~") | (= "dev") } + "coq-mathcomp-solvable" { (>= "1.17.0" & < "1.20~") | (= "dev") } "coq-mathcomp-field" "coq-mathcomp-bigenough" { (>= "1.0.0") } ] diff --git a/coq-mathcomp-classical.opam b/coq-mathcomp-classical.opam index 463a8dfa5..98e33e80c 100644 --- a/coq-mathcomp-classical.opam +++ b/coq-mathcomp-classical.opam @@ -18,8 +18,8 @@ the Coq proof-assistant and using the Mathematical Components library.""" build: [make "-C" "classical" "-j%{jobs}%"] install: [make "-C" "classical" "install"] depends: [ - "coq" { (>= "8.14" & < "8.19~") | (= "dev") } - "coq-mathcomp-ssreflect" { (>= "1.13.0" & < "1.19~") | (= "dev") } + "coq" { (>= "8.15" & < "8.19~") | (= "dev") } + "coq-mathcomp-ssreflect" { (>= "1.17.0" & < "1.20~") | (= "dev") } "coq-mathcomp-fingroup" "coq-mathcomp-algebra" "coq-mathcomp-finmap" { (>= "1.5.1" & < "1.6~") | (= "dev") } From ba96f45995d0026f9d82d679562c2acf20f67de1 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Mon, 15 Jan 2024 17:07:24 +0100 Subject: [PATCH 2/2] Add Coq 8.19 --- .github/workflows/docker-action.yml | 1 + .github/workflows/nix-action-8.19.yml | 272 ++++++++++++++++++++++++++ .nix/config.nix | 9 +- .nix/coq-nix-toolbox.nix | 2 +- coq-mathcomp-classical.opam | 2 +- 5 files changed, 283 insertions(+), 3 deletions(-) create mode 100644 .github/workflows/nix-action-8.19.yml diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 4b0c9b7a0..2275c619e 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -19,6 +19,7 @@ jobs: - 'mathcomp/mathcomp:1.17.0-coq-8.16' - 'mathcomp/mathcomp:1.17.0-coq-8.17' - 'mathcomp/mathcomp:1.18.0-coq-8.18' + - 'mathcomp/mathcomp:1.19.0-coq-8.19' fail-fast: false steps: - uses: actions/checkout@v2 diff --git a/.github/workflows/nix-action-8.19.yml b/.github/workflows/nix-action-8.19.yml new file mode 100644 index 000000000..25e3135b8 --- /dev/null +++ b/.github/workflows/nix-action-8.19.yml @@ -0,0 +1,272 @@ +jobs: + coq: + 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@v3 + 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@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target coq + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"8.19\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ + s/.*/built/\") >> $GITHUB_OUTPUT\n" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "coq" + mathcomp: + needs: + - coq + 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@v3 + 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@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target mathcomp + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"8.19\" --argstr job \"mathcomp\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ + s/.*/built/\") >> $GITHUB_OUTPUT\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-fingroup' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp-fingroup" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-algebra' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp-algebra" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-solvable' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp-solvable" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-field' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp-field" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-character' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp-character" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: hierarchy-builder' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "hierarchy-builder" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp" + mathcomp-analysis: + needs: + - coq + 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@v3 + 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@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target mathcomp-analysis + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"8.19\" --argstr job \"mathcomp-analysis\" \\\n --dry-run 2>&1\ + \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\ + built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-classical' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp-classical" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-field' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp-field" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: hierarchy-builder' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "hierarchy-builder" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp-analysis" + mathcomp-analysis-single: + needs: + - coq + 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@v3 + 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@v3 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target mathcomp-analysis-single + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"8.19\" --argstr job \"mathcomp-analysis-single\" \\\n --dry-run\ + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-algebra' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp-algebra" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-field' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp-field" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: hierarchy-builder' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "hierarchy-builder" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp-analysis-single" +name: Nix CI for bundle 8.19 +'on': + pull_request: + paths: + - .github/workflows/nix-action-8.19.yml + pull_request_target: + paths-ignore: + - .github/workflows/nix-action-8.19.yml + types: + - opened + - synchronize + - reopened + push: + branches: + - master + - hierarchy-builder diff --git a/.nix/config.nix b/.nix/config.nix index 45cbfaf14..c386d9a2c 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -31,7 +31,7 @@ ## select an entry to build in the following `bundles` set ## defaults to "default" - default-bundle = "8.15"; + default-bundle = "8.18"; ## write one `bundles.name` attribute set per ## alternative configuration @@ -44,6 +44,13 @@ bundles."8.17".coqPackages.coq.override.version = "8.17"; bundles."8.18".push-branches = [ "master" "hierarchy-builder" ]; bundles."8.18".coqPackages.coq.override.version = "8.18"; + bundles."8.19".push-branches = [ "master" "hierarchy-builder" ]; + bundles."8.19".coqPackages = { + coq.override.version = "8.19"; + mathcomp.override.version = "mathcomp-1.19.0"; + mathcomp-bigenough.override.version = "1.0.1"; + mathcomp-finmap.override.version = "1.5.2"; + }; bundles."master".push-branches = [ "master" "hierarchy-builder" ]; bundles."master".coqPackages = { diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index b0c3834f0..c654d4e24 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"7e631f043d424ce82f3308824bf64fbfdee04c80" +"e91399553b1efcadb7e90e5ff024ba540fcfc111" diff --git a/coq-mathcomp-classical.opam b/coq-mathcomp-classical.opam index 98e33e80c..1f2b1c898 100644 --- a/coq-mathcomp-classical.opam +++ b/coq-mathcomp-classical.opam @@ -18,7 +18,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.15" & < "8.19~") | (= "dev") } + "coq" { (>= "8.15" & < "8.20~") | (= "dev") } "coq-mathcomp-ssreflect" { (>= "1.17.0" & < "1.20~") | (= "dev") } "coq-mathcomp-fingroup" "coq-mathcomp-algebra"