diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index efe7aa0b9..2275c619e 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -15,13 +15,11 @@ 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' + - 'mathcomp/mathcomp:1.19.0-coq-8.19' fail-fast: false steps: - uses: actions/checkout@v2 diff --git a/.github/workflows/nix-action-8.14.yml b/.github/workflows/nix-action-8.19.yml similarity index 66% rename from .github/workflows/nix-action-8.14.yml rename to .github/workflows/nix-action-8.19.yml index fc1f56e3d..25e3135b8 100644 --- a/.github/workflows/nix-action-8.14.yml +++ b/.github/workflows/nix-action-8.19.yml @@ -39,13 +39,93 @@ jobs: - 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\ + \ 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.14" --argstr + 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 @@ -87,32 +167,28 @@ jobs: - 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\ + \ 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.14" --argstr + 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.14" --argstr + 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.14" --argstr + 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-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 + 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.14" --argstr + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr job "mathcomp-analysis" mathcomp-analysis-single: needs: @@ -155,43 +231,37 @@ jobs: - 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\ + \ 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.14" --argstr + 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.14" --argstr + 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-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 + 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-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 + 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.14" --argstr + 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.14 +name: Nix CI for bundle 8.19 'on': pull_request: paths: - - .github/workflows/** + - .github/workflows/nix-action-8.19.yml pull_request_target: + paths-ignore: + - .github/workflows/nix-action-8.19.yml types: - opened - synchronize @@ -199,3 +269,4 @@ name: Nix CI for bundle 8.14 push: branches: - master + - hierarchy-builder diff --git a/.nix/config.nix b/.nix/config.nix index cc858f180..c386d9a2c 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -31,13 +31,12 @@ ## 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 ## 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"; @@ -45,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/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..1f2b1c898 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.20~") | (= "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") }