From 0e9d2322ebaba6b420b2b39f572f9983e8fa50e5 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 21 Feb 2025 18:18:55 +0100 Subject: [PATCH 1/2] [CI] Drop Coq 8.16 and 8.17 --- .github/workflows/nix-action-8.16.yml | 254 -------------------------- .github/workflows/nix-action-8.17.yml | 254 -------------------------- .nix/config.nix | 10 +- coq-mathcomp-odd-order.opam | 2 +- 4 files changed, 2 insertions(+), 518 deletions(-) delete mode 100644 .github/workflows/nix-action-8.16.yml delete mode 100644 .github/workflows/nix-action-8.17.yml diff --git a/.github/workflows/nix-action-8.16.yml b/.github/workflows/nix-action-8.16.yml deleted file mode 100644 index 20042a6..0000000 --- a/.github/workflows/nix-action-8.16.yml +++ /dev/null @@ -1,254 +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 math-comp - uses: cachix/cachix-action@v15 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepGetDerivation - name: Getting derivation for current job (coq) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.16\" --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.16" --argstr - job "coq" - mathcomp: - needs: - - coq - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@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 math-comp - uses: cachix/cachix-action@v15 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepGetDerivation - name: Getting derivation for current job (mathcomp) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.16\" --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 - 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.16" --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 "8.16" --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" --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" --argstr - job "mathcomp-fingroup" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr - job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-solvable' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr - job "mathcomp-solvable" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr - job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-character' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr - job "mathcomp-character" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: hierarchy-builder' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --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" --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" --argstr - job "mathcomp" - odd-order: - needs: - - coq - - mathcomp - 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 math-comp - uses: cachix/cachix-action@v15 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepGetDerivation - name: Getting derivation for current job (odd-order) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.16\" --argstr job \"odd-order\" \\\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.16" --argstr - job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-character' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr - job "mathcomp-character" - - 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" --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" --argstr - job "mathcomp-fingroup" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr - job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-solvable' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr - job "mathcomp-solvable" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr - job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr - job "mathcomp" - - 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" --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" --argstr - job "odd-order" -name: Nix CI for bundle 8.16 -on: - pull_request: - paths: - - .github/workflows/nix-action-8.16.yml - pull_request_target: - paths-ignore: - - .github/workflows/nix-action-8.16.yml - types: - - opened - - synchronize - - reopened - push: - branches: - - master diff --git a/.github/workflows/nix-action-8.17.yml b/.github/workflows/nix-action-8.17.yml deleted file mode 100644 index 95df62f..0000000 --- a/.github/workflows/nix-action-8.17.yml +++ /dev/null @@ -1,254 +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 math-comp - uses: cachix/cachix-action@v15 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepGetDerivation - name: Getting derivation for current job (coq) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.17\" --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.17" --argstr - job "coq" - mathcomp: - needs: - - coq - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@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 math-comp - uses: cachix/cachix-action@v15 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepGetDerivation - name: Getting derivation for current job (mathcomp) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.17\" --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 - 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" --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 "8.17" --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.17" --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" --argstr - job "mathcomp-fingroup" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr - job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-solvable' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr - job "mathcomp-solvable" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr - job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-character' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr - job "mathcomp-character" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: hierarchy-builder' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --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.17" --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" --argstr - job "mathcomp" - odd-order: - needs: - - coq - - mathcomp - 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 math-comp - uses: cachix/cachix-action@v15 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepGetDerivation - name: Getting derivation for current job (odd-order) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"8.17\" --argstr job \"odd-order\" \\\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" --argstr - job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-character' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr - job "mathcomp-character" - - 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" --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" --argstr - job "mathcomp-fingroup" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr - job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-solvable' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr - job "mathcomp-solvable" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr - job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr - job "mathcomp" - - 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" --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" --argstr - job "odd-order" -name: Nix CI for bundle 8.17 -on: - pull_request: - paths: - - .github/workflows/nix-action-8.17.yml - pull_request_target: - paths-ignore: - - .github/workflows/nix-action-8.17.yml - types: - - opened - - synchronize - - reopened - push: - branches: - - master diff --git a/.nix/config.nix b/.nix/config.nix index b9ac7a8..e3b107b 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -30,19 +30,11 @@ ## select an entry to build in the following `bundles` set ## defaults to "default" - default-bundle = "8.18"; + 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."8.16".coqPackages = { - coq.override.version = "8.16"; - mathcomp.override.version = "mathcomp-2.1.0"; - }; - bundles."8.17".coqPackages = { - coq.override.version = "8.17"; - mathcomp.override.version = "mathcomp-2.1.0"; - }; bundles."8.18".coqPackages = { coq.override.version = "8.18"; mathcomp.override.version = "mathcomp-2.1.0"; diff --git a/coq-mathcomp-odd-order.opam b/coq-mathcomp-odd-order.opam index 80af8c9..b343316 100644 --- a/coq-mathcomp-odd-order.opam +++ b/coq-mathcomp-odd-order.opam @@ -13,7 +13,7 @@ install: [ make "install" ] depends: [ "ocaml" "coq-mathcomp-character" { (>= "2.0.0") | (= "dev") } - "coq" { >= "8.16" } + "coq" { >= "8.18" } ] tags: [ "keyword:finite groups" "keyword:Feit Thompson theorem" "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" ] authors: [ "Jeremy Avigad <>" "Andrea Asperti <>" "Stephane Le Roux <>" "Yves Bertot <>" "Laurence Rideau <>" "Enrico Tassi <>" "Ioana Pasca <>" "Georges Gonthier <>" "Sidi Ould Biha <>" "Cyril Cohen <>" "Francois Garillot <>" "Alexey Solovyev <>" "Russell O'Connor <>" "Laurent Théry <>" "Assia Mahboubi <>" ] From 693ed245d337fad52241a43050ba1d32a214d05e Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Tue, 18 Feb 2025 10:14:28 +0100 Subject: [PATCH 2/2] Remove Stdlib dependency --- Makefile.coq.local | 8 ++++++++ theories/PFsection1.v | 2 +- 2 files changed, 9 insertions(+), 1 deletion(-) create mode 100644 Makefile.coq.local 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/theories/PFsection1.v b/theories/PFsection1.v index 414a05b..b4073da 100644 --- a/theories/PFsection1.v +++ b/theories/PFsection1.v @@ -1,6 +1,6 @@ (* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) -From Coq Require Import RelationClasses. +From Corelib Require Import RelationClasses. From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path. From mathcomp Require Import div choice fintype tuple finfun bigop prime finset. From mathcomp Require Import order.