diff --git a/.github/workflows/nix-action-coq-master.yml b/.github/workflows/nix-action-coq-master.yml index fd6d86975..c2e854464 100644 --- a/.github/workflows/nix-action-coq-master.yml +++ b/.github/workflows/nix-action-coq-master.yml @@ -1,7 +1,6 @@ jobs: - QuickChick: - needs: - - mathcomp-ssreflect + coq: + needs: [] runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -9,7 +8,7 @@ jobs: \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ \ }}\" >> $GITHUB_ENV\nfi\n" - name: Git checkout - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.target_commit }} @@ -23,7 +22,7 @@ jobs: \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - name: Git checkout - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.tested_commit }} @@ -38,33 +37,18 @@ jobs: extraPullNames: coq, coq-community, math-comp name: coq-elpi - id: stepCheck - name: Checking presence of CI target QuickChick + name: Checking presence of CI target coq run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-master\" --argstr job \"QuickChick\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\ - built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" - --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-master" - --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-master" - --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-master" - --argstr job "simple-io" + \ bundle \"coq-master\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ + s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" - --argstr job "QuickChick" + --argstr job "coq" coq-elpi: - needs: [] + needs: + - coq runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -72,7 +56,7 @@ jobs: \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ \ }}\" >> $GITHUB_ENV\nfi\n" - name: Git checkout - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.target_commit }} @@ -86,7 +70,7 @@ jobs: \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - name: Git checkout - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.tested_commit }} @@ -114,64 +98,9 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" --argstr job "coq-elpi" - coquelicot: - needs: - - mathcomp-ssreflect - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ - \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ - \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ - \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ - \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v27 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq-elpi - uses: cachix/cachix-action@v15 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, math-comp - name: coq-elpi - - 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-master\" --argstr job \"coquelicot\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\ - built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" - --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-master" - --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-master" - --argstr job "coquelicot" hierarchy-builder: needs: + - coq - coq-elpi runs-on: ubuntu-latest steps: @@ -180,7 +109,7 @@ jobs: \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ \ }}\" >> $GITHUB_ENV\nfi\n" - name: Git checkout - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.target_commit }} @@ -194,7 +123,7 @@ jobs: \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - name: Git checkout - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.tested_commit }} @@ -226,82 +155,9 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" --argstr job "hierarchy-builder" - interval: - needs: - - coquelicot - - mathcomp-ssreflect - - mathcomp-fingroup - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ - \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ - \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ - \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ - \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v27 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq-elpi - uses: cachix/cachix-action@v15 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, math-comp - name: coq-elpi - - 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-master\" --argstr job \"interval\" \\\n --dry-run 2>&1 >\ - \ /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\"\ - \ | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" - --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-master" - --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-master" - --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-master" - --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-master" - --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-master" - --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-master" - --argstr job "interval" mathcomp: needs: + - coq - mathcomp-ssreflect - mathcomp-fingroup - mathcomp-algebra @@ -316,7 +172,7 @@ jobs: \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ \ }}\" >> $GITHUB_ENV\nfi\n" - name: Git checkout - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.target_commit }} @@ -330,7 +186,7 @@ jobs: \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - name: Git checkout - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.tested_commit }} @@ -388,6 +244,7 @@ jobs: --argstr job "mathcomp" mathcomp-algebra: needs: + - coq - mathcomp-ssreflect - mathcomp-fingroup - hierarchy-builder @@ -398,7 +255,7 @@ jobs: \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ \ }}\" >> $GITHUB_ENV\nfi\n" - name: Git checkout - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.target_commit }} @@ -412,7 +269,7 @@ jobs: \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - name: Git checkout - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.tested_commit }} @@ -454,9 +311,9 @@ jobs: --argstr job "mathcomp-algebra" mathcomp-analysis: needs: + - coq - mathcomp-classical - mathcomp-field - - mathcomp-bigenough - hierarchy-builder runs-on: ubuntu-latest steps: @@ -465,7 +322,7 @@ jobs: \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ \ }}\" >> $GITHUB_ENV\nfi\n" - name: Git checkout - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.target_commit }} @@ -479,7 +336,7 @@ jobs: \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - name: Git checkout - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.tested_commit }} @@ -511,10 +368,6 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-field' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" --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 "coq-master" - --argstr job "mathcomp-bigenough" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: hierarchy-builder' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" @@ -523,64 +376,9 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" --argstr job "mathcomp-analysis" - mathcomp-bigenough: - needs: - - mathcomp-ssreflect - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ - \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ - \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ - \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ - \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v27 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq-elpi - uses: cachix/cachix-action@v15 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, math-comp - name: coq-elpi - - 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-master\" --argstr job \"mathcomp-bigenough\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" - --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-master" - --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-master" - --argstr job "mathcomp-bigenough" mathcomp-character: needs: + - coq - mathcomp-ssreflect - mathcomp-fingroup - mathcomp-algebra @@ -594,7 +392,7 @@ jobs: \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ \ }}\" >> $GITHUB_ENV\nfi\n" - name: Git checkout - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.target_commit }} @@ -608,7 +406,7 @@ jobs: \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - name: Git checkout - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.tested_commit }} @@ -662,6 +460,7 @@ jobs: --argstr job "mathcomp-character" mathcomp-classical: needs: + - coq - mathcomp-algebra - mathcomp-finmap - hierarchy-builder @@ -672,7 +471,7 @@ jobs: \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ \ }}\" >> $GITHUB_ENV\nfi\n" - name: Git checkout - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.target_commit }} @@ -686,7 +485,7 @@ jobs: \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - name: Git checkout - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.tested_commit }} @@ -728,6 +527,7 @@ jobs: --argstr job "mathcomp-classical" mathcomp-field: needs: + - coq - mathcomp-ssreflect - mathcomp-fingroup - mathcomp-algebra @@ -740,7 +540,7 @@ jobs: \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ \ }}\" >> $GITHUB_ENV\nfi\n" - name: Git checkout - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.target_commit }} @@ -754,7 +554,7 @@ jobs: \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - name: Git checkout - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.tested_commit }} @@ -804,6 +604,7 @@ jobs: --argstr job "mathcomp-field" mathcomp-fingroup: needs: + - coq - mathcomp-ssreflect - hierarchy-builder runs-on: ubuntu-latest @@ -813,7 +614,7 @@ jobs: \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ \ }}\" >> $GITHUB_ENV\nfi\n" - name: Git checkout - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.target_commit }} @@ -827,7 +628,7 @@ jobs: \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - name: Git checkout - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.tested_commit }} @@ -865,6 +666,7 @@ jobs: --argstr job "mathcomp-fingroup" mathcomp-finmap: needs: + - coq - mathcomp-ssreflect runs-on: ubuntu-latest steps: @@ -873,7 +675,7 @@ jobs: \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ \ }}\" >> $GITHUB_ENV\nfi\n" - name: Git checkout - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.target_commit }} @@ -887,7 +689,7 @@ jobs: \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - name: Git checkout - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.tested_commit }} @@ -921,6 +723,7 @@ jobs: --argstr job "mathcomp-finmap" mathcomp-solvable: needs: + - coq - mathcomp-ssreflect - mathcomp-fingroup - mathcomp-algebra @@ -932,7 +735,7 @@ jobs: \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ \ }}\" >> $GITHUB_ENV\nfi\n" - name: Git checkout - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.target_commit }} @@ -946,7 +749,7 @@ jobs: \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - name: Git checkout - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.tested_commit }} @@ -992,6 +795,7 @@ jobs: --argstr job "mathcomp-solvable" mathcomp-ssreflect: needs: + - coq - hierarchy-builder runs-on: ubuntu-latest steps: @@ -1000,7 +804,7 @@ jobs: \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ \ }}\" >> $GITHUB_ENV\nfi\n" - name: Git checkout - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.target_commit }} @@ -1014,7 +818,7 @@ jobs: \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - name: Git checkout - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.tested_commit }} @@ -1048,6 +852,7 @@ jobs: --argstr job "mathcomp-ssreflect" odd-order: needs: + - coq - mathcomp-character - mathcomp-ssreflect - mathcomp-fingroup @@ -1062,7 +867,7 @@ jobs: \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ \ }}\" >> $GITHUB_ENV\nfi\n" - name: Git checkout - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.target_commit }} @@ -1076,7 +881,7 @@ jobs: \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - name: Git checkout - uses: actions/checkout@v3 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ env.tested_commit }} @@ -1132,74 +937,6 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" --argstr job "odd-order" - vcfloat: - needs: - - interval - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ - \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ - \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ - \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ - \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v27 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq-elpi - uses: cachix/cachix-action@v15 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, math-comp - name: coq-elpi - - id: stepCheck - name: Checking presence of CI target vcfloat - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-master\" --argstr job \"vcfloat\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ - s/.*/built/\") >> $GITHUB_OUTPUT\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: interval' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" - --argstr job "interval" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: compcert' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" - --argstr job "compcert" - - 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-master" - --argstr job "flocq" - - 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-master" - --argstr job "bignums" - - 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-master" - --argstr job "vcfloat" name: Nix CI for bundle coq-master 'on': pull_request: diff --git a/.nix/config.nix b/.nix/config.nix index 1b6ecd1ed..402762323 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -34,6 +34,8 @@ "coq-master".coqPackages = { + coq.override.version = "master"; + hierarchy-builder.override.version = "master"; hierarchy-builder-shim.job = false; diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index 6d4f52f1c..5dfe65178 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"bf47d818bbbd0f6a2d48cc4e0d876e0109077c75" +"208d8cd3c82113f719ae67d7652203da3fbbcbe4" diff --git a/.nix/coq-overlays/coq-elpi/default.nix b/.nix/coq-overlays/coq-elpi/default.nix index 3cc12b156..a9c862175 100644 --- a/.nix/coq-overlays/coq-elpi/default.nix +++ b/.nix/coq-overlays/coq-elpi/default.nix @@ -11,7 +11,7 @@ with builtins; with lib; let { case = "8.17"; out = { version = "1.17.0"; };} { case = "8.18"; out = { version = "v1.18.1"; };} { case = "8.19"; out = { version = "v1.18.2"; };} - ] {} ); + ] { version = "v1.19.4"; } ); in mkCoqDerivation { pname = "elpi"; repo = "coq-elpi";