From 57c04eae064bafd47dc4a2d63ae68eaa18f7f36f Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 28 Sep 2022 15:34:39 +0200 Subject: [PATCH] Update nix & opam --- .github/workflows/nix-action-coq-8.15.yml | 71 ++- .github/workflows/nix-action-coq-8.16.yml | 61 +- .../workflows/nix-action-coq-mcHB-8.16.yml | 567 +++++++++++++++++- .nix/coq-nix-toolbox.nix | 2 +- coq-hierarchy-builder-shim.opam | 2 +- coq-hierarchy-builder.opam | 2 +- 6 files changed, 643 insertions(+), 62 deletions(-) diff --git a/.github/workflows/nix-action-coq-8.15.yml b/.github/workflows/nix-action-coq-8.15.yml index c02f572e4..af72e4639 100644 --- a/.github/workflows/nix-action-coq-8.15.yml +++ b/.github/workflows/nix-action-coq-8.15.yml @@ -141,6 +141,7 @@ jobs: mathcomp-analysis: needs: - coq + - mathcomp-classical - hierarchy-builder runs-on: ubuntu-latest steps: @@ -176,18 +177,10 @@ jobs: name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15" --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 "coq-8.15" - --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 "coq-8.15" --argstr job "mathcomp-field" - - 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 "coq-8.15" - --argstr job "mathcomp-finmap" - 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 "coq-8.15" @@ -196,6 +189,10 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-real-closed' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15" --argstr job "mathcomp-real-closed" + - 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 "coq-8.15" + --argstr job "mathcomp-classical" - 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 "coq-8.15" @@ -204,6 +201,64 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15" --argstr job "mathcomp-analysis" + mathcomp-classical: + needs: + - coq + - hierarchy-builder + 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-classical + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-8.15\" --argstr job \"mathcomp-classical\" \\\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 "coq-8.15" + --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 "coq-8.15" + --argstr job "mathcomp-ssreflect" + - 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 "coq-8.15" + --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 "coq-8.15" + --argstr job "mathcomp-finmap" + - 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 "coq-8.15" + --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 "coq-8.15" + --argstr job "mathcomp-classical" mathcomp-single: needs: - coq diff --git a/.github/workflows/nix-action-coq-8.16.yml b/.github/workflows/nix-action-coq-8.16.yml index a224c784c..8aadff070 100644 --- a/.github/workflows/nix-action-coq-8.16.yml +++ b/.github/workflows/nix-action-coq-8.16.yml @@ -35,9 +35,10 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16" --argstr job "coq" - coq-elpi: + graph-theory: needs: - coq + - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to test @@ -63,23 +64,34 @@ jobs: extraPullNames: coq, coq-community name: math-comp - id: stepCheck - name: Checking presence of CI target coq-elpi + name: Checking presence of CI target graph-theory run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.16\" --argstr job \"coq-elpi\" \\\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" + \ bundle \"coq-8.16\" --argstr job \"graph-theory\" \\\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 "coq-8.16" --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 "coq-8.16" + --argstr job "mathcomp-algebra" + - 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 "coq-8.16" + --argstr job "mathcomp-fingroup" + - 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 "coq-8.16" + --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 "coq-8.16" - --argstr job "coq-elpi" + --argstr job "graph-theory" hierarchy-builder: needs: - coq - - coq-elpi runs-on: ubuntu-latest steps: - name: Determine which commit to test @@ -122,10 +134,9 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16" --argstr job "hierarchy-builder" - mathcomp-analysis: + mathcomp: needs: - coq - - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to test @@ -151,11 +162,11 @@ jobs: extraPullNames: coq, coq-community name: math-comp - id: stepCheck - name: Checking presence of CI target mathcomp-analysis + name: Checking presence of CI target mathcomp run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.16\" --argstr job \"mathcomp-analysis\" \\\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" + \ bundle \"coq-8.16\" --argstr job \"mathcomp\" \\\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 previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16" @@ -165,29 +176,32 @@ jobs: run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16" --argstr job "mathcomp-ssreflect" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' + name: 'Building/fetching previous CI target: mathcomp-fingroup' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16" - --argstr job "mathcomp-field" + --argstr job "mathcomp-fingroup" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-finmap' + name: 'Building/fetching previous CI target: mathcomp-algebra' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16" - --argstr job "mathcomp-finmap" + --argstr job "mathcomp-algebra" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-real-closed' + name: 'Building/fetching previous CI target: mathcomp-solvable' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16" - --argstr job "mathcomp-real-closed" + --argstr job "mathcomp-solvable" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: hierarchy-builder' + name: 'Building/fetching previous CI target: mathcomp-field' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16" - --argstr job "hierarchy-builder" + --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 "coq-8.16" + --argstr job "mathcomp-character" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16" - --argstr job "mathcomp-analysis" + --argstr job "mathcomp" mathcomp-single: needs: - coq - - coq-elpi - hierarchy-builder runs-on: ubuntu-latest steps: @@ -238,7 +252,6 @@ jobs: mathcomp-single-planB-src: needs: - coq - - coq-elpi - hierarchy-builder runs-on: ubuntu-latest steps: diff --git a/.github/workflows/nix-action-coq-mcHB-8.16.yml b/.github/workflows/nix-action-coq-mcHB-8.16.yml index bfeab5dd5..8ce64fc4e 100644 --- a/.github/workflows/nix-action-coq-mcHB-8.16.yml +++ b/.github/workflows/nix-action-coq-mcHB-8.16.yml @@ -1,4 +1,218 @@ jobs: + QuickChick: + needs: + - coq + - mathcomp-ssreflect + 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 QuickChick + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-mcHB-8.16\" --argstr job \"QuickChick\" \\\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 "coq-mcHB-8.16" + --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 "coq-mcHB-8.16" + --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq-ext-lib' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "coq-ext-lib" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: simple-io' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "simple-io" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "QuickChick" + Verdi: + needs: + - coq + - mathcomp-ssreflect + 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 Verdi + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-mcHB-8.16\" --argstr job \"Verdi\" \\\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 "coq-mcHB-8.16" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: Cheerios' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "Cheerios" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: InfSeqExt' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "InfSeqExt" + - 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 "coq-mcHB-8.16" + --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 "coq-mcHB-8.16" + --argstr job "Verdi" + addition-chains: + needs: + - coq + - mathcomp-ssreflect + - mathcomp-algebra + - mathcomp-fingroup + 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 addition-chains + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-mcHB-8.16\" --argstr job \"addition-chains\" \\\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 "coq-mcHB-8.16" + --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 "coq-mcHB-8.16" + --argstr job "mathcomp-ssreflect" + - 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 "coq-mcHB-8.16" + --argstr job "mathcomp-algebra" + - 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 "coq-mcHB-8.16" + --argstr job "mathcomp-fingroup" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: paramcoq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "paramcoq" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "addition-chains" + autosubst: + needs: + - coq + - mathcomp-ssreflect + 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 autosubst + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-mcHB-8.16\" --argstr job \"autosubst\" \\\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 "coq-mcHB-8.16" + --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 "coq-mcHB-8.16" + --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 "coq-mcHB-8.16" + --argstr job "autosubst" coq: needs: [] runs-on: ubuntu-latest @@ -35,9 +249,10 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" --argstr job "coq" - coq-elpi: + coq-bits: needs: - coq + - mathcomp-algebra runs-on: ubuntu-latest steps: - name: Determine which commit to test @@ -63,19 +278,115 @@ jobs: extraPullNames: coq, coq-community name: math-comp - id: stepCheck - name: Checking presence of CI target coq-elpi + name: Checking presence of CI target coq-bits run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-mcHB-8.16\" --argstr job \"coq-elpi\" \\\n --dry-run 2>&1\ + \ bundle \"coq-mcHB-8.16\" --argstr job \"coq-bits\" \\\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 "coq-mcHB-8.16" --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 "coq-mcHB-8.16" + --argstr job "mathcomp-algebra" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" - --argstr job "coq-elpi" + --argstr job "coq-bits" + coquelicot: + needs: + - coq + - mathcomp-ssreflect + 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 coquelicot + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-mcHB-8.16\" --argstr job \"coquelicot\" \\\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 "coq-mcHB-8.16" + --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 "coq-mcHB-8.16" + --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 "coq-mcHB-8.16" + --argstr job "coquelicot" + deriving: + needs: + - coq + - mathcomp-ssreflect + 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 deriving + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-mcHB-8.16\" --argstr job \"deriving\" \\\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 "coq-mcHB-8.16" + --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 "coq-mcHB-8.16" + --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 "coq-mcHB-8.16" + --argstr job "deriving" fourcolor: needs: - coq @@ -135,7 +446,6 @@ jobs: hierarchy-builder: needs: - coq - - coq-elpi runs-on: ubuntu-latest steps: - name: Determine which commit to test @@ -181,7 +491,6 @@ jobs: hierarchy-builder-shim: needs: - coq - - coq-elpi runs-on: ubuntu-latest steps: - name: Determine which commit to test @@ -224,6 +533,70 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" --argstr job "hierarchy-builder-shim" + interval: + needs: + - coq + - coquelicot + - mathcomp-ssreflect + - mathcomp-fingroup + 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 interval + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-mcHB-8.16\" --argstr job \"interval\" \\\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 "coq-mcHB-8.16" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: bignums' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "bignums" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coquelicot' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "coquelicot" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: flocq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "flocq" + - 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 "coq-mcHB-8.16" + --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 "coq-mcHB-8.16" + --argstr job "mathcomp-fingroup" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "interval" mathcomp: needs: - coq @@ -233,7 +606,6 @@ jobs: - mathcomp-solvable - mathcomp-field - mathcomp-character - - coq-elpi - hierarchy-builder runs-on: ubuntu-latest steps: @@ -310,7 +682,6 @@ jobs: - coq - mathcomp-ssreflect - mathcomp-fingroup - - coq-elpi - hierarchy-builder runs-on: ubuntu-latest steps: @@ -369,9 +740,9 @@ jobs: mathcomp-analysis: needs: - coq - - mathcomp-ssreflect - mathcomp-field - - mathcomp-finmap + - mathcomp-bigenough + - mathcomp-classical - hierarchy-builder runs-on: ubuntu-latest steps: @@ -407,18 +778,18 @@ jobs: name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" --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 "coq-mcHB-8.16" - --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 "coq-mcHB-8.16" --argstr job "mathcomp-field" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-finmap' + name: 'Building/fetching previous CI target: mathcomp-bigenough' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" - --argstr job "mathcomp-finmap" + --argstr job "mathcomp-bigenough" + - 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 "coq-mcHB-8.16" + --argstr job "mathcomp-classical" - 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 "coq-mcHB-8.16" @@ -427,6 +798,52 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" --argstr job "mathcomp-analysis" + mathcomp-bigenough: + needs: + - coq + - mathcomp-ssreflect + 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 \"coq-mcHB-8.16\" --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 "coq-mcHB-8.16" + --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 "coq-mcHB-8.16" + --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 "coq-mcHB-8.16" + --argstr job "mathcomp-bigenough" mathcomp-character: needs: - coq @@ -435,7 +852,6 @@ jobs: - mathcomp-algebra - mathcomp-solvable - mathcomp-field - - coq-elpi - hierarchy-builder runs-on: ubuntu-latest steps: @@ -503,6 +919,67 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" --argstr job "mathcomp-character" + mathcomp-classical: + needs: + - coq + - mathcomp-ssreflect + - mathcomp-algebra + - mathcomp-finmap + - hierarchy-builder + 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-classical + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-mcHB-8.16\" --argstr job \"mathcomp-classical\" \\\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 "coq-mcHB-8.16" + --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 "coq-mcHB-8.16" + --argstr job "mathcomp-ssreflect" + - 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 "coq-mcHB-8.16" + --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 "coq-mcHB-8.16" + --argstr job "mathcomp-finmap" + - 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 "coq-mcHB-8.16" + --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 "coq-mcHB-8.16" + --argstr job "mathcomp-classical" mathcomp-field: needs: - coq @@ -510,7 +987,6 @@ jobs: - mathcomp-fingroup - mathcomp-algebra - mathcomp-solvable - - coq-elpi - hierarchy-builder runs-on: ubuntu-latest steps: @@ -578,7 +1054,6 @@ jobs: needs: - coq - mathcomp-ssreflect - - coq-elpi - hierarchy-builder runs-on: ubuntu-latest steps: @@ -679,9 +1154,7 @@ jobs: mathcomp-single: needs: - coq - - coq-elpi - hierarchy-builder - - coq-elpi - hierarchy-builder runs-on: ubuntu-latest steps: @@ -740,9 +1213,7 @@ jobs: mathcomp-single-planB: needs: - coq - - coq-elpi - hierarchy-builder - - coq-elpi - hierarchy-builder-shim runs-on: ubuntu-latest steps: @@ -801,9 +1272,7 @@ jobs: mathcomp-single-planB-src: needs: - coq - - coq-elpi - hierarchy-builder - - coq-elpi - hierarchy-builder runs-on: ubuntu-latest steps: @@ -865,7 +1334,6 @@ jobs: - mathcomp-ssreflect - mathcomp-fingroup - mathcomp-algebra - - coq-elpi - hierarchy-builder runs-on: ubuntu-latest steps: @@ -928,7 +1396,6 @@ jobs: mathcomp-ssreflect: needs: - coq - - coq-elpi - hierarchy-builder runs-on: ubuntu-latest steps: @@ -1052,6 +1519,52 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" --argstr job "odd-order" + reglang: + needs: + - coq + - mathcomp-ssreflect + 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 reglang + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-mcHB-8.16\" --argstr job \"reglang\" \\\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 "coq-mcHB-8.16" + --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 "coq-mcHB-8.16" + --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 "coq-mcHB-8.16" + --argstr job "reglang" name: Nix CI for bundle coq-mcHB-8.16 'on': pull_request: diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index fddb4f818..2e80cf19b 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"a2aa6afce9ebfea39501cdf43a3a3bd08e557a26" +"4f0eb194b37b6e0db28be2eb4643bd6924abf7ab" diff --git a/coq-hierarchy-builder-shim.opam b/coq-hierarchy-builder-shim.opam index 935914113..6f44b2a7f 100644 --- a/coq-hierarchy-builder-shim.opam +++ b/coq-hierarchy-builder-shim.opam @@ -11,7 +11,7 @@ dev-repo: "git+https://github.com/math-comp/hierarchy-builder" build: [ make "-C" "shim" "build" ] install: [ make "-C" "shim" "install" ] conflicts: [ "coq-hierarchy-builder" ] -depends: [ "coq-elpi" { (>= "1.14" & < "1.16~") | = "dev" } ] +depends: [ "coq-elpi" { (>= "1.14" & < "1.17~") | = "dev" } ] synopsis: "Shim package for HB" description: """ This package provide the support constants one can use to compile files diff --git a/coq-hierarchy-builder.opam b/coq-hierarchy-builder.opam index d4ea65af1..03a6abfae 100644 --- a/coq-hierarchy-builder.opam +++ b/coq-hierarchy-builder.opam @@ -12,7 +12,7 @@ build: [ [ make "build"] [ make "test-suite" ] {with-test} ] install: [ make "install" ] -depends: [ "coq-elpi" { (>= "1.14" & < "1.16~") | = "dev" } ] +depends: [ "coq-elpi" { (>= "1.14" & < "1.17~") | = "dev" } ] conflicts: [ "coq-hierarchy-builder-shim" ] synopsis: "High level commands to declare and evolve a hierarchy based on packed classes" description: """