From 2046e7a7923ef863b3973720347b9e3e158ab252 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sat, 22 Jan 2022 12:04:04 +0100 Subject: [PATCH 1/2] Add %N for nat constants This is in preparation of https://github.com/math-comp/math-comp/pull/841 This is backward compatible (it only ensures that natural number constants will kee being interpreted in nat_scope when a number notation will be added in ring_scope). --- theories/abel.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/abel.v b/theories/abel.v index 08e7ee4..17e5f2d 100644 --- a/theories/abel.v +++ b/theories/abel.v @@ -1176,13 +1176,13 @@ pose simp := (rmorphB, rmorphD, map_polyZ, map_polyXn, map_polyX, map_polyC). by do !rewrite [map_poly _ _]simp/= ?natz. Qed. -Lemma size_poly_example_int : size poly_example_int = 6. +Lemma size_poly_example_int : size poly_example_int = 6%N. Proof. rewrite /poly_example_int -addrA size_addl ?size_polyXn//. by rewrite size_addl ?size_opp ?size_scale ?size_polyX -?polyCn ?size_polyC. Qed. -Lemma size_poly_example : size poly_example = 6. +Lemma size_poly_example : size poly_example = 6%N. Proof. rewrite /poly_example -addrA size_addl ?size_polyXn//. by rewrite size_addl ?size_opp ?size_scale ?size_polyX -?polyCn ?size_polyC. From bdc2dde746f8fbd71577021ddf5b1b5c2ac4cbb7 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sat, 22 Jan 2022 12:10:41 +0100 Subject: [PATCH 2/2] [CI] Add Coq 8.14 and 8.15 --- .github/workflows/docker-action.yml | 7 + .../workflows/nix-action-coq8.11+mc1.12.yml | 62 +++--- .../workflows/nix-action-coq8.11+mcmaster.yml | 137 +++++++----- .../workflows/nix-action-coq8.12+mc1.12.yml | 62 +++--- .../workflows/nix-action-coq8.12+mcmaster.yml | 137 +++++++----- .../workflows/nix-action-coq8.13+mc1.12.yml | 62 +++--- .../workflows/nix-action-coq8.13+mcmaster.yml | 137 +++++++----- .../workflows/nix-action-coq8.14+mc1.12.yml | 99 +++++++++ .../workflows/nix-action-coq8.14+mcmaster.yml | 199 ++++++++++++++++++ .../nix-action-coqmaster+mcmaster.yml | 199 ++++++++++++++++++ .nix/config.nix | 8 +- .nix/coq-nix-toolbox.nix | 2 +- coq-mathcomp-abel.opam | 4 +- 13 files changed, 828 insertions(+), 287 deletions(-) create mode 100644 .github/workflows/nix-action-coq8.14+mc1.12.yml create mode 100644 .github/workflows/nix-action-coq8.14+mcmaster.yml create mode 100644 .github/workflows/nix-action-coqmaster+mcmaster.yml diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index ee1e253..13a0bd1 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -21,10 +21,17 @@ jobs: - 'mathcomp/mathcomp:1.12.0-coq-8.11' - 'mathcomp/mathcomp:1.12.0-coq-8.12' - 'mathcomp/mathcomp:1.12.0-coq-8.13' + - 'mathcomp/mathcomp:1.12.0-coq-8.14' + - 'mathcomp/mathcomp:1.14.0-coq-8.11' + - 'mathcomp/mathcomp:1.14.0-coq-8.12' + - 'mathcomp/mathcomp:1.14.0-coq-8.13' + - 'mathcomp/mathcomp:1.14.0-coq-8.14' + - 'mathcomp/mathcomp:1.14.0-coq-8.15' - 'mathcomp/mathcomp-dev:coq-8.11' - 'mathcomp/mathcomp-dev:coq-8.12' - 'mathcomp/mathcomp-dev:coq-8.13' - 'mathcomp/mathcomp-dev:coq-8.14' + - 'mathcomp/mathcomp-dev:coq-8.15' - 'mathcomp/mathcomp-dev:coq-dev' fail-fast: false steps: diff --git a/.github/workflows/nix-action-coq8.11+mc1.12.yml b/.github/workflows/nix-action-coq8.11+mc1.12.yml index ddf49ac..ca35a10 100644 --- a/.github/workflows/nix-action-coq8.11+mc1.12.yml +++ b/.github/workflows/nix-action-coq8.11+mc1.12.yml @@ -3,41 +3,34 @@ jobs: needs: [] runs-on: ubuntu-latest steps: - - name: Determine which ref to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_ref=${{\ - \ github.ref }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + - 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 if [ -z \"$merge_commit\" ]; then\n echo \"tested_ref=refs/pull/${{\ - \ github.event.number }}/head\" >> $GITHUB_ENV\n else\n echo \"tested_ref=refs/pull/${{\ - \ github.event.number }}/merge\" >> $GITHUB_ENV\n fi\nfi\n" + \ | cut -f1)\n if [ -z \"$merge_commit\" ]; 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@v2 with: fetch-depth: 0 - ref: ${{ env.tested_ref }} + ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v12 + uses: cachix/install-nix-action@v16 with: nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq - uses: cachix/cachix-action@v8 - with: - name: coq - - name: Cachix setup coq-community - uses: cachix/cachix-action@v8 - with: - name: coq-community - name: Cachix setup math-comp - uses: cachix/cachix-action@v8 + uses: cachix/cachix-action@v10 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 \"coq8.11+mc1.12\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo ::set-output name=status::$(echo $nb_dry_run | grep \"built:\" | sed\ - \ \"s/.*/built/\")\n" + echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\")\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 "coq8.11+mc1.12" @@ -47,41 +40,34 @@ jobs: - coq runs-on: ubuntu-latest steps: - - name: Determine which ref to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_ref=${{\ - \ github.ref }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + - 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 if [ -z \"$merge_commit\" ]; then\n echo \"tested_ref=refs/pull/${{\ - \ github.event.number }}/head\" >> $GITHUB_ENV\n else\n echo \"tested_ref=refs/pull/${{\ - \ github.event.number }}/merge\" >> $GITHUB_ENV\n fi\nfi\n" + \ | cut -f1)\n if [ -z \"$merge_commit\" ]; 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@v2 with: fetch-depth: 0 - ref: ${{ env.tested_ref }} + ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v12 + uses: cachix/install-nix-action@v16 with: nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq - uses: cachix/cachix-action@v8 - with: - name: coq - - name: Cachix setup coq-community - uses: cachix/cachix-action@v8 - with: - name: coq-community - name: Cachix setup math-comp - uses: cachix/cachix-action@v8 + uses: cachix/cachix-action@v10 with: authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community name: math-comp - id: stepCheck name: Checking presence of CI target mathcomp-abel run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"coq8.11+mc1.12\" --argstr job \"mathcomp-abel\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho ::set-output name=status::$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\")\n" + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\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 "coq8.11+mc1.12" diff --git a/.github/workflows/nix-action-coq8.11+mcmaster.yml b/.github/workflows/nix-action-coq8.11+mcmaster.yml index 8935e4f..4213188 100644 --- a/.github/workflows/nix-action-coq8.11+mcmaster.yml +++ b/.github/workflows/nix-action-coq8.11+mcmaster.yml @@ -3,41 +3,34 @@ jobs: needs: [] runs-on: ubuntu-latest steps: - - name: Determine which ref to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_ref=${{\ - \ github.ref }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + - 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 if [ -z \"$merge_commit\" ]; then\n echo \"tested_ref=refs/pull/${{\ - \ github.event.number }}/head\" >> $GITHUB_ENV\n else\n echo \"tested_ref=refs/pull/${{\ - \ github.event.number }}/merge\" >> $GITHUB_ENV\n fi\nfi\n" + \ | cut -f1)\n if [ -z \"$merge_commit\" ]; 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@v2 with: fetch-depth: 0 - ref: ${{ env.tested_ref }} + ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v12 + uses: cachix/install-nix-action@v16 with: nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq - uses: cachix/cachix-action@v8 - with: - name: coq - - name: Cachix setup coq-community - uses: cachix/cachix-action@v8 - with: - name: coq-community - name: Cachix setup math-comp - uses: cachix/cachix-action@v8 + uses: cachix/cachix-action@v10 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 \"coq8.11+mcmaster\" --argstr job \"coq\" \\\n --dry-run 2>&1 >\ - \ /dev/null)\necho ::set-output name=status::$(echo $nb_dry_run | grep \"\ - built:\" | sed \"s/.*/built/\")\n" + \ /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ + \ | grep \"built:\" | sed \"s/.*/built/\")\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 "coq8.11+mcmaster" @@ -48,41 +41,34 @@ jobs: - mathcomp-real-closed runs-on: ubuntu-latest steps: - - name: Determine which ref to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_ref=${{\ - \ github.ref }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + - 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 if [ -z \"$merge_commit\" ]; then\n echo \"tested_ref=refs/pull/${{\ - \ github.event.number }}/head\" >> $GITHUB_ENV\n else\n echo \"tested_ref=refs/pull/${{\ - \ github.event.number }}/merge\" >> $GITHUB_ENV\n fi\nfi\n" + \ | cut -f1)\n if [ -z \"$merge_commit\" ]; 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@v2 with: fetch-depth: 0 - ref: ${{ env.tested_ref }} + ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v12 + uses: cachix/install-nix-action@v16 with: nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq - uses: cachix/cachix-action@v8 - with: - name: coq - - name: Cachix setup coq-community - uses: cachix/cachix-action@v8 - with: - name: coq-community - name: Cachix setup math-comp - uses: cachix/cachix-action@v8 + uses: cachix/cachix-action@v10 with: authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community name: math-comp - id: stepCheck name: Checking presence of CI target mathcomp-abel run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"coq8.11+mcmaster\" --argstr job \"mathcomp-abel\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho ::set-output name=status::$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\")\n" + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\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 "coq8.11+mcmaster" @@ -99,46 +85,85 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.11+mcmaster" --argstr job "mathcomp-abel" - mathcomp-real-closed: + mathcomp-bigenough: needs: - coq runs-on: ubuntu-latest steps: - - name: Determine which ref to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_ref=${{\ - \ github.ref }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + - 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 if [ -z \"$merge_commit\" ]; then\n echo \"tested_ref=refs/pull/${{\ - \ github.event.number }}/head\" >> $GITHUB_ENV\n else\n echo \"tested_ref=refs/pull/${{\ - \ github.event.number }}/merge\" >> $GITHUB_ENV\n fi\nfi\n" + \ | cut -f1)\n if [ -z \"$merge_commit\" ]; 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@v2 with: fetch-depth: 0 - ref: ${{ env.tested_ref }} + ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v12 + uses: cachix/install-nix-action@v16 with: nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq - uses: cachix/cachix-action@v8 + - name: Cachix setup math-comp + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target mathcomp-bigenough + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq8.11+mcmaster\" --argstr job \"mathcomp-bigenough\" \\\n --dry-run\ + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\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 "coq8.11+mcmaster" + --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 "coq8.11+mcmaster" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.11+mcmaster" + --argstr job "mathcomp-bigenough" + mathcomp-real-closed: + needs: + - coq + - mathcomp-bigenough + runs-on: ubuntu-latest + steps: + - 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 if [ -z \"$merge_commit\" ]; 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@v2 with: - name: coq - - name: Cachix setup coq-community - uses: cachix/cachix-action@v8 + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 with: - name: coq-community + nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup math-comp - uses: cachix/cachix-action@v8 + uses: cachix/cachix-action@v10 with: authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community name: math-comp - id: stepCheck name: Checking presence of CI target mathcomp-real-closed run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"coq8.11+mcmaster\" --argstr job \"mathcomp-real-closed\" \\\n \ - \ --dry-run 2>&1 > /dev/null)\necho ::set-output name=status::$(echo $nb_dry_run\ - \ | grep \"built:\" | sed \"s/.*/built/\")\n" + \ --dry-run 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\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 "coq8.11+mcmaster" diff --git a/.github/workflows/nix-action-coq8.12+mc1.12.yml b/.github/workflows/nix-action-coq8.12+mc1.12.yml index 78a6c18..115c249 100644 --- a/.github/workflows/nix-action-coq8.12+mc1.12.yml +++ b/.github/workflows/nix-action-coq8.12+mc1.12.yml @@ -3,41 +3,34 @@ jobs: needs: [] runs-on: ubuntu-latest steps: - - name: Determine which ref to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_ref=${{\ - \ github.ref }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + - 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 if [ -z \"$merge_commit\" ]; then\n echo \"tested_ref=refs/pull/${{\ - \ github.event.number }}/head\" >> $GITHUB_ENV\n else\n echo \"tested_ref=refs/pull/${{\ - \ github.event.number }}/merge\" >> $GITHUB_ENV\n fi\nfi\n" + \ | cut -f1)\n if [ -z \"$merge_commit\" ]; 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@v2 with: fetch-depth: 0 - ref: ${{ env.tested_ref }} + ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v12 + uses: cachix/install-nix-action@v16 with: nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq - uses: cachix/cachix-action@v8 - with: - name: coq - - name: Cachix setup coq-community - uses: cachix/cachix-action@v8 - with: - name: coq-community - name: Cachix setup math-comp - uses: cachix/cachix-action@v8 + uses: cachix/cachix-action@v10 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 \"coq8.12+mc1.12\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo ::set-output name=status::$(echo $nb_dry_run | grep \"built:\" | sed\ - \ \"s/.*/built/\")\n" + echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\")\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 "coq8.12+mc1.12" @@ -47,41 +40,34 @@ jobs: - coq runs-on: ubuntu-latest steps: - - name: Determine which ref to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_ref=${{\ - \ github.ref }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + - 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 if [ -z \"$merge_commit\" ]; then\n echo \"tested_ref=refs/pull/${{\ - \ github.event.number }}/head\" >> $GITHUB_ENV\n else\n echo \"tested_ref=refs/pull/${{\ - \ github.event.number }}/merge\" >> $GITHUB_ENV\n fi\nfi\n" + \ | cut -f1)\n if [ -z \"$merge_commit\" ]; 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@v2 with: fetch-depth: 0 - ref: ${{ env.tested_ref }} + ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v12 + uses: cachix/install-nix-action@v16 with: nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq - uses: cachix/cachix-action@v8 - with: - name: coq - - name: Cachix setup coq-community - uses: cachix/cachix-action@v8 - with: - name: coq-community - name: Cachix setup math-comp - uses: cachix/cachix-action@v8 + uses: cachix/cachix-action@v10 with: authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community name: math-comp - id: stepCheck name: Checking presence of CI target mathcomp-abel run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"coq8.12+mc1.12\" --argstr job \"mathcomp-abel\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho ::set-output name=status::$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\")\n" + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\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 "coq8.12+mc1.12" diff --git a/.github/workflows/nix-action-coq8.12+mcmaster.yml b/.github/workflows/nix-action-coq8.12+mcmaster.yml index 3e0468a..52a645a 100644 --- a/.github/workflows/nix-action-coq8.12+mcmaster.yml +++ b/.github/workflows/nix-action-coq8.12+mcmaster.yml @@ -3,41 +3,34 @@ jobs: needs: [] runs-on: ubuntu-latest steps: - - name: Determine which ref to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_ref=${{\ - \ github.ref }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + - 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 if [ -z \"$merge_commit\" ]; then\n echo \"tested_ref=refs/pull/${{\ - \ github.event.number }}/head\" >> $GITHUB_ENV\n else\n echo \"tested_ref=refs/pull/${{\ - \ github.event.number }}/merge\" >> $GITHUB_ENV\n fi\nfi\n" + \ | cut -f1)\n if [ -z \"$merge_commit\" ]; 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@v2 with: fetch-depth: 0 - ref: ${{ env.tested_ref }} + ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v12 + uses: cachix/install-nix-action@v16 with: nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq - uses: cachix/cachix-action@v8 - with: - name: coq - - name: Cachix setup coq-community - uses: cachix/cachix-action@v8 - with: - name: coq-community - name: Cachix setup math-comp - uses: cachix/cachix-action@v8 + uses: cachix/cachix-action@v10 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 \"coq8.12+mcmaster\" --argstr job \"coq\" \\\n --dry-run 2>&1 >\ - \ /dev/null)\necho ::set-output name=status::$(echo $nb_dry_run | grep \"\ - built:\" | sed \"s/.*/built/\")\n" + \ /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ + \ | grep \"built:\" | sed \"s/.*/built/\")\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 "coq8.12+mcmaster" @@ -48,41 +41,34 @@ jobs: - mathcomp-real-closed runs-on: ubuntu-latest steps: - - name: Determine which ref to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_ref=${{\ - \ github.ref }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + - 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 if [ -z \"$merge_commit\" ]; then\n echo \"tested_ref=refs/pull/${{\ - \ github.event.number }}/head\" >> $GITHUB_ENV\n else\n echo \"tested_ref=refs/pull/${{\ - \ github.event.number }}/merge\" >> $GITHUB_ENV\n fi\nfi\n" + \ | cut -f1)\n if [ -z \"$merge_commit\" ]; 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@v2 with: fetch-depth: 0 - ref: ${{ env.tested_ref }} + ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v12 + uses: cachix/install-nix-action@v16 with: nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq - uses: cachix/cachix-action@v8 - with: - name: coq - - name: Cachix setup coq-community - uses: cachix/cachix-action@v8 - with: - name: coq-community - name: Cachix setup math-comp - uses: cachix/cachix-action@v8 + uses: cachix/cachix-action@v10 with: authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community name: math-comp - id: stepCheck name: Checking presence of CI target mathcomp-abel run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"coq8.12+mcmaster\" --argstr job \"mathcomp-abel\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho ::set-output name=status::$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\")\n" + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\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 "coq8.12+mcmaster" @@ -99,46 +85,85 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.12+mcmaster" --argstr job "mathcomp-abel" - mathcomp-real-closed: + mathcomp-bigenough: needs: - coq runs-on: ubuntu-latest steps: - - name: Determine which ref to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_ref=${{\ - \ github.ref }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + - 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 if [ -z \"$merge_commit\" ]; then\n echo \"tested_ref=refs/pull/${{\ - \ github.event.number }}/head\" >> $GITHUB_ENV\n else\n echo \"tested_ref=refs/pull/${{\ - \ github.event.number }}/merge\" >> $GITHUB_ENV\n fi\nfi\n" + \ | cut -f1)\n if [ -z \"$merge_commit\" ]; 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@v2 with: fetch-depth: 0 - ref: ${{ env.tested_ref }} + ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v12 + uses: cachix/install-nix-action@v16 with: nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq - uses: cachix/cachix-action@v8 + - name: Cachix setup math-comp + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target mathcomp-bigenough + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq8.12+mcmaster\" --argstr job \"mathcomp-bigenough\" \\\n --dry-run\ + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\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 "coq8.12+mcmaster" + --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 "coq8.12+mcmaster" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.12+mcmaster" + --argstr job "mathcomp-bigenough" + mathcomp-real-closed: + needs: + - coq + - mathcomp-bigenough + runs-on: ubuntu-latest + steps: + - 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 if [ -z \"$merge_commit\" ]; 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@v2 with: - name: coq - - name: Cachix setup coq-community - uses: cachix/cachix-action@v8 + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 with: - name: coq-community + nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup math-comp - uses: cachix/cachix-action@v8 + uses: cachix/cachix-action@v10 with: authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community name: math-comp - id: stepCheck name: Checking presence of CI target mathcomp-real-closed run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"coq8.12+mcmaster\" --argstr job \"mathcomp-real-closed\" \\\n \ - \ --dry-run 2>&1 > /dev/null)\necho ::set-output name=status::$(echo $nb_dry_run\ - \ | grep \"built:\" | sed \"s/.*/built/\")\n" + \ --dry-run 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\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 "coq8.12+mcmaster" diff --git a/.github/workflows/nix-action-coq8.13+mc1.12.yml b/.github/workflows/nix-action-coq8.13+mc1.12.yml index 752d190..aef5479 100644 --- a/.github/workflows/nix-action-coq8.13+mc1.12.yml +++ b/.github/workflows/nix-action-coq8.13+mc1.12.yml @@ -3,41 +3,34 @@ jobs: needs: [] runs-on: ubuntu-latest steps: - - name: Determine which ref to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_ref=${{\ - \ github.ref }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + - 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 if [ -z \"$merge_commit\" ]; then\n echo \"tested_ref=refs/pull/${{\ - \ github.event.number }}/head\" >> $GITHUB_ENV\n else\n echo \"tested_ref=refs/pull/${{\ - \ github.event.number }}/merge\" >> $GITHUB_ENV\n fi\nfi\n" + \ | cut -f1)\n if [ -z \"$merge_commit\" ]; 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@v2 with: fetch-depth: 0 - ref: ${{ env.tested_ref }} + ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v12 + uses: cachix/install-nix-action@v16 with: nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq - uses: cachix/cachix-action@v8 - with: - name: coq - - name: Cachix setup coq-community - uses: cachix/cachix-action@v8 - with: - name: coq-community - name: Cachix setup math-comp - uses: cachix/cachix-action@v8 + uses: cachix/cachix-action@v10 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 \"coq8.13+mc1.12\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo ::set-output name=status::$(echo $nb_dry_run | grep \"built:\" | sed\ - \ \"s/.*/built/\")\n" + echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\")\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 "coq8.13+mc1.12" @@ -47,41 +40,34 @@ jobs: - coq runs-on: ubuntu-latest steps: - - name: Determine which ref to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_ref=${{\ - \ github.ref }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + - 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 if [ -z \"$merge_commit\" ]; then\n echo \"tested_ref=refs/pull/${{\ - \ github.event.number }}/head\" >> $GITHUB_ENV\n else\n echo \"tested_ref=refs/pull/${{\ - \ github.event.number }}/merge\" >> $GITHUB_ENV\n fi\nfi\n" + \ | cut -f1)\n if [ -z \"$merge_commit\" ]; 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@v2 with: fetch-depth: 0 - ref: ${{ env.tested_ref }} + ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v12 + uses: cachix/install-nix-action@v16 with: nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq - uses: cachix/cachix-action@v8 - with: - name: coq - - name: Cachix setup coq-community - uses: cachix/cachix-action@v8 - with: - name: coq-community - name: Cachix setup math-comp - uses: cachix/cachix-action@v8 + uses: cachix/cachix-action@v10 with: authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community name: math-comp - id: stepCheck name: Checking presence of CI target mathcomp-abel run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"coq8.13+mc1.12\" --argstr job \"mathcomp-abel\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho ::set-output name=status::$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\")\n" + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\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 "coq8.13+mc1.12" diff --git a/.github/workflows/nix-action-coq8.13+mcmaster.yml b/.github/workflows/nix-action-coq8.13+mcmaster.yml index 2504cee..b2c2902 100644 --- a/.github/workflows/nix-action-coq8.13+mcmaster.yml +++ b/.github/workflows/nix-action-coq8.13+mcmaster.yml @@ -3,41 +3,34 @@ jobs: needs: [] runs-on: ubuntu-latest steps: - - name: Determine which ref to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_ref=${{\ - \ github.ref }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + - 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 if [ -z \"$merge_commit\" ]; then\n echo \"tested_ref=refs/pull/${{\ - \ github.event.number }}/head\" >> $GITHUB_ENV\n else\n echo \"tested_ref=refs/pull/${{\ - \ github.event.number }}/merge\" >> $GITHUB_ENV\n fi\nfi\n" + \ | cut -f1)\n if [ -z \"$merge_commit\" ]; 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@v2 with: fetch-depth: 0 - ref: ${{ env.tested_ref }} + ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v12 + uses: cachix/install-nix-action@v16 with: nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq - uses: cachix/cachix-action@v8 - with: - name: coq - - name: Cachix setup coq-community - uses: cachix/cachix-action@v8 - with: - name: coq-community - name: Cachix setup math-comp - uses: cachix/cachix-action@v8 + uses: cachix/cachix-action@v10 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 \"coq8.13+mcmaster\" --argstr job \"coq\" \\\n --dry-run 2>&1 >\ - \ /dev/null)\necho ::set-output name=status::$(echo $nb_dry_run | grep \"\ - built:\" | sed \"s/.*/built/\")\n" + \ /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ + \ | grep \"built:\" | sed \"s/.*/built/\")\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 "coq8.13+mcmaster" @@ -48,41 +41,34 @@ jobs: - mathcomp-real-closed runs-on: ubuntu-latest steps: - - name: Determine which ref to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_ref=${{\ - \ github.ref }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + - 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 if [ -z \"$merge_commit\" ]; then\n echo \"tested_ref=refs/pull/${{\ - \ github.event.number }}/head\" >> $GITHUB_ENV\n else\n echo \"tested_ref=refs/pull/${{\ - \ github.event.number }}/merge\" >> $GITHUB_ENV\n fi\nfi\n" + \ | cut -f1)\n if [ -z \"$merge_commit\" ]; 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@v2 with: fetch-depth: 0 - ref: ${{ env.tested_ref }} + ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v12 + uses: cachix/install-nix-action@v16 with: nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq - uses: cachix/cachix-action@v8 - with: - name: coq - - name: Cachix setup coq-community - uses: cachix/cachix-action@v8 - with: - name: coq-community - name: Cachix setup math-comp - uses: cachix/cachix-action@v8 + uses: cachix/cachix-action@v10 with: authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community name: math-comp - id: stepCheck name: Checking presence of CI target mathcomp-abel run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"coq8.13+mcmaster\" --argstr job \"mathcomp-abel\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho ::set-output name=status::$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\")\n" + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\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 "coq8.13+mcmaster" @@ -99,46 +85,85 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.13+mcmaster" --argstr job "mathcomp-abel" - mathcomp-real-closed: + mathcomp-bigenough: needs: - coq runs-on: ubuntu-latest steps: - - name: Determine which ref to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_ref=${{\ - \ github.ref }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + - 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 if [ -z \"$merge_commit\" ]; then\n echo \"tested_ref=refs/pull/${{\ - \ github.event.number }}/head\" >> $GITHUB_ENV\n else\n echo \"tested_ref=refs/pull/${{\ - \ github.event.number }}/merge\" >> $GITHUB_ENV\n fi\nfi\n" + \ | cut -f1)\n if [ -z \"$merge_commit\" ]; 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@v2 with: fetch-depth: 0 - ref: ${{ env.tested_ref }} + ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v12 + uses: cachix/install-nix-action@v16 with: nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq - uses: cachix/cachix-action@v8 + - name: Cachix setup math-comp + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target mathcomp-bigenough + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq8.13+mcmaster\" --argstr job \"mathcomp-bigenough\" \\\n --dry-run\ + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\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 "coq8.13+mcmaster" + --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 "coq8.13+mcmaster" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.13+mcmaster" + --argstr job "mathcomp-bigenough" + mathcomp-real-closed: + needs: + - coq + - mathcomp-bigenough + runs-on: ubuntu-latest + steps: + - 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 if [ -z \"$merge_commit\" ]; 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@v2 with: - name: coq - - name: Cachix setup coq-community - uses: cachix/cachix-action@v8 + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 with: - name: coq-community + nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup math-comp - uses: cachix/cachix-action@v8 + uses: cachix/cachix-action@v10 with: authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community name: math-comp - id: stepCheck name: Checking presence of CI target mathcomp-real-closed run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"coq8.13+mcmaster\" --argstr job \"mathcomp-real-closed\" \\\n \ - \ --dry-run 2>&1 > /dev/null)\necho ::set-output name=status::$(echo $nb_dry_run\ - \ | grep \"built:\" | sed \"s/.*/built/\")\n" + \ --dry-run 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\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 "coq8.13+mcmaster" diff --git a/.github/workflows/nix-action-coq8.14+mc1.12.yml b/.github/workflows/nix-action-coq8.14+mc1.12.yml new file mode 100644 index 0000000..c05c806 --- /dev/null +++ b/.github/workflows/nix-action-coq8.14+mc1.12.yml @@ -0,0 +1,99 @@ +jobs: + coq: + needs: [] + runs-on: ubuntu-latest + steps: + - 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 if [ -z \"$merge_commit\" ]; 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@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v10 + 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 \"coq8.14+mc1.12\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\")\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 "coq8.14+mc1.12" + --argstr job "coq" + mathcomp-abel: + needs: + - coq + runs-on: ubuntu-latest + steps: + - 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 if [ -z \"$merge_commit\" ]; 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@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target mathcomp-abel + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq8.14+mc1.12\" --argstr job \"mathcomp-abel\" \\\n --dry-run\ + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\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 "coq8.14+mc1.12" + --argstr job "coq" + - 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 "coq8.14+mc1.12" + --argstr job "mathcomp-field" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-real-closed' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mc1.12" + --argstr job "mathcomp-real-closed" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mc1.12" + --argstr job "mathcomp-abel" +name: Nix CI for bundle coq8.14+mc1.12 +'on': + pull_request: + paths: + - .github/workflows/** + pull_request_target: + types: + - opened + - synchronize + - reopened + push: + branches: + - master diff --git a/.github/workflows/nix-action-coq8.14+mcmaster.yml b/.github/workflows/nix-action-coq8.14+mcmaster.yml new file mode 100644 index 0000000..ad0594a --- /dev/null +++ b/.github/workflows/nix-action-coq8.14+mcmaster.yml @@ -0,0 +1,199 @@ +jobs: + coq: + needs: [] + runs-on: ubuntu-latest + steps: + - 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 if [ -z \"$merge_commit\" ]; 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@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v10 + 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 \"coq8.14+mcmaster\" --argstr job \"coq\" \\\n --dry-run 2>&1 >\ + \ /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ + \ | grep \"built:\" | sed \"s/.*/built/\")\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 "coq8.14+mcmaster" + --argstr job "coq" + mathcomp-abel: + needs: + - coq + - mathcomp-real-closed + runs-on: ubuntu-latest + steps: + - 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 if [ -z \"$merge_commit\" ]; 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@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target mathcomp-abel + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq8.14+mcmaster\" --argstr job \"mathcomp-abel\" \\\n --dry-run\ + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\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 "coq8.14+mcmaster" + --argstr job "coq" + - 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 "coq8.14+mcmaster" + --argstr job "mathcomp-field" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-real-closed' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mcmaster" + --argstr job "mathcomp-real-closed" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mcmaster" + --argstr job "mathcomp-abel" + mathcomp-bigenough: + needs: + - coq + runs-on: ubuntu-latest + steps: + - 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 if [ -z \"$merge_commit\" ]; 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@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target mathcomp-bigenough + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq8.14+mcmaster\" --argstr job \"mathcomp-bigenough\" \\\n --dry-run\ + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\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 "coq8.14+mcmaster" + --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 "coq8.14+mcmaster" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mcmaster" + --argstr job "mathcomp-bigenough" + mathcomp-real-closed: + needs: + - coq + - mathcomp-bigenough + runs-on: ubuntu-latest + steps: + - 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 if [ -z \"$merge_commit\" ]; 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@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target mathcomp-real-closed + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq8.14+mcmaster\" --argstr job \"mathcomp-real-closed\" \\\n \ + \ --dry-run 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\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 "coq8.14+mcmaster" + --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 "coq8.14+mcmaster" + --argstr job "mathcomp-ssreflect" + - 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 "coq8.14+mcmaster" + --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 "coq8.14+mcmaster" + --argstr job "mathcomp-bigenough" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.14+mcmaster" + --argstr job "mathcomp-real-closed" +name: Nix CI for bundle coq8.14+mcmaster +'on': + pull_request: + paths: + - .github/workflows/** + pull_request_target: + types: + - opened + - synchronize + - reopened + push: + branches: + - master diff --git a/.github/workflows/nix-action-coqmaster+mcmaster.yml b/.github/workflows/nix-action-coqmaster+mcmaster.yml new file mode 100644 index 0000000..4baf4bb --- /dev/null +++ b/.github/workflows/nix-action-coqmaster+mcmaster.yml @@ -0,0 +1,199 @@ +jobs: + coq: + needs: [] + runs-on: ubuntu-latest + steps: + - 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 if [ -z \"$merge_commit\" ]; 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@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v10 + 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 \"coqmaster+mcmaster\" --argstr job \"coq\" \\\n --dry-run 2>&1\ + \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ + \ | grep \"built:\" | sed \"s/.*/built/\")\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 "coqmaster+mcmaster" + --argstr job "coq" + mathcomp-abel: + needs: + - coq + - mathcomp-real-closed + runs-on: ubuntu-latest + steps: + - 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 if [ -z \"$merge_commit\" ]; 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@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target mathcomp-abel + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coqmaster+mcmaster\" --argstr job \"mathcomp-abel\" \\\n --dry-run\ + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\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 "coqmaster+mcmaster" + --argstr job "coq" + - 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 "coqmaster+mcmaster" + --argstr job "mathcomp-field" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-real-closed' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coqmaster+mcmaster" + --argstr job "mathcomp-real-closed" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coqmaster+mcmaster" + --argstr job "mathcomp-abel" + mathcomp-bigenough: + needs: + - coq + runs-on: ubuntu-latest + steps: + - 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 if [ -z \"$merge_commit\" ]; 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@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target mathcomp-bigenough + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coqmaster+mcmaster\" --argstr job \"mathcomp-bigenough\" \\\n \ + \ --dry-run 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\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 "coqmaster+mcmaster" + --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 "coqmaster+mcmaster" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coqmaster+mcmaster" + --argstr job "mathcomp-bigenough" + mathcomp-real-closed: + needs: + - coq + - mathcomp-bigenough + runs-on: ubuntu-latest + steps: + - 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 if [ -z \"$merge_commit\" ]; 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@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target mathcomp-real-closed + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coqmaster+mcmaster\" --argstr job \"mathcomp-real-closed\" \\\n\ + \ --dry-run 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\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 "coqmaster+mcmaster" + --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 "coqmaster+mcmaster" + --argstr job "mathcomp-ssreflect" + - 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 "coqmaster+mcmaster" + --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 "coqmaster+mcmaster" + --argstr job "mathcomp-bigenough" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coqmaster+mcmaster" + --argstr job "mathcomp-real-closed" +name: Nix CI for bundle coqmaster+mcmaster +'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 49eeb96..5e57c51 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 = "coq8.13+mc1.12"; + default-bundle = "coq8.14+mc1.12"; ## write one `bundles.name` attribute set per ## alternative configuration @@ -45,14 +45,18 @@ mathcomp.job = false; } // (if (mcv == "master") then { mathcomp-real-closed.override.version = "master"; + mathcomp-bigenough.override.version = "1.0.1"; } else {}); }; in gen "8.11" "1.12" // gen "8.12" "1.12" // gen "8.13" "1.12" // + gen "8.14" "1.12" // gen "8.11" "master" // gen "8.12" "master" // - gen "8.13" "master"; + gen "8.13" "master" // + gen "8.14" "master" // + gen "master" "master"; ## Cachix caches to use in CI ## Below we list some standard ones diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index 8fbacb8..dfe7d7a 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"6d7dff56a09dc6ab6209a061fea9eef60bd08429" +"d7085993c05f91421f0c169816396d59edb4c920" diff --git a/coq-mathcomp-abel.opam b/coq-mathcomp-abel.opam index ac26d3b..8f2256a 100644 --- a/coq-mathcomp-abel.opam +++ b/coq-mathcomp-abel.opam @@ -21,8 +21,8 @@ Mathematical Components library.""" build: [make "-j%{jobs}%"] install: [make "install"] depends: [ - "coq" { (>= "8.10" & < "8.15~") | = "dev" } - "coq-mathcomp-ssreflect" { (>= "1.12.0" & < "1.14~") | = "dev" } + "coq" { (>= "8.10" & < "8.16~") | = "dev" } + "coq-mathcomp-ssreflect" { (>= "1.12.0" & < "1.15~") | = "dev" } "coq-mathcomp-fingroup" "coq-mathcomp-algebra" "coq-mathcomp-solvable"