diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 043c304..a7ac240 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -19,9 +19,7 @@ jobs: strategy: matrix: image: - - 'mathcomp/mathcomp:2.1.0-coq-8.16' - 'mathcomp/mathcomp:2.1.0-coq-8.18' - - 'mathcomp/mathcomp:2.2.0-coq-8.16' - 'mathcomp/mathcomp:2.2.0-coq-8.19' - 'mathcomp/mathcomp:2.3.0-coq-8.20' - 'mathcomp/mathcomp-dev:rocq-prover-dev' diff --git a/.github/workflows/nix-action-8.18+2.1.yml b/.github/workflows/nix-action-8.18+2.1.yml deleted file mode 100644 index 64b6bcf..0000000 --- a/.github/workflows/nix-action-8.18+2.1.yml +++ /dev/null @@ -1,289 +0,0 @@ -jobs: - coq: - needs: [] - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v4 - 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@v4 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v30 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq-community - uses: cachix/cachix-action@v15 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, math-comp - name: coq-community - - id: stepGetDerivation - name: Getting derivation for current job (coq) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.18+2.1\" --argstr job \"coq\" \\\n --dry-run 2> err > out || (touch - fail; true)\n" - - name: Error reporting - run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" - - name: Failure check - run: if [ -e fail ]; then exit 1; else exit 0; fi; - - id: stepCheck - name: Checking presence of CI target for current job - run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18+2.1" - --argstr job "coq" - fourcolor: - needs: - - coq - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v4 - 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@v4 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v30 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq-community - uses: cachix/cachix-action@v15 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, math-comp - name: coq-community - - id: stepGetDerivation - name: Getting derivation for current job (fourcolor) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.18+2.1\" --argstr job \"fourcolor\" \\\n --dry-run 2> err > out || (touch - fail; true)\n" - - name: Error reporting - run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" - - name: Failure check - run: if [ -e fail ]; then exit 1; else exit 0; fi; - - id: stepCheck - name: Checking presence of CI target for current job - run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18+2.1" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18+2.1" - --argstr job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18+2.1" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-fingroup' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18+2.1" - --argstr job "mathcomp-fingroup" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: stdlib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18+2.1" - --argstr job "stdlib" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18+2.1" - --argstr job "fourcolor" - graph-theory: - needs: - - coq - - mathcomp-finmap - - fourcolor - 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@v4 - 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@v4 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v30 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq-community - uses: cachix/cachix-action@v15 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, math-comp - name: coq-community - - id: stepGetDerivation - name: Getting derivation for current job (graph-theory) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.18+2.1\" --argstr job \"graph-theory\" \\\n --dry-run 2> err > out || - (touch fail; true)\n" - - name: Error reporting - run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" - - name: Failure check - run: if [ -e fail ]; then exit 1; else exit 0; fi; - - id: stepCheck - name: Checking presence of CI target for current job - run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18+2.1" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18+2.1" - --argstr job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-finmap' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18+2.1" - --argstr job "mathcomp-finmap" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-fingroup' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18+2.1" - --argstr job "mathcomp-fingroup" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: fourcolor' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18+2.1" - --argstr job "fourcolor" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: hierarchy-builder' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18+2.1" - --argstr job "hierarchy-builder" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18+2.1" - --argstr job "graph-theory" - mathcomp-finmap: - needs: - - coq - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v4 - 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@v4 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v30 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq-community - uses: cachix/cachix-action@v15 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, math-comp - name: coq-community - - id: stepGetDerivation - name: Getting derivation for current job (mathcomp-finmap) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.18+2.1\" --argstr job \"mathcomp-finmap\" \\\n --dry-run 2> err > out - || (touch fail; true)\n" - - name: Error reporting - run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" - - name: Failure check - run: if [ -e fail ]; then exit 1; else exit 0; fi; - - id: stepCheck - name: Checking presence of CI target for current job - run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18+2.1" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18+2.1" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: stdlib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18+2.1" - --argstr job "stdlib" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18+2.1" - --argstr job "mathcomp-finmap" -name: Nix CI for bundle 8.18+2.1 -on: - pull_request: - paths: - - .github/workflows/nix-action-8.18+2.1.yml - pull_request_target: - paths-ignore: - - .github/workflows/nix-action-8.18+2.1.yml - types: - - opened - - synchronize - - reopened - push: - branches: - - master diff --git a/.github/workflows/nix-action-8.17+2.1.yml b/.github/workflows/nix-action-8.18.yml similarity index 68% rename from .github/workflows/nix-action-8.17+2.1.yml rename to .github/workflows/nix-action-8.18.yml index 6287a3a..f0998c9 100644 --- a/.github/workflows/nix-action-8.17+2.1.yml +++ b/.github/workflows/nix-action-8.18.yml @@ -39,8 +39,8 @@ jobs: - id: stepGetDerivation name: Getting derivation for current job (coq) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.17+2.1\" --argstr job \"coq\" \\\n --dry-run 2> err > out || (touch - fail; true)\n" + \"8.18\" --argstr job \"coq\" \\\n --dry-run 2> err > out || (touch fail; + true)\n" - name: Error reporting run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" - name: Failure check @@ -50,8 +50,8 @@ jobs: run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17+2.1" - --argstr job "coq" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "coq" fourcolor: needs: - coq @@ -93,7 +93,7 @@ jobs: - id: stepGetDerivation name: Getting derivation for current job (fourcolor) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.17+2.1\" --argstr job \"fourcolor\" \\\n --dry-run 2> err > out || (touch + \"8.18\" --argstr job \"fourcolor\" \\\n --dry-run 2> err > out || (touch fail; true)\n" - name: Error reporting run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" @@ -104,32 +104,31 @@ jobs: run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17+2.1" - --argstr job "coq" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "coq" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17+2.1" - --argstr job "mathcomp-algebra" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "mathcomp-algebra" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17+2.1" - --argstr job "mathcomp-ssreflect" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "mathcomp-ssreflect" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-fingroup' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17+2.1" - --argstr job "mathcomp-fingroup" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "mathcomp-fingroup" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: stdlib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17+2.1" - --argstr job "stdlib" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "stdlib" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17+2.1" - --argstr job "fourcolor" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "fourcolor" graph-theory: needs: - coq - - mathcomp-finmap - fourcolor runs-on: ubuntu-latest steps: @@ -169,8 +168,8 @@ jobs: - id: stepGetDerivation name: Getting derivation for current job (graph-theory) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.17+2.1\" --argstr job \"graph-theory\" \\\n --dry-run 2> err > out || - (touch fail; true)\n" + \"8.18\" --argstr job \"graph-theory\" \\\n --dry-run 2> err > out || (touch + fail; true)\n" - name: Error reporting run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" - name: Failure check @@ -180,106 +179,44 @@ jobs: run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17+2.1" - --argstr job "coq" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "coq" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17+2.1" - --argstr job "mathcomp-algebra" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "mathcomp-algebra" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-finmap' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17+2.1" - --argstr job "mathcomp-finmap" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "mathcomp-finmap" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-fingroup' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17+2.1" - --argstr job "mathcomp-fingroup" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "mathcomp-fingroup" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-algebra-tactics' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "mathcomp-algebra-tactics" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: fourcolor' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17+2.1" - --argstr job "fourcolor" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "fourcolor" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: hierarchy-builder' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17+2.1" - --argstr job "hierarchy-builder" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17+2.1" - --argstr job "graph-theory" - mathcomp-finmap: - needs: - - coq - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v4 - 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@v4 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v30 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq-community - uses: cachix/cachix-action@v15 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, math-comp - name: coq-community - - id: stepGetDerivation - name: Getting derivation for current job (mathcomp-finmap) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.17+2.1\" --argstr job \"mathcomp-finmap\" \\\n --dry-run 2> err > out - || (touch fail; true)\n" - - name: Error reporting - run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" - - name: Failure check - run: if [ -e fail ]; then exit 1; else exit 0; fi; - - id: stepCheck - name: Checking presence of CI target for current job - run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17+2.1" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17+2.1" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: stdlib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17+2.1" - --argstr job "stdlib" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "hierarchy-builder" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17+2.1" - --argstr job "mathcomp-finmap" -name: Nix CI for bundle 8.17+2.1 + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr + job "graph-theory" +name: Nix CI for bundle 8.18 on: pull_request: paths: - - .github/workflows/nix-action-8.17+2.1.yml + - .github/workflows/nix-action-8.18.yml pull_request_target: paths-ignore: - - .github/workflows/nix-action-8.17+2.1.yml + - .github/workflows/nix-action-8.18.yml types: - opened - synchronize diff --git a/.github/workflows/nix-action-8.19+2.2.yml b/.github/workflows/nix-action-8.19+2.2.yml deleted file mode 100644 index c5127f0..0000000 --- a/.github/workflows/nix-action-8.19+2.2.yml +++ /dev/null @@ -1,289 +0,0 @@ -jobs: - coq: - needs: [] - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v4 - 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@v4 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v30 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq-community - uses: cachix/cachix-action@v15 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, math-comp - name: coq-community - - id: stepGetDerivation - name: Getting derivation for current job (coq) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.19+2.2\" --argstr job \"coq\" \\\n --dry-run 2> err > out || (touch - fail; true)\n" - - name: Error reporting - run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" - - name: Failure check - run: if [ -e fail ]; then exit 1; else exit 0; fi; - - id: stepCheck - name: Checking presence of CI target for current job - run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19+2.2" - --argstr job "coq" - fourcolor: - needs: - - coq - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v4 - 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@v4 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v30 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq-community - uses: cachix/cachix-action@v15 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, math-comp - name: coq-community - - id: stepGetDerivation - name: Getting derivation for current job (fourcolor) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.19+2.2\" --argstr job \"fourcolor\" \\\n --dry-run 2> err > out || (touch - fail; true)\n" - - name: Error reporting - run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" - - name: Failure check - run: if [ -e fail ]; then exit 1; else exit 0; fi; - - id: stepCheck - name: Checking presence of CI target for current job - run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19+2.2" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19+2.2" - --argstr job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19+2.2" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-fingroup' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19+2.2" - --argstr job "mathcomp-fingroup" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: stdlib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19+2.2" - --argstr job "stdlib" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19+2.2" - --argstr job "fourcolor" - graph-theory: - needs: - - coq - - mathcomp-finmap - - fourcolor - 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@v4 - 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@v4 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v30 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq-community - uses: cachix/cachix-action@v15 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, math-comp - name: coq-community - - id: stepGetDerivation - name: Getting derivation for current job (graph-theory) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.19+2.2\" --argstr job \"graph-theory\" \\\n --dry-run 2> err > out || - (touch fail; true)\n" - - name: Error reporting - run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" - - name: Failure check - run: if [ -e fail ]; then exit 1; else exit 0; fi; - - id: stepCheck - name: Checking presence of CI target for current job - run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19+2.2" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19+2.2" - --argstr job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-finmap' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19+2.2" - --argstr job "mathcomp-finmap" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-fingroup' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19+2.2" - --argstr job "mathcomp-fingroup" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: fourcolor' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19+2.2" - --argstr job "fourcolor" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: hierarchy-builder' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19+2.2" - --argstr job "hierarchy-builder" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19+2.2" - --argstr job "graph-theory" - mathcomp-finmap: - needs: - - coq - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v4 - 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@v4 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v30 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq-community - uses: cachix/cachix-action@v15 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, math-comp - name: coq-community - - id: stepGetDerivation - name: Getting derivation for current job (mathcomp-finmap) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.19+2.2\" --argstr job \"mathcomp-finmap\" \\\n --dry-run 2> err > out - || (touch fail; true)\n" - - name: Error reporting - run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" - - name: Failure check - run: if [ -e fail ]; then exit 1; else exit 0; fi; - - id: stepCheck - name: Checking presence of CI target for current job - run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19+2.2" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19+2.2" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: stdlib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19+2.2" - --argstr job "stdlib" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19+2.2" - --argstr job "mathcomp-finmap" -name: Nix CI for bundle 8.19+2.2 -on: - pull_request: - paths: - - .github/workflows/nix-action-8.19+2.2.yml - pull_request_target: - paths-ignore: - - .github/workflows/nix-action-8.19+2.2.yml - types: - - opened - - synchronize - - reopened - push: - branches: - - master diff --git a/.github/workflows/nix-action-9.0+2.3.yml b/.github/workflows/nix-action-8.19.yml similarity index 69% rename from .github/workflows/nix-action-9.0+2.3.yml rename to .github/workflows/nix-action-8.19.yml index c1a4782..db2dac2 100644 --- a/.github/workflows/nix-action-9.0+2.3.yml +++ b/.github/workflows/nix-action-8.19.yml @@ -39,7 +39,7 @@ jobs: - id: stepGetDerivation name: Getting derivation for current job (coq) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"9.0+2.3\" --argstr job \"coq\" \\\n --dry-run 2> err > out || (touch fail; + \"8.19\" --argstr job \"coq\" \\\n --dry-run 2> err > out || (touch fail; true)\n" - name: Error reporting run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" @@ -50,8 +50,8 @@ jobs: run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0+2.3" - --argstr job "coq" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "coq" fourcolor: needs: - coq @@ -93,7 +93,7 @@ jobs: - id: stepGetDerivation name: Getting derivation for current job (fourcolor) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"9.0+2.3\" --argstr job \"fourcolor\" \\\n --dry-run 2> err > out || (touch + \"8.19\" --argstr job \"fourcolor\" \\\n --dry-run 2> err > out || (touch fail; true)\n" - name: Error reporting run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" @@ -104,32 +104,31 @@ jobs: run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT - 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 "9.0+2.3" - --argstr job "coq" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "coq" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0+2.3" - --argstr job "mathcomp-algebra" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp-algebra" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0+2.3" - --argstr job "mathcomp-ssreflect" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp-ssreflect" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-fingroup' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0+2.3" - --argstr job "mathcomp-fingroup" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp-fingroup" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: stdlib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0+2.3" - --argstr job "stdlib" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "stdlib" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0+2.3" - --argstr job "fourcolor" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "fourcolor" graph-theory: needs: - coq - - mathcomp-finmap - fourcolor runs-on: ubuntu-latest steps: @@ -169,8 +168,8 @@ jobs: - id: stepGetDerivation name: Getting derivation for current job (graph-theory) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"9.0+2.3\" --argstr job \"graph-theory\" \\\n --dry-run 2> err > out || - (touch fail; true)\n" + \"8.19\" --argstr job \"graph-theory\" \\\n --dry-run 2> err > out || (touch + fail; true)\n" - name: Error reporting run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" - name: Failure check @@ -180,106 +179,44 @@ jobs: run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT - 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 "9.0+2.3" - --argstr job "coq" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "coq" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0+2.3" - --argstr job "mathcomp-algebra" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp-algebra" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-finmap' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0+2.3" - --argstr job "mathcomp-finmap" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp-finmap" - 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 "9.0+2.3" - --argstr job "mathcomp-fingroup" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp-fingroup" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-algebra-tactics' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp-algebra-tactics" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: fourcolor' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0+2.3" - --argstr job "fourcolor" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "fourcolor" - 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 "9.0+2.3" - --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 "9.0+2.3" - --argstr job "graph-theory" - mathcomp-finmap: - needs: - - coq - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v4 - 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@v4 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v30 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq-community - uses: cachix/cachix-action@v15 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, math-comp - name: coq-community - - id: stepGetDerivation - name: Getting derivation for current job (mathcomp-finmap) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"9.0+2.3\" --argstr job \"mathcomp-finmap\" \\\n --dry-run 2> err > out - || (touch fail; true)\n" - - name: Error reporting - run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" - - name: Failure check - run: if [ -e fail ]; then exit 1; else exit 0; fi; - - id: stepCheck - name: Checking presence of CI target for current job - run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT - - 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 "9.0+2.3" - --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 "9.0+2.3" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: stdlib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0+2.3" - --argstr job "stdlib" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "hierarchy-builder" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0+2.3" - --argstr job "mathcomp-finmap" -name: Nix CI for bundle 9.0+2.3 + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "graph-theory" +name: Nix CI for bundle 8.19 on: pull_request: paths: - - .github/workflows/nix-action-9.0+2.3.yml + - .github/workflows/nix-action-8.19.yml pull_request_target: paths-ignore: - - .github/workflows/nix-action-9.0+2.3.yml + - .github/workflows/nix-action-8.19.yml types: - opened - synchronize diff --git a/.github/workflows/nix-action-8.20+2.3.yml b/.github/workflows/nix-action-8.20+2.3.yml deleted file mode 100644 index 0abd78a..0000000 --- a/.github/workflows/nix-action-8.20+2.3.yml +++ /dev/null @@ -1,289 +0,0 @@ -jobs: - coq: - needs: [] - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v4 - 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@v4 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v30 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq-community - uses: cachix/cachix-action@v15 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, math-comp - name: coq-community - - id: stepGetDerivation - name: Getting derivation for current job (coq) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.20+2.3\" --argstr job \"coq\" \\\n --dry-run 2> err > out || (touch - fail; true)\n" - - name: Error reporting - run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" - - name: Failure check - run: if [ -e fail ]; then exit 1; else exit 0; fi; - - id: stepCheck - name: Checking presence of CI target for current job - run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20+2.3" - --argstr job "coq" - fourcolor: - needs: - - coq - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v4 - 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@v4 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v30 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq-community - uses: cachix/cachix-action@v15 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, math-comp - name: coq-community - - id: stepGetDerivation - name: Getting derivation for current job (fourcolor) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.20+2.3\" --argstr job \"fourcolor\" \\\n --dry-run 2> err > out || (touch - fail; true)\n" - - name: Error reporting - run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" - - name: Failure check - run: if [ -e fail ]; then exit 1; else exit 0; fi; - - id: stepCheck - name: Checking presence of CI target for current job - run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20+2.3" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20+2.3" - --argstr job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20+2.3" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-fingroup' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20+2.3" - --argstr job "mathcomp-fingroup" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: stdlib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20+2.3" - --argstr job "stdlib" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20+2.3" - --argstr job "fourcolor" - graph-theory: - needs: - - coq - - mathcomp-finmap - - fourcolor - 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@v4 - 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@v4 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v30 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq-community - uses: cachix/cachix-action@v15 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, math-comp - name: coq-community - - id: stepGetDerivation - name: Getting derivation for current job (graph-theory) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.20+2.3\" --argstr job \"graph-theory\" \\\n --dry-run 2> err > out || - (touch fail; true)\n" - - name: Error reporting - run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" - - name: Failure check - run: if [ -e fail ]; then exit 1; else exit 0; fi; - - id: stepCheck - name: Checking presence of CI target for current job - run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20+2.3" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20+2.3" - --argstr job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-finmap' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20+2.3" - --argstr job "mathcomp-finmap" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-fingroup' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20+2.3" - --argstr job "mathcomp-fingroup" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: fourcolor' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20+2.3" - --argstr job "fourcolor" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: hierarchy-builder' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20+2.3" - --argstr job "hierarchy-builder" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20+2.3" - --argstr job "graph-theory" - mathcomp-finmap: - needs: - - coq - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v4 - 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@v4 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v30 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq-community - uses: cachix/cachix-action@v15 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, math-comp - name: coq-community - - id: stepGetDerivation - name: Getting derivation for current job (mathcomp-finmap) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.20+2.3\" --argstr job \"mathcomp-finmap\" \\\n --dry-run 2> err > out - || (touch fail; true)\n" - - name: Error reporting - run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" - - name: Failure check - run: if [ -e fail ]; then exit 1; else exit 0; fi; - - id: stepCheck - name: Checking presence of CI target for current job - run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20+2.3" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20+2.3" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: stdlib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20+2.3" - --argstr job "stdlib" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20+2.3" - --argstr job "mathcomp-finmap" -name: Nix CI for bundle 8.20+2.3 -on: - pull_request: - paths: - - .github/workflows/nix-action-8.20+2.3.yml - pull_request_target: - paths-ignore: - - .github/workflows/nix-action-8.20+2.3.yml - types: - - opened - - synchronize - - reopened - push: - branches: - - master diff --git a/.github/workflows/nix-action-8.20.yml b/.github/workflows/nix-action-8.20.yml new file mode 100644 index 0000000..d3949a4 --- /dev/null +++ b/.github/workflows/nix-action-8.20.yml @@ -0,0 +1,143 @@ +jobs: + coq: + needs: [] + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ + github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha + }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v4 + 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@v4 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v30 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-community + uses: cachix/cachix-action@v15 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, math-comp + name: coq-community + - id: stepGetDerivation + name: Getting derivation for current job (coq) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"8.20\" --argstr job \"coq\" \\\n --dry-run 2> err > out || (touch fail; + true)\n" + - name: Error reporting + run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" + - name: Failure check + run: if [ -e fail ]; then exit 1; else exit 0; fi; + - id: stepCheck + name: Checking presence of CI target for current job + run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr + job "coq" + fourcolor: + needs: + - coq + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ + github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha + }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v4 + 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@v4 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v30 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-community + uses: cachix/cachix-action@v15 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, math-comp + name: coq-community + - id: stepGetDerivation + name: Getting derivation for current job (fourcolor) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"8.20\" --argstr job \"fourcolor\" \\\n --dry-run 2> err > out || (touch + fail; true)\n" + - name: Error reporting + run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" + - name: Failure check + run: if [ -e fail ]; then exit 1; else exit 0; fi; + - id: stepCheck + name: Checking presence of CI target for current job + run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr + job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-algebra' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr + job "mathcomp-algebra" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr + job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-fingroup' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr + job "mathcomp-fingroup" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: stdlib' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr + job "stdlib" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr + job "fourcolor" +name: Nix CI for bundle 8.20 +on: + pull_request: + paths: + - .github/workflows/nix-action-8.20.yml + pull_request_target: + paths-ignore: + - .github/workflows/nix-action-8.20.yml + types: + - opened + - synchronize + - reopened + push: + branches: + - master diff --git a/.github/workflows/nix-action-9.0.yml b/.github/workflows/nix-action-9.0.yml new file mode 100644 index 0000000..1b71691 --- /dev/null +++ b/.github/workflows/nix-action-9.0.yml @@ -0,0 +1,143 @@ +jobs: + coq: + needs: [] + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ + github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha + }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v4 + 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@v4 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v30 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-community + uses: cachix/cachix-action@v15 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, math-comp + name: coq-community + - id: stepGetDerivation + name: Getting derivation for current job (coq) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"9.0\" --argstr job \"coq\" \\\n --dry-run 2> err > out || (touch fail; + true)\n" + - name: Error reporting + run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" + - name: Failure check + run: if [ -e fail ]; then exit 1; else exit 0; fi; + - id: stepCheck + name: Checking presence of CI target for current job + run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" --argstr + job "coq" + fourcolor: + needs: + - coq + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ + github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha + }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v4 + 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@v4 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v30 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-community + uses: cachix/cachix-action@v15 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, math-comp + name: coq-community + - id: stepGetDerivation + name: Getting derivation for current job (fourcolor) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"9.0\" --argstr job \"fourcolor\" \\\n --dry-run 2> err > out || (touch + fail; true)\n" + - name: Error reporting + run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" + - name: Failure check + run: if [ -e fail ]; then exit 1; else exit 0; fi; + - id: stepCheck + name: Checking presence of CI target for current job + run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT + - 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 "9.0" --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 "9.0" --argstr + job "mathcomp-algebra" + - 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 "9.0" --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 "9.0" --argstr + job "mathcomp-fingroup" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: stdlib' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" --argstr + job "stdlib" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" --argstr + job "fourcolor" +name: Nix CI for bundle 9.0 +on: + pull_request: + paths: + - .github/workflows/nix-action-9.0.yml + pull_request_target: + paths-ignore: + - .github/workflows/nix-action-9.0.yml + types: + - opened + - synchronize + - reopened + push: + branches: + - master diff --git a/.github/workflows/nix-action-8.16+2.1.yml b/.github/workflows/nix-action-master.yml similarity index 71% rename from .github/workflows/nix-action-8.16+2.1.yml rename to .github/workflows/nix-action-master.yml index 1e2dafd..6bf92ad 100644 --- a/.github/workflows/nix-action-8.16+2.1.yml +++ b/.github/workflows/nix-action-master.yml @@ -39,8 +39,8 @@ jobs: - id: stepGetDerivation name: Getting derivation for current job (coq) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.16+2.1\" --argstr job \"coq\" \\\n --dry-run 2> err > out || (touch - fail; true)\n" + \"master\" --argstr job \"coq\" \\\n --dry-run 2> err > out || (touch fail; + true)\n" - name: Error reporting run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" - name: Failure check @@ -50,8 +50,66 @@ jobs: run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16+2.1" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "coq" + coq-elpi: + needs: + - coq + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ + github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha + }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@v4 + 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@v4 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v30 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup coq-community + uses: cachix/cachix-action@v15 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, math-comp + name: coq-community + - id: stepGetDerivation + name: Getting derivation for current job (coq-elpi) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"master\" --argstr job \"coq-elpi\" \\\n --dry-run 2> err > out || (touch + fail; true)\n" + - name: Error reporting + run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" + - name: Failure check + run: if [ -e fail ]; then exit 1; else exit 0; fi; + - id: stepCheck + name: Checking presence of CI target for current job + run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT + - 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 "master" --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "coq-elpi" fourcolor: needs: - coq @@ -93,7 +151,7 @@ jobs: - id: stepGetDerivation name: Getting derivation for current job (fourcolor) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.16+2.1\" --argstr job \"fourcolor\" \\\n --dry-run 2> err > out || (touch + \"master\" --argstr job \"fourcolor\" \\\n --dry-run 2> err > out || (touch fail; true)\n" - name: Error reporting run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" @@ -104,33 +162,32 @@ jobs: run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16+2.1" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" --argstr job "coq" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16+2.1" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" --argstr job "mathcomp-algebra" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16+2.1" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "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 "8.16+2.1" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" --argstr job "mathcomp-fingroup" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: stdlib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16+2.1" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" --argstr job "stdlib" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16+2.1" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" --argstr job "fourcolor" - graph-theory: + hierarchy-builder: needs: - coq - - mathcomp-finmap - - fourcolor + - coq-elpi runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -167,10 +224,10 @@ jobs: extraPullNames: coq, math-comp name: coq-community - id: stepGetDerivation - name: Getting derivation for current job (graph-theory) + name: Getting derivation for current job (hierarchy-builder) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.16+2.1\" --argstr job \"graph-theory\" \\\n --dry-run 2> err > out || - (touch fail; true)\n" + \"master\" --argstr job \"hierarchy-builder\" \\\n --dry-run 2> err > out + || (touch fail; true)\n" - name: Error reporting run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" - name: Failure check @@ -180,35 +237,24 @@ jobs: run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16+2.1" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" --argstr job "coq" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16+2.1" - --argstr job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-finmap' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16+2.1" - --argstr job "mathcomp-finmap" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-fingroup' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16+2.1" - --argstr job "mathcomp-fingroup" + name: 'Building/fetching previous CI target: coq-elpi' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "coq-elpi" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: fourcolor' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16+2.1" - --argstr job "fourcolor" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: hierarchy-builder' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16+2.1" - --argstr job "hierarchy-builder" + name: 'Building/fetching previous CI target: stdlib' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "stdlib" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16+2.1" - --argstr job "graph-theory" - mathcomp-finmap: + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "hierarchy-builder" + mathcomp: needs: - coq + - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -245,10 +291,10 @@ jobs: extraPullNames: coq, math-comp name: coq-community - id: stepGetDerivation - name: Getting derivation for current job (mathcomp-finmap) + name: Getting derivation for current job (mathcomp) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.16+2.1\" --argstr job \"mathcomp-finmap\" \\\n --dry-run 2> err > out - || (touch fail; true)\n" + \"master\" --argstr job \"mathcomp\" \\\n --dry-run 2> err > out || (touch + fail; true)\n" - name: Error reporting run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" - name: Failure check @@ -258,28 +304,56 @@ jobs: run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16+2.1" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: stdlib' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "stdlib" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16+2.1" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "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 "master" + --argstr job "mathcomp-fingroup" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-algebra' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "mathcomp-algebra" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-solvable' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "mathcomp-solvable" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-field' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --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 "master" + --argstr job "mathcomp-character" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: hierarchy-builder' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "hierarchy-builder" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: stdlib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16+2.1" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" --argstr job "stdlib" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16+2.1" - --argstr job "mathcomp-finmap" -name: Nix CI for bundle 8.16+2.1 + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "mathcomp" +name: Nix CI for bundle master on: pull_request: paths: - - .github/workflows/nix-action-8.16+2.1.yml + - .github/workflows/nix-action-master.yml pull_request_target: paths-ignore: - - .github/workflows/nix-action-8.16+2.1.yml + - .github/workflows/nix-action-master.yml types: - opened - synchronize diff --git a/.nix/config.nix b/.nix/config.nix index 869b20a..d1c8226 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -30,37 +30,37 @@ ## select an entry to build in the following `bundles` set ## defaults to "default" - default-bundle = "8.20+2.3"; + default-bundle = "8.20"; ## write one `bundles.name` attribute set per ## alternative configuration, the can be used to ## compute several ci jobs as well - bundles = let - mc21 = { - mathcomp.override.version = "2.1.0"; - mathcomp.job = false; - mathcomp-finmap.override.version = "2.0.0"; - graph-theory.override.version = "v0.9.3"; + bundles = { + "8.18".coqPackages = { + coq.override.version = "8.18"; }; - mc22 = { - mathcomp.override.version = "2.2.0"; - mathcomp.job = false; - mathcomp-finmap.override.version = "2.1.0"; - graph-theory.override.version = "v0.9.4"; + "8.19".coqPackages = { + coq.override.version = "8.19"; }; - mc23 = { - mathcomp.override.version = "2.3.0"; - mathcomp.job = false; - mathcomp-finmap.override.version = "2.1.0"; - graph-theory.override.version = "v0.9.5"; + "8.20".coqPackages = { + coq.override.version = "8.20"; }; - in { - "8.16+2.1".coqPackages = { coq.override.version = "8.16"; } // mc21; - "8.17+2.1".coqPackages = { coq.override.version = "8.17"; } // mc21; - "8.18+2.1".coqPackages = { coq.override.version = "8.18"; } // mc21; - "8.19+2.2".coqPackages = { coq.override.version = "8.19"; } // mc22; - "8.20+2.3".coqPackages = { coq.override.version = "8.20"; } // mc23; - "9.0+2.3".coqPackages = { coq.override.version = "9.0"; } // mc23; + "9.0".coqPackages = { + coq.override.version = "9.0"; + }; + "master" = { rocqPackages = { + rocq-core.override.version = "master"; + rocq-elpi.override.version = "master"; + rocq-elpi.override.elpi-version = "2.0.7"; + stdlib.override.version = "master"; + }; coqPackages = { + coq.override.version = "master"; + coq-elpi.override.version = "master"; + coq-elpi.override.elpi-version = "2.0.7"; + hierarchy-builder.override.version = "master"; + mathcomp.override.version = "master"; + stdlib.override.version = "master"; + }; }; ## you may mark a package as a CI job as follows # coqPackages..ci.job = "test"; diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index 172eec9..b53317b 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"249b84ba5526b5b8c49f236923d595c8505717f2" +"23abc2d7903983f4fd414288677d6b421d412cd6" diff --git a/.nix/coq-overlays/mathcomp/default.nix b/.nix/coq-overlays/mathcomp/default.nix deleted file mode 100644 index dbaf587..0000000 --- a/.nix/coq-overlays/mathcomp/default.nix +++ /dev/null @@ -1,122 +0,0 @@ -############################################################################ -# This file mainly provides the `mathcomp` derivation, which is # -# essentially a meta-package containing all core mathcomp libraries # -# (ssreflect fingroup algebra solvable field character). They can be # -# accessed individually through the passthrough attributes of mathcomp # -# bearing the same names (mathcomp.ssreflect, etc). # -############################################################################ -# Compiling a custom version of mathcomp using `mathcomp.override`. # -# This is the replacement for the former `mathcomp_ config` function. # -# See the documentation at doc/languages-frameworks/coq.section.md. # -############################################################################ - -{ lib, ncurses, graphviz, lua, fetchzip, - coq-elpi, hierarchy-builder, - mkCoqDerivation, recurseIntoAttrs, withDoc ? false, single ? false, - coqPackages, coq, version ? null }@args: -with builtins // lib; -let - repo = "math-comp"; - owner = "math-comp"; - withDoc = single && (args.withDoc or false); - defaultVersion = with versions; switch coq.coq-version [ - { case = isGe "8.11"; out = "1.14.0"; } - { case = range "8.11" "8.15"; out = "1.13.0"; } - { case = range "8.10" "8.13"; out = "1.12.0"; } - { case = range "8.7" "8.12"; out = "1.11.0"; } - { case = range "8.7" "8.11"; out = "1.10.0"; } - { case = range "8.7" "8.11"; out = "1.9.0"; } - { case = range "8.7" "8.9"; out = "1.8.0"; } - { case = range "8.6" "8.9"; out = "1.7.0"; } - { case = range "8.5" "8.7"; out = "1.6.4"; } - ] null; - release = { - "1.14.0".sha256 = "07yamlp1c0g5nahkd2gpfhammcca74ga2s6qr7a3wm6y6j5pivk9"; - "1.13.0".sha256 = "0j4cz2y1r1aw79snkcf1pmicgzf8swbaf9ippz0vg99a572zqzri"; - "1.12.0".sha256 = "1ccfny1vwgmdl91kz5xlmhq4wz078xm4z5wpd0jy5rn890dx03wp"; - "1.11.0".sha256 = "06a71d196wd5k4wg7khwqb7j7ifr7garhwkd54s86i0j7d6nhl3c"; - "1.10.0".sha256 = "1b9m6pwxxyivw7rgx82gn5kmgv2mfv3h3y0mmjcjfypi8ydkrlbv"; - "1.9.0".sha256 = "0lid9zaazdi3d38l8042lczb02pw5m9wq0yysiilx891hgq2p81r"; - "1.8.0".sha256 = "07l40is389ih8bi525gpqs3qp4yb2kl11r9c8ynk1ifpjzpnabwp"; - "1.7.0".sha256 = "0wnhj9nqpx2bw6n1l4i8jgrw3pjajvckvj3lr4vzjb3my2lbxdd1"; - "1.6.4".sha256 = "09ww48qbjsvpjmy1g9yhm0rrkq800ffq21p6fjkbwd34qvd82raz"; - "1.6.1".sha256 = "1ilw6vm4dlsdv9cd7kmf0vfrh2kkzr45wrqr8m37miy0byzr4p9i"; - }; - releaseRev = v: "mathcomp-${v}"; - - # list of core mathcomp packages sorted by dependency order - packages = [ "ssreflect" "fingroup" "algebra" "solvable" "field" "character" "all" ]; - - mathcomp_ = package: let - mathcomp-deps = if package == "single" then [] - else map mathcomp_ (head (splitList (pred.equal package) packages)); - pkgpath = if package == "single" then "mathcomp" else "mathcomp/${package}"; - pname = if package == "single" then "mathcomp" else "mathcomp-${package}"; - pkgallMake = '' - echo "all.v" > Make - echo "-I ." >> Make - echo "-R . mathcomp.all" >> Make - ''; - derivation = mkCoqDerivation ({ - inherit version pname defaultVersion release releaseRev repo owner; - - mlPlugin = versions.isLe "8.6" coq.coq-version; - nativeBuildInputs = optionals withDoc [ graphviz lua ]; - buildInputs = [ ncurses ]; - propagatedBuildInputs = [ coq-elpi hierarchy-builder ] ++ mathcomp-deps; - - buildFlags = optional withDoc "doc"; - - preBuild = '' - if [[ -f etc/utils/ssrcoqdep ]] - then patchShebangs etc/utils/ssrcoqdep - fi - if [[ -f etc/buildlibgraph ]] - then patchShebangs etc/buildlibgraph - fi - '' + '' - cd ${pkgpath} - '' + optionalString (package == "all") pkgallMake; - - meta = { - homepage = "https://math-comp.github.io/"; - license = licenses.cecill-b; - maintainers = with maintainers; [ vbgl jwiegley cohencyril ]; - }; - } // optionalAttrs (package != "single") - { passthru = genAttrs packages mathcomp_; } - // optionalAttrs withDoc { - htmldoc_template = - fetchzip { - url = "https://github.com/math-comp/math-comp.github.io/archive/doc-1.12.0.zip"; - sha256 = "0y1352ha2yy6k2dl375sb1r68r1qi9dyyy7dyzj5lp9hxhhq69x8"; - }; - postBuild = '' - cp -rf _build_doc/* . - rm -r _build_doc - ''; - postInstall = - let tgt = "$out/share/coq/${coq.coq-version}/"; in - optionalString withDoc '' - mkdir -p ${tgt} - cp -r htmldoc ${tgt} - cp -r $htmldoc_template/htmldoc_template/* ${tgt}/htmldoc/ - ''; - buildTargets = "doc"; - extraInstallFlags = [ "-f Makefile.coq" ]; - }); - patched-derivation1 = derivation.overrideAttrs (o: - optionalAttrs (o.pname != null && o.pname == "mathcomp-all" && - o.version != null && o.version != "dev" && versions.isLt "1.7" o.version) - { preBuild = ""; buildPhase = ""; installPhase = "echo doing nothing"; } - ); - patched-derivation = patched-derivation1.overrideAttrs (o: - optionalAttrs (versions.isLe "8.7" coq.coq-version || - (o.version != "dev" && versions.isLe "1.7" o.version)) - { - installFlags = o.installFlags ++ [ "-f Makefile.coq" ]; - } - ); - in patched-derivation; -in -mathcomp_ (if single then "single" else "all") diff --git a/Makefile.coq.local b/Makefile.coq.local new file mode 100644 index 0000000..968028f --- /dev/null +++ b/Makefile.coq.local @@ -0,0 +1,8 @@ +pre-all:: + if command -v coqc > /dev/null && (coqc --version | grep -q '8.18\|8.19\|8.20') ; then \ + for f in $(shell grep "From Corelib" $$(find . -name "*.v") | cut -d: -f1) ; do \ + sed -i.bak $${f} -e 's/From Corelib/From Coq/' ; \ + sed -i.bak $${f} -e 's/PosDef/PArith/' ; \ + $(RM) $${f}.bak ; \ + done ; \ + fi diff --git a/README.md b/README.md index cdc7d61..107febb 100644 --- a/README.md +++ b/README.md @@ -35,7 +35,7 @@ basic plane topology definitions, and a theory of combinatorial hypermaps. - Coq-community maintainer(s): - Yves Bertot ([**@ybertot**](https://github.com/ybertot)) - License: [CeCILL-B](LICENSE) -- Compatible Coq versions: 8.16 or later +- Compatible Coq versions: 8.18 or later - Additional dependencies: - [MathComp ssreflect 2.1.0 or later](https://math-comp.github.io) - [MathComp algebra](https://math-comp.github.io) diff --git a/coq-fourcolor-reals.opam b/coq-fourcolor-reals.opam index 15b62a1..01630bb 100644 --- a/coq-fourcolor-reals.opam +++ b/coq-fourcolor-reals.opam @@ -15,7 +15,7 @@ with proofs of properties such as categoricity.""" build: [make "-C" "theories/reals" "-j%{jobs}%"] install: [make "-C" "theories/reals" "install"] depends: [ - "coq" {>= "8.16"} + "coq" {>= "8.18"} "coq-mathcomp-ssreflect" {>= "2.1.0"} "coq-mathcomp-algebra" ] diff --git a/coq-fourcolor.opam b/coq-fourcolor.opam index cfe2477..f86856a 100644 --- a/coq-fourcolor.opam +++ b/coq-fourcolor.opam @@ -17,7 +17,7 @@ basic plane topology definitions, and a theory of combinatorial hypermaps.""" build: [make "-C" "theories/proof" "-j%{jobs}%"] install: [make "-C" "theories/proof" "install"] depends: [ - "coq" {>= "8.16"} + "coq" {>= "8.18"} "coq-mathcomp-ssreflect" {>= "2.1.0"} "coq-mathcomp-algebra" "coq-hierarchy-builder" {>= "1.5.0"} diff --git a/meta.yml b/meta.yml index 4f5c370..614d4df 100644 --- a/meta.yml +++ b/meta.yml @@ -36,16 +36,12 @@ license: identifier: CECILL-B supported_coq_versions: - text: 8.16 or later - opam: '{>= "8.16"}' + text: 8.18 or later + opam: '{>= "8.18"}' tested_coq_opam_versions: -- version: '2.1.0-coq-8.16' - repo: 'mathcomp/mathcomp' - version: '2.1.0-coq-8.18' repo: 'mathcomp/mathcomp' -- version: '2.2.0-coq-8.16' - repo: 'mathcomp/mathcomp' - version: '2.2.0-coq-8.19' repo: 'mathcomp/mathcomp' - version: '2.3.0-coq-8.20' diff --git a/theories/proof/Makefile.coq.local b/theories/proof/Makefile.coq.local new file mode 100644 index 0000000..968028f --- /dev/null +++ b/theories/proof/Makefile.coq.local @@ -0,0 +1,8 @@ +pre-all:: + if command -v coqc > /dev/null && (coqc --version | grep -q '8.18\|8.19\|8.20') ; then \ + for f in $(shell grep "From Corelib" $$(find . -name "*.v") | cut -d: -f1) ; do \ + sed -i.bak $${f} -e 's/From Corelib/From Coq/' ; \ + sed -i.bak $${f} -e 's/PosDef/PArith/' ; \ + $(RM) $${f}.bak ; \ + done ; \ + fi diff --git a/theories/proof/approx.v b/theories/proof/approx.v index 63d3e71..54d14f2 100644 --- a/theories/proof/approx.v +++ b/theories/proof/approx.v @@ -1,11 +1,11 @@ (* (c) Copyright 2006-2018 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) +From Corelib Require Import Setoid Morphisms. From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice. From mathcomp Require Import fintype tuple path fingraph bigop order ssralg. From mathcomp Require Import ssrnum ssrint div intdiv. From fourcolor Require Import hypermap geometry coloring grid matte. From fourcolor Require Import real realplane. -From Coq Require Import Setoid Morphisms. From fourcolor Require Import realsyntax realprop. (******************************************************************************) diff --git a/theories/proof/dedekind.v b/theories/proof/dedekind.v index af3722c..79c8304 100644 --- a/theories/proof/dedekind.v +++ b/theories/proof/dedekind.v @@ -1,9 +1,9 @@ (* (c) Copyright 2006-2018 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) +From Corelib Require Import Setoid Morphisms. From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq order. From mathcomp Require Import ssralg ssrnum ssrint rat. From fourcolor Require Import real. -From Coq Require Import Setoid Morphisms. (******************************************************************************) (* Construcion of the real numbers as a complete totally ordered field. *) diff --git a/theories/reals/Makefile.coq.local b/theories/reals/Makefile.coq.local new file mode 100644 index 0000000..968028f --- /dev/null +++ b/theories/reals/Makefile.coq.local @@ -0,0 +1,8 @@ +pre-all:: + if command -v coqc > /dev/null && (coqc --version | grep -q '8.18\|8.19\|8.20') ; then \ + for f in $(shell grep "From Corelib" $$(find . -name "*.v") | cut -d: -f1) ; do \ + sed -i.bak $${f} -e 's/From Corelib/From Coq/' ; \ + sed -i.bak $${f} -e 's/PosDef/PArith/' ; \ + $(RM) $${f}.bak ; \ + done ; \ + fi diff --git a/theories/reals/realcategorical.v b/theories/reals/realcategorical.v index a4a6894..80f4593 100644 --- a/theories/reals/realcategorical.v +++ b/theories/reals/realcategorical.v @@ -1,8 +1,8 @@ (* (c) Copyright 2006-2018 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) +From Corelib Require Import Setoid Morphisms. From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq order. From mathcomp Require Import ssralg ssrnum ssrint rat. -From Coq Require Import Morphisms Setoid. From fourcolor Require Import real realsyntax realprop. (******************************************************************************) diff --git a/theories/reals/realprop.v b/theories/reals/realprop.v index 8af8291..d1e76b9 100644 --- a/theories/reals/realprop.v +++ b/theories/reals/realprop.v @@ -1,8 +1,8 @@ (* (c) Copyright 2006-2018 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) +From Corelib Require Import Morphisms Setoid. From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat div order. From mathcomp Require Import ssralg ssrnum ssrint archimedean rat intdiv. -From Coq Require Import Morphisms Setoid. From fourcolor Require Import real realsyntax. (******************************************************************************)