diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index faae92d..61c7bc8 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -9,6 +9,7 @@ on: pull_request: branches: - '**' + workflow_dispatch: jobs: build: @@ -17,14 +18,17 @@ jobs: strategy: matrix: image: - - 'mathcomp/mathcomp-dev:coq-8.20' - - 'mathcomp/mathcomp-dev:coq-8.19' - - 'mathcomp/mathcomp:2.2.0-coq-8.20' - - 'mathcomp/mathcomp:2.2.0-coq-8.19' - - 'mathcomp/mathcomp:2.1.0-coq-8.18' + - 'mathcomp/mathcomp-dev:rocq-prover-dev' + - 'mathcomp/mathcomp-dev:rocq-prover-9.2' + - 'mathcomp/mathcomp-dev:rocq-prover-9.1' + - 'mathcomp/mathcomp-dev:rocq-prover-9.0' + - 'mathcomp/mathcomp:2.5.0-rocq-prover-9.1' + - 'mathcomp/mathcomp:2.5.0-rocq-prover-9.0' + - 'mathcomp/mathcomp:2.4.0-rocq-prover-9.1' + - 'mathcomp/mathcomp:2.4.0-rocq-prover-9.0' fail-fast: false steps: - - uses: actions/checkout@v3 + - uses: actions/checkout@v4 - uses: coq-community/docker-coq-action@v1 with: opam_file: 'coq-mathcomp-abel.opam' diff --git a/.github/workflows/nix-action-coq-9.0.yml b/.github/workflows/nix-action-coq-9.0.yml deleted file mode 100644 index 31ec2cd..0000000 --- a/.github/workflows/nix-action-coq-9.0.yml +++ /dev/null @@ -1,410 +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 - \"coq-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 "coq-9.0" - --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 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-elpi) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"coq-9.0\" --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 "coq-9.0" - --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 "coq-9.0" - --argstr job "coq-elpi" - hierarchy-builder: - needs: - - coq - - coq-elpi - 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 (hierarchy-builder) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"coq-9.0\" --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 - 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 "coq-9.0" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq-elpi' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-9.0" - --argstr job "coq-elpi" - - 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 "coq-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 "coq-9.0" - --argstr job "hierarchy-builder" - mathcomp-abel: - needs: - - coq - - mathcomp-real-closed - 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-abel) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"coq-9.0\" --argstr job \"mathcomp-abel\" \\\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 "coq-9.0" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-9.0" - --argstr job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-real-closed' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-9.0" - --argstr job "mathcomp-real-closed" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-9.0" - --argstr job "mathcomp-abel" - mathcomp-bigenough: - 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-bigenough) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"coq-9.0\" --argstr job \"mathcomp-bigenough\" \\\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 "coq-9.0" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-9.0" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-9.0" - --argstr job "mathcomp-bigenough" - mathcomp-real-closed: - needs: - - coq - - mathcomp-bigenough - 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-real-closed) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"coq-9.0\" --argstr job \"mathcomp-real-closed\" \\\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 "coq-9.0" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-9.0" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-9.0" - --argstr job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-9.0" - --argstr job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-fingroup' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-9.0" - --argstr job "mathcomp-fingroup" - - 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 "coq-9.0" - --argstr job "mathcomp-solvable" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-bigenough' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-9.0" - --argstr job "mathcomp-bigenough" - - 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 "coq-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 "coq-9.0" - --argstr job "mathcomp-real-closed" -name: Nix CI for bundle coq-9.0 -on: - pull_request: - paths: - - .github/workflows/nix-action-coq-9.0.yml - pull_request_target: - paths-ignore: - - .github/workflows/nix-action-coq-9.0.yml - types: - - opened - - synchronize - - reopened - push: - branches: - - master diff --git a/.github/workflows/nix-action-coq8.18+mcmathcomp-2.1.0.yml b/.github/workflows/nix-action-coq8.18+mcmathcomp-2.1.0.yml deleted file mode 100644 index 29ff130..0000000 --- a/.github/workflows/nix-action-coq8.18+mcmathcomp-2.1.0.yml +++ /dev/null @@ -1,285 +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 - \"coq8.18+mcmathcomp-2.1.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 "coq8.18+mcmathcomp-2.1.0" - --argstr job "coq" - mathcomp-abel: - needs: - - coq - - mathcomp-real-closed - 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-abel) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"coq8.18+mcmathcomp-2.1.0\" --argstr job \"mathcomp-abel\" \\\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 "coq8.18+mcmathcomp-2.1.0" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18+mcmathcomp-2.1.0" - --argstr job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-real-closed' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18+mcmathcomp-2.1.0" - --argstr job "mathcomp-real-closed" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18+mcmathcomp-2.1.0" - --argstr job "mathcomp-abel" - mathcomp-bigenough: - 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-bigenough) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"coq8.18+mcmathcomp-2.1.0\" --argstr job \"mathcomp-bigenough\" \\\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 "coq8.18+mcmathcomp-2.1.0" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18+mcmathcomp-2.1.0" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18+mcmathcomp-2.1.0" - --argstr job "mathcomp-bigenough" - mathcomp-real-closed: - needs: - - coq - - mathcomp-bigenough - 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-real-closed) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"coq8.18+mcmathcomp-2.1.0\" --argstr job \"mathcomp-real-closed\" \\\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 "coq8.18+mcmathcomp-2.1.0" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18+mcmathcomp-2.1.0" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18+mcmathcomp-2.1.0" - --argstr job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18+mcmathcomp-2.1.0" - --argstr job "mathcomp-field" - - 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 "coq8.18+mcmathcomp-2.1.0" - --argstr job "mathcomp-fingroup" - - 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 "coq8.18+mcmathcomp-2.1.0" - --argstr job "mathcomp-solvable" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-bigenough' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.18+mcmathcomp-2.1.0" - --argstr job "mathcomp-bigenough" - - 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 "coq8.18+mcmathcomp-2.1.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 "coq8.18+mcmathcomp-2.1.0" - --argstr job "mathcomp-real-closed" -name: Nix CI for bundle coq8.18+mcmathcomp-2.1.0 -on: - pull_request: - paths: - - .github/workflows/nix-action-coq8.18+mcmathcomp-2.1.0.yml - pull_request_target: - paths-ignore: - - .github/workflows/nix-action-coq8.18+mcmathcomp-2.1.0.yml - types: - - opened - - synchronize - - reopened - push: - branches: - - master diff --git a/.github/workflows/nix-action-coq8.19+mcmathcomp-2.2.0.yml b/.github/workflows/nix-action-coq8.19+mcmathcomp-2.2.0.yml deleted file mode 100644 index 615bdde..0000000 --- a/.github/workflows/nix-action-coq8.19+mcmathcomp-2.2.0.yml +++ /dev/null @@ -1,285 +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 - \"coq8.19+mcmathcomp-2.2.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 "coq8.19+mcmathcomp-2.2.0" - --argstr job "coq" - mathcomp-abel: - needs: - - coq - - mathcomp-real-closed - 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-abel) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"coq8.19+mcmathcomp-2.2.0\" --argstr job \"mathcomp-abel\" \\\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 "coq8.19+mcmathcomp-2.2.0" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.19+mcmathcomp-2.2.0" - --argstr job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-real-closed' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.19+mcmathcomp-2.2.0" - --argstr job "mathcomp-real-closed" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.19+mcmathcomp-2.2.0" - --argstr job "mathcomp-abel" - mathcomp-bigenough: - 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-bigenough) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"coq8.19+mcmathcomp-2.2.0\" --argstr job \"mathcomp-bigenough\" \\\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 "coq8.19+mcmathcomp-2.2.0" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.19+mcmathcomp-2.2.0" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.19+mcmathcomp-2.2.0" - --argstr job "mathcomp-bigenough" - mathcomp-real-closed: - needs: - - coq - - mathcomp-bigenough - 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-real-closed) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"coq8.19+mcmathcomp-2.2.0\" --argstr job \"mathcomp-real-closed\" \\\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 "coq8.19+mcmathcomp-2.2.0" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.19+mcmathcomp-2.2.0" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.19+mcmathcomp-2.2.0" - --argstr job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.19+mcmathcomp-2.2.0" - --argstr job "mathcomp-field" - - 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 "coq8.19+mcmathcomp-2.2.0" - --argstr job "mathcomp-fingroup" - - 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 "coq8.19+mcmathcomp-2.2.0" - --argstr job "mathcomp-solvable" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-bigenough' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.19+mcmathcomp-2.2.0" - --argstr job "mathcomp-bigenough" - - 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 "coq8.19+mcmathcomp-2.2.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 "coq8.19+mcmathcomp-2.2.0" - --argstr job "mathcomp-real-closed" -name: Nix CI for bundle coq8.19+mcmathcomp-2.2.0 -on: - pull_request: - paths: - - .github/workflows/nix-action-coq8.19+mcmathcomp-2.2.0.yml - pull_request_target: - paths-ignore: - - .github/workflows/nix-action-coq8.19+mcmathcomp-2.2.0.yml - types: - - opened - - synchronize - - reopened - push: - branches: - - master diff --git a/.github/workflows/nix-action-coq8.20+mcmathcomp-2.3.0.yml b/.github/workflows/nix-action-coq8.20+mcmathcomp-2.3.0.yml deleted file mode 100644 index 11ab9f8..0000000 --- a/.github/workflows/nix-action-coq8.20+mcmathcomp-2.3.0.yml +++ /dev/null @@ -1,285 +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 - \"coq8.20+mcmathcomp-2.3.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 "coq8.20+mcmathcomp-2.3.0" - --argstr job "coq" - mathcomp-abel: - needs: - - coq - - mathcomp-real-closed - 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-abel) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"coq8.20+mcmathcomp-2.3.0\" --argstr job \"mathcomp-abel\" \\\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 "coq8.20+mcmathcomp-2.3.0" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.20+mcmathcomp-2.3.0" - --argstr job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-real-closed' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.20+mcmathcomp-2.3.0" - --argstr job "mathcomp-real-closed" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.20+mcmathcomp-2.3.0" - --argstr job "mathcomp-abel" - mathcomp-bigenough: - 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-bigenough) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"coq8.20+mcmathcomp-2.3.0\" --argstr job \"mathcomp-bigenough\" \\\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 "coq8.20+mcmathcomp-2.3.0" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.20+mcmathcomp-2.3.0" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.20+mcmathcomp-2.3.0" - --argstr job "mathcomp-bigenough" - mathcomp-real-closed: - needs: - - coq - - mathcomp-bigenough - 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-real-closed) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"coq8.20+mcmathcomp-2.3.0\" --argstr job \"mathcomp-real-closed\" \\\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 "coq8.20+mcmathcomp-2.3.0" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.20+mcmathcomp-2.3.0" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.20+mcmathcomp-2.3.0" - --argstr job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.20+mcmathcomp-2.3.0" - --argstr job "mathcomp-field" - - 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 "coq8.20+mcmathcomp-2.3.0" - --argstr job "mathcomp-fingroup" - - 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 "coq8.20+mcmathcomp-2.3.0" - --argstr job "mathcomp-solvable" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-bigenough' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq8.20+mcmathcomp-2.3.0" - --argstr job "mathcomp-bigenough" - - 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 "coq8.20+mcmathcomp-2.3.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 "coq8.20+mcmathcomp-2.3.0" - --argstr job "mathcomp-real-closed" -name: Nix CI for bundle coq8.20+mcmathcomp-2.3.0 -on: - pull_request: - paths: - - .github/workflows/nix-action-coq8.20+mcmathcomp-2.3.0.yml - pull_request_target: - paths-ignore: - - .github/workflows/nix-action-coq8.20+mcmathcomp-2.3.0.yml - types: - - opened - - synchronize - - reopened - push: - branches: - - master diff --git a/.github/workflows/nix-action-coqmaster+mcmaster.yml b/.github/workflows/nix-action-coqmaster+mcmaster.yml deleted file mode 100644 index 50fc257..0000000 --- a/.github/workflows/nix-action-coqmaster+mcmaster.yml +++ /dev/null @@ -1,366 +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@v3 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ - \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ - \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ - \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ - \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v27 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v15 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target coq - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coqmaster+mcmaster\" --argstr job \"coq\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\ - built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coqmaster+mcmaster" - --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@v3 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ - \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ - \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ - \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ - \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v27 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v15 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target coq-elpi - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coqmaster+mcmaster\" --argstr job \"coq-elpi\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coqmaster+mcmaster" - --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 "coqmaster+mcmaster" - --argstr job "coq-elpi" - hierarchy-builder: - needs: - - coq - - coq-elpi - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ - \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ - \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ - \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ - \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v27 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v15 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target hierarchy-builder - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coqmaster+mcmaster\" --argstr job \"hierarchy-builder\" \\\n \ - \ --dry-run 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run\ - \ | grep \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coqmaster+mcmaster" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq-elpi' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coqmaster+mcmaster" - --argstr job "coq-elpi" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coqmaster+mcmaster" - --argstr job "hierarchy-builder" - mathcomp-abel: - needs: - - coq - - mathcomp-real-closed - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ - \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ - \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ - \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ - \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v27 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v15 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target mathcomp-abel - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coqmaster+mcmaster\" --argstr job \"mathcomp-abel\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coqmaster+mcmaster" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coqmaster+mcmaster" - --argstr job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-real-closed' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coqmaster+mcmaster" - --argstr job "mathcomp-real-closed" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coqmaster+mcmaster" - --argstr job "mathcomp-abel" - mathcomp-bigenough: - needs: - - coq - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ - \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ - \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ - \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ - \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v27 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v15 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target mathcomp-bigenough - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coqmaster+mcmaster\" --argstr job \"mathcomp-bigenough\" \\\n \ - \ --dry-run 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run\ - \ | grep \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coqmaster+mcmaster" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coqmaster+mcmaster" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coqmaster+mcmaster" - --argstr job "mathcomp-bigenough" - mathcomp-real-closed: - needs: - - coq - - mathcomp-bigenough - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ - \ }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ - \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ - \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ - \ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\ - \ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\ - \ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\ - \ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\ - \ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v3 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v27 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v15 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target mathcomp-real-closed - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coqmaster+mcmaster\" --argstr job \"mathcomp-real-closed\" \\\n\ - \ --dry-run 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run\ - \ | grep \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coqmaster+mcmaster" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coqmaster+mcmaster" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coqmaster+mcmaster" - --argstr job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coqmaster+mcmaster" - --argstr job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-fingroup' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coqmaster+mcmaster" - --argstr job "mathcomp-fingroup" - - 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 "coqmaster+mcmaster" - --argstr job "mathcomp-solvable" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-bigenough' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coqmaster+mcmaster" - --argstr job "mathcomp-bigenough" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coqmaster+mcmaster" - --argstr job "mathcomp-real-closed" -name: Nix CI for bundle coqmaster+mcmaster -'on': - pull_request: - paths: - - .github/workflows/nix-action-coqmaster+mcmaster.yml - pull_request_target: - paths-ignore: - - .github/workflows/nix-action-coqmaster+mcmaster.yml - types: - - opened - - synchronize - - reopened - push: - branches: - - master diff --git a/.github/workflows/nix-action-rocq-9.0.yml b/.github/workflows/nix-action-rocq-9.0.yml new file mode 100644 index 0000000..72f7453 --- /dev/null +++ b/.github/workflows/nix-action-rocq-9.0.yml @@ -0,0 +1,200 @@ +jobs: + coq: + needs: + - rocq-core + 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@v6 + 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@v6 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v31 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v16 + 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 + \"rocq-9.0\" --argstr job \"coq\" \\\n --dry-run 2> err > out || (touch + fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation + failed\"; exit 1; fi\n" + - id: stepCheck + name: Checking presence of CI target for current job + run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs + actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ + ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ + \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ + status=fetched\" >> $GITHUB_OUTPUT\nfi\n" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: rocq-core' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.0" --argstr job "rocq-core" + - if: steps.stepCheck.outputs.status != 'fetched' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.0" --argstr job "coq" + mathcomp-abel: + 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@v6 + 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@v6 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v31 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v16 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepGetDerivation + name: Getting derivation for current job (mathcomp-abel) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"rocq-9.0\" --argstr job \"mathcomp-abel\" \\\n --dry-run 2> err > out + || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting + derivation failed\"; exit 1; fi\n" + - id: stepCheck + name: Checking presence of CI target for current job + run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs + actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ + ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ + \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ + status=fetched\" >> $GITHUB_OUTPUT\nfi\n" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.0" --argstr job "coq" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.0" --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-field' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.0" --argstr job "mathcomp-field" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-real-closed' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.0" --argstr job "mathcomp-real-closed" + - if: steps.stepCheck.outputs.status != 'fetched' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.0" --argstr job "mathcomp-abel" + rocq-core: + 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@v6 + 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@v6 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v31 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v16 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepGetDerivation + name: Getting derivation for current job (rocq-core) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"rocq-9.0\" --argstr job \"rocq-core\" \\\n --dry-run 2> err > out || (touch + fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation + failed\"; exit 1; fi\n" + - id: stepCheck + name: Checking presence of CI target for current job + run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs + actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ + ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ + \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ + status=fetched\" >> $GITHUB_OUTPUT\nfi\n" + - if: steps.stepCheck.outputs.status != 'fetched' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.0" --argstr job "rocq-core" +name: Nix CI for bundle rocq-9.0 +on: + pull_request: + paths: + - .github/workflows/nix-action-rocq-9.0.yml + pull_request_target: + paths-ignore: + - .github/workflows/nix-action-rocq-9.0.yml + types: + - opened + - synchronize + - reopened + push: + branches: + - master diff --git a/.github/workflows/nix-action-rocq-9.1.yml b/.github/workflows/nix-action-rocq-9.1.yml new file mode 100644 index 0000000..3b8a13b --- /dev/null +++ b/.github/workflows/nix-action-rocq-9.1.yml @@ -0,0 +1,200 @@ +jobs: + coq: + needs: + - rocq-core + 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@v6 + 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@v6 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v31 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v16 + 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 + \"rocq-9.1\" --argstr job \"coq\" \\\n --dry-run 2> err > out || (touch + fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation + failed\"; exit 1; fi\n" + - id: stepCheck + name: Checking presence of CI target for current job + run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs + actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ + ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ + \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ + status=fetched\" >> $GITHUB_OUTPUT\nfi\n" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: rocq-core' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "rocq-core" + - if: steps.stepCheck.outputs.status != 'fetched' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "coq" + mathcomp-abel: + 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@v6 + 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@v6 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v31 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v16 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepGetDerivation + name: Getting derivation for current job (mathcomp-abel) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"rocq-9.1\" --argstr job \"mathcomp-abel\" \\\n --dry-run 2> err > out + || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting + derivation failed\"; exit 1; fi\n" + - id: stepCheck + name: Checking presence of CI target for current job + run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs + actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ + ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ + \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ + status=fetched\" >> $GITHUB_OUTPUT\nfi\n" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "coq" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-field' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "mathcomp-field" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-real-closed' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "mathcomp-real-closed" + - if: steps.stepCheck.outputs.status != 'fetched' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "mathcomp-abel" + rocq-core: + 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@v6 + 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@v6 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v31 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v16 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepGetDerivation + name: Getting derivation for current job (rocq-core) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"rocq-9.1\" --argstr job \"rocq-core\" \\\n --dry-run 2> err > out || (touch + fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation + failed\"; exit 1; fi\n" + - id: stepCheck + name: Checking presence of CI target for current job + run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs + actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ + ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ + \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ + status=fetched\" >> $GITHUB_OUTPUT\nfi\n" + - if: steps.stepCheck.outputs.status != 'fetched' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "rocq-core" +name: Nix CI for bundle rocq-9.1 +on: + pull_request: + paths: + - .github/workflows/nix-action-rocq-9.1.yml + pull_request_target: + paths-ignore: + - .github/workflows/nix-action-rocq-9.1.yml + types: + - opened + - synchronize + - reopened + push: + branches: + - master diff --git a/.github/workflows/nix-action-coq-master.yml b/.github/workflows/nix-action-rocq-master.yml similarity index 56% rename from .github/workflows/nix-action-coq-master.yml rename to .github/workflows/nix-action-rocq-master.yml index 78d5918..1e93d70 100644 --- a/.github/workflows/nix-action-coq-master.yml +++ b/.github/workflows/nix-action-rocq-master.yml @@ -1,8 +1,7 @@ jobs: - bignums: + coq: needs: - - coq - - stdlib + - rocq-core runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -10,7 +9,7 @@ jobs: github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\nfi\n" - name: Git checkout - uses: actions/checkout@v4 + uses: actions/checkout@v6 with: fetch-depth: 0 ref: ${{ env.target_commit }} @@ -24,46 +23,44 @@ jobs: }}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\ \ fi\nfi\n" - name: Git checkout - uses: actions/checkout@v4 + uses: actions/checkout@v6 with: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v30 + uses: cachix/install-nix-action@v31 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup math-comp - uses: cachix/cachix-action@v15 + uses: cachix/cachix-action@v16 with: authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} extraPullNames: coq, coq-community name: math-comp - id: stepGetDerivation - name: Getting derivation for current job (bignums) + name: Getting derivation for current job (coq) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"coq-master\" --argstr job \"bignums\" \\\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; + \"rocq-master\" --argstr job \"coq\" \\\n --dry-run 2> err > out || (touch + fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation + failed\"; exit 1; fi\n" - 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 "coq-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 "coq-master" - --argstr job "stdlib" - - if: steps.stepCheck.outputs.status == 'built' + run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs + actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ + ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ + \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ + status=fetched\" >> $GITHUB_OUTPUT\nfi\n" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: rocq-core' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-master" --argstr job "rocq-core" + - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" - --argstr job "bignums" - coq: - needs: [] + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-master" --argstr job "coq" + coq-elpi: + needs: + - rocq-core runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -71,7 +68,7 @@ jobs: github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\nfi\n" - name: Git checkout - uses: actions/checkout@v4 + uses: actions/checkout@v6 with: fetch-depth: 0 ref: ${{ env.target_commit }} @@ -85,39 +82,45 @@ jobs: }}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\ \ fi\nfi\n" - name: Git checkout - uses: actions/checkout@v4 + uses: actions/checkout@v6 with: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v30 + uses: cachix/install-nix-action@v31 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup math-comp - uses: cachix/cachix-action@v15 + uses: cachix/cachix-action@v16 with: authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} extraPullNames: coq, coq-community name: math-comp - id: stepGetDerivation - name: Getting derivation for current job (coq) + name: Getting derivation for current job (coq-elpi) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"coq-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 - run: if [ -e fail ]; then exit 1; else exit 0; fi; + \"rocq-master\" --argstr job \"coq-elpi\" \\\n --dry-run 2> err > out || + (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting + derivation failed\"; exit 1; fi\n" - 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' + run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs + actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ + ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ + \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ + status=fetched\" >> $GITHUB_OUTPUT\nfi\n" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: rocq-core' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-master" --argstr job "rocq-core" + - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" - --argstr job "coq" - coq-elpi: + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-master" --argstr job "coq-elpi" + hierarchy-builder: needs: - - coq + - rocq-core + - coq-elpi runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -125,7 +128,7 @@ jobs: github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\nfi\n" - name: Git checkout - uses: actions/checkout@v4 + uses: actions/checkout@v6 with: fetch-depth: 0 ref: ${{ env.target_commit }} @@ -139,45 +142,49 @@ jobs: }}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\ \ fi\nfi\n" - name: Git checkout - uses: actions/checkout@v4 + uses: actions/checkout@v6 with: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v30 + uses: cachix/install-nix-action@v31 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup math-comp - uses: cachix/cachix-action@v15 + uses: cachix/cachix-action@v16 with: authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} extraPullNames: coq, coq-community name: math-comp - id: stepGetDerivation - name: Getting derivation for current job (coq-elpi) + name: Getting derivation for current job (hierarchy-builder) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"coq-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; + \"rocq-master\" --argstr job \"hierarchy-builder\" \\\n --dry-run 2> err + > out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: + getting derivation failed\"; exit 1; fi\n" - 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 "coq-master" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' + run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs + actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ + ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ + \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ + status=fetched\" >> $GITHUB_OUTPUT\nfi\n" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: rocq-core' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-master" --argstr job "rocq-core" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: coq-elpi' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-master" --argstr job "coq-elpi" + - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" - --argstr job "coq-elpi" - hierarchy-builder: + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-master" --argstr job "hierarchy-builder" + mathcomp: needs: - - coq - - coq-elpi - - stdlib + - rocq-core + - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -185,7 +192,7 @@ jobs: github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\nfi\n" - name: Git checkout - uses: actions/checkout@v4 + uses: actions/checkout@v6 with: fetch-depth: 0 ref: ${{ env.target_commit }} @@ -199,48 +206,49 @@ jobs: }}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\ \ fi\nfi\n" - name: Git checkout - uses: actions/checkout@v4 + uses: actions/checkout@v6 with: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v30 + uses: cachix/install-nix-action@v31 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup math-comp - uses: cachix/cachix-action@v15 + uses: cachix/cachix-action@v16 with: authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} extraPullNames: coq, coq-community name: math-comp - id: stepGetDerivation - name: Getting derivation for current job (hierarchy-builder) + name: Getting derivation for current job (mathcomp) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"coq-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 - run: if [ -e fail ]; then exit 1; else exit 0; fi; + \"rocq-master\" --argstr job \"mathcomp\" \\\n --dry-run 2> err > out || + (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting + derivation failed\"; exit 1; fi\n" - 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 "coq-master" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq-elpi' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" - --argstr job "coq-elpi" - - 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 "coq-master" - --argstr job "stdlib" - - if: steps.stepCheck.outputs.status == 'built' + run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs + actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ + ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ + \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ + status=fetched\" >> $GITHUB_OUTPUT\nfi\n" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: rocq-core' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-master" --argstr job "rocq-core" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-character' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-master" --argstr job "mathcomp-character" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: hierarchy-builder' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-master" --argstr job "hierarchy-builder" + - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" - --argstr job "hierarchy-builder" + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-master" --argstr job "mathcomp" mathcomp-abel: needs: - coq @@ -252,7 +260,7 @@ jobs: github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\nfi\n" - name: Git checkout - uses: actions/checkout@v4 + uses: actions/checkout@v6 with: fetch-depth: 0 ref: ${{ env.target_commit }} @@ -266,16 +274,16 @@ jobs: }}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\ \ fi\nfi\n" - name: Git checkout - uses: actions/checkout@v4 + uses: actions/checkout@v6 with: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v30 + uses: cachix/install-nix-action@v31 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup math-comp - uses: cachix/cachix-action@v15 + uses: cachix/cachix-action@v16 with: authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} extraPullNames: coq, coq-community @@ -283,30 +291,39 @@ jobs: - id: stepGetDerivation name: Getting derivation for current job (mathcomp-abel) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"coq-master\" --argstr job \"mathcomp-abel\" \\\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; + \"rocq-master\" --argstr job \"mathcomp-abel\" \\\n --dry-run 2> err > out + || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting + derivation failed\"; exit 1; fi\n" - 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' + run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs + actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ + ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ + \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ + status=fetched\" >> $GITHUB_OUTPUT\nfi\n" + - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-master" --argstr job "coq" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-master" --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-field' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-master" --argstr job "mathcomp-field" + - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-real-closed' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" - --argstr job "mathcomp-real-closed" - - if: steps.stepCheck.outputs.status == 'built' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-master" --argstr job "mathcomp-real-closed" + - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" - --argstr job "mathcomp-abel" - mathcomp-bigenough: + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-master" --argstr job "mathcomp-abel" + mathcomp-real-closed: needs: - - coq + - rocq-core runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -314,7 +331,7 @@ jobs: github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\nfi\n" - name: Git checkout - uses: actions/checkout@v4 + uses: actions/checkout@v6 with: fetch-depth: 0 ref: ${{ env.target_commit }} @@ -328,45 +345,48 @@ jobs: }}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\ \ fi\nfi\n" - name: Git checkout - uses: actions/checkout@v4 + uses: actions/checkout@v6 with: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v30 + uses: cachix/install-nix-action@v31 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup math-comp - uses: cachix/cachix-action@v15 + uses: cachix/cachix-action@v16 with: authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} extraPullNames: coq, coq-community name: math-comp - id: stepGetDerivation - name: Getting derivation for current job (mathcomp-bigenough) + name: Getting derivation for current job (mathcomp-real-closed) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"coq-master\" --argstr job \"mathcomp-bigenough\" \\\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; + \"rocq-master\" --argstr job \"mathcomp-real-closed\" \\\n --dry-run 2> + err > out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"\ + Error: getting derivation failed\"; exit 1; fi\n" - 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 "coq-master" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' + run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs + actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ + ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ + \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ + status=fetched\" >> $GITHUB_OUTPUT\nfi\n" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: rocq-core' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-master" --argstr job "rocq-core" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-field' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-master" --argstr job "mathcomp-field" + - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" - --argstr job "mathcomp-bigenough" - mathcomp-real-closed: + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-master" --argstr job "mathcomp-real-closed" + micromega-plugin: needs: - - coq - - mathcomp-bigenough - - stdlib + - rocq-core runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -374,7 +394,7 @@ jobs: github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\nfi\n" - name: Git checkout - uses: actions/checkout@v4 + uses: actions/checkout@v6 with: fetch-depth: 0 ref: ${{ env.target_commit }} @@ -388,51 +408,43 @@ jobs: }}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\ \ fi\nfi\n" - name: Git checkout - uses: actions/checkout@v4 + uses: actions/checkout@v6 with: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v30 + uses: cachix/install-nix-action@v31 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup math-comp - uses: cachix/cachix-action@v15 + uses: cachix/cachix-action@v16 with: authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} extraPullNames: coq, coq-community name: math-comp - id: stepGetDerivation - name: Getting derivation for current job (mathcomp-real-closed) + name: Getting derivation for current job (micromega-plugin) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"coq-master\" --argstr job \"mathcomp-real-closed\" \\\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; + \"rocq-master\" --argstr job \"micromega-plugin\" \\\n --dry-run 2> err + > out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: + getting derivation failed\"; exit 1; fi\n" - 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 "coq-master" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-bigenough' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" - --argstr job "mathcomp-bigenough" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: stdlib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" - --argstr job "stdlib" - - if: steps.stepCheck.outputs.status == 'built' + run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs + actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ + ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ + \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ + status=fetched\" >> $GITHUB_OUTPUT\nfi\n" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: rocq-core' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-master" --argstr job "rocq-core" + - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" - --argstr job "mathcomp-real-closed" - stdlib: - needs: - - coq + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-master" --argstr job "micromega-plugin" + rocq-core: + needs: [] runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -440,7 +452,7 @@ jobs: github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\nfi\n" - name: Git checkout - uses: actions/checkout@v4 + uses: actions/checkout@v6 with: fetch-depth: 0 ref: ${{ env.target_commit }} @@ -454,48 +466,99 @@ jobs: }}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\ \ fi\nfi\n" - name: Git checkout - uses: actions/checkout@v4 + uses: actions/checkout@v6 with: fetch-depth: 0 ref: ${{ env.tested_commit }} - name: Cachix install - uses: cachix/install-nix-action@v30 + uses: cachix/install-nix-action@v31 with: nix_path: nixpkgs=channel:nixpkgs-unstable - name: Cachix setup math-comp - uses: cachix/cachix-action@v15 + uses: cachix/cachix-action@v16 with: authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} extraPullNames: coq, coq-community name: math-comp - id: stepGetDerivation - name: Getting derivation for current job (stdlib) + name: Getting derivation for current job (rocq-core) run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"coq-master\" --argstr job \"stdlib\" \\\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; + \"rocq-master\" --argstr job \"rocq-core\" \\\n --dry-run 2> err > out || + (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting + derivation failed\"; exit 1; fi\n" - 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 "coq-master" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' + run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs + actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ + ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ + \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ + status=fetched\" >> $GITHUB_OUTPUT\nfi\n" + - if: steps.stepCheck.outputs.status != 'fetched' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-master" --argstr job "rocq-core" + rocq-elpi: + 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@v6 + 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@v6 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v31 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v16 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepGetDerivation + name: Getting derivation for current job (rocq-elpi) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"rocq-master\" --argstr job \"rocq-elpi\" \\\n --dry-run 2> err > out || + (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting + derivation failed\"; exit 1; fi\n" + - id: stepCheck + name: Checking presence of CI target for current job + run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs + actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ + ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ + \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ + status=fetched\" >> $GITHUB_OUTPUT\nfi\n" + - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" - --argstr job "stdlib" -name: Nix CI for bundle coq-master + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-master" --argstr job "rocq-elpi" +name: Nix CI for bundle rocq-master on: pull_request: paths: - - .github/workflows/nix-action-coq-master.yml + - .github/workflows/nix-action-rocq-master.yml pull_request_target: paths-ignore: - - .github/workflows/nix-action-coq-master.yml + - .github/workflows/nix-action-rocq-master.yml types: - opened - synchronize diff --git a/.nix/config.nix b/.nix/config.nix index 8a98d09..cbcbfc7 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -25,60 +25,48 @@ ## /!\ Manual overlays in `.nix/coq-overlays` should be preferred then. # buildInputs = [ ]; + ## Set this when the package has no rocqPackages version yet + ## (either in nixpkgs or in .nix/rocq-overlays) + no-rocq-yet = true; + ## Indicate the relative location of your _CoqProject ## If not specified, it defaults to "_CoqProject" # coqproject = "_CoqProject"; ## select an entry to build in the following `bundles` set ## defaults to "default" - default-bundle = "coq8.20+mcmathcomp-2.3.0"; + default-bundle = "rocq-9.1"; ## write one `bundles.name` attribute set per ## alternative configuration ## When generating GitHub Action CI, one workflow file ## will be created per bundle - bundles = let - gen = coqv: mcv: elpiv: - { "coq${coqv}+mc${mcv}" = { - coqPackages = { - coq.override.version = coqv; - mathcomp.override.version = mcv; - mathcomp.job = false; - } // (if (coqv == "master") then { - coq-elpi.override.version = "master"; - hierarchy-builder.override.version = "master"; - } else {}) // { - mathcomp-real-closed.override.version = "master"; - mathcomp-bigenough.override.version = "1.0.1"; - }; - ocamlPackages = if (elpiv != "") then { elpi.override.version = elpiv; } else {}; - }; }; in - gen "8.18" "mathcomp-2.1.0" "" // - gen "8.19" "mathcomp-2.2.0" "" // - gen "8.20" "mathcomp-2.3.0" "" // { - "coq-9.0".coqPackages = { - coq.override.version = "9.0"; - coq-elpi.job = true; - hierarchy-builder.job = true; - mathcomp-real-closed.override.version = "master"; - mathcomp-bigenough.override.version = "1.0.2"; - }; - "coq-master" = { rocqPackages = { + bundles = + { + "rocq-master" = { rocqPackages = { rocq-core.override.version = "master"; rocq-elpi.override.version = "master"; - rocq-elpi.override.elpi-version = "2.0.7"; - stdlib.override.version = "master"; - bignums.override.version = "master"; + hierarchy-builder.override.version = "master"; + micromega-plugin.override.version = "master"; + mathcomp.override.version = "master"; + mathcomp-real-closed.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"; + micromega-plugin.override.version = "master"; mathcomp.override.version = "master"; mathcomp-real-closed.override.version = "master"; - mathcomp-bigenough.override.version = "1.0.2"; - stdlib.override.version = "master"; - bignums.override.version = "master"; + }; }; + "rocq-9.1" = { rocqPackages = { + rocq-core.override.version = "9.1"; + }; coqPackages = { + coq.override.version = "9.1"; + }; }; + "rocq-9.0" = { rocqPackages = { + rocq-core.override.version = "9.0"; + }; coqPackages = { + coq.override.version = "9.0"; }; }; }; diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index b53317b..ab408cc 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"23abc2d7903983f4fd414288677d6b421d412cd6" +"9cd6ca08dba2a6557e46cbf3243a24f7f67ec5ff" diff --git a/Makefile.coq.local b/Makefile.coq.local deleted file mode 100644 index f7ea7f6..0000000 --- a/Makefile.coq.local +++ /dev/null @@ -1,8 +0,0 @@ -pre-all:: - if command -v coqc > /dev/null && (coqc --version | grep -q '8.16\|8.17\|8.18\|8.19\|8.20') ; then \ - for f in $(shell grep "From Corelib" $$(find . -name "*.v") | cut -d: -f1) ; do \ - sed -i.bak 's/From Corelib/From Coq/' $${f} ; \ - sed -i.bak 's/PosDef/PArith/' $${f} ; \ - $(RM) $${f}.bak ; \ - done ; \ - fi diff --git a/README.md b/README.md index cf955b6..a2cf601 100644 --- a/README.md +++ b/README.md @@ -26,15 +26,15 @@ Mathematical Components library. - Assia Mahboubi (initial) - Pierre-Yves Strub (initial) - License: [CeCILL-B](CeCILL-B) -- Compatible Coq versions: Coq 8.10 to 8.16 +- Compatible Rocq/Coq versions: 9.0 or later - Additional dependencies: - - [MathComp ssreflect 2.0 and later](https://math-comp.github.io) + - [MathComp ssreflect 2.4 and later](https://math-comp.github.io) - [MathComp fingroup](https://math-comp.github.io) - [MathComp algebra](https://math-comp.github.io) - [MathComp solvable](https://math-comp.github.io) - [MathComp field](https://math-comp.github.io) - - [MathComp real closed >= 2.0.0](https://github.com/math-comp/real-closed) -- Coq namespace: `Abel` + - [MathComp real closed](https://github.com/math-comp/real-closed) +- Rocq/Coq namespace: `Abel` - Related publication(s): - [Unsolvability of the Quintic Formalized in Dependent Type Theory ](https://hal.inria.fr/hal-03136002) @@ -45,15 +45,19 @@ The easiest way to install the latest released version of Abel - Ruffini Theorem is via [OPAM](https://opam.ocaml.org/doc/Install.html): ```shell -opam repo add coq-released https://coq.inria.fr/opam/released +opam repo add rocq-released https://rocq-prover.org/opam/released opam install coq-mathcomp-abel ``` -To instead build and install manually, do: +To instead build and install manually, you need to make sure that all the +libraries this development depends on are installed. The easiest way to do that +is still to rely on opam: ``` shell git clone https://github.com/math-comp/abel.git cd abel +opam repo add rocq-released https://rocq-prover.org/opam/released +opam install --deps-only . make # or make -j make install ``` diff --git a/coq-mathcomp-abel.opam b/coq-mathcomp-abel.opam index b543fe4..ce66454 100644 --- a/coq-mathcomp-abel.opam +++ b/coq-mathcomp-abel.opam @@ -21,13 +21,13 @@ Mathematical Components library.""" build: [make "-j%{jobs}%"] install: [make "install"] depends: [ - "coq" { (>= "8.18" & < "9.1~") | = "dev" } - "coq-mathcomp-ssreflect" { (>= "2.1.0" & < "2.4~") | = "dev" } + "rocq-core" {>= "9.0"} + "coq-mathcomp-ssreflect" {>= "2.4"} "coq-mathcomp-fingroup" "coq-mathcomp-algebra" "coq-mathcomp-solvable" "coq-mathcomp-field" - "coq-mathcomp-real-closed" { (>= "2.0.0") | = "dev" } + "coq-mathcomp-real-closed" ] tags: [ diff --git a/meta.yml b/meta.yml index 61548a2..24596a6 100644 --- a/meta.yml +++ b/meta.yml @@ -41,27 +41,33 @@ license: file: CeCILL-B supported_coq_versions: - text: Coq 8.18 to 9.0 - opam: '{ (>= "8.18" & < "9.1~") | = "dev" }' + text: '9.0 or later' + opam: '{>= "9.0"}' tested_coq_opam_versions: -- version: 'coq-8.20' +- version: 'rocq-prover-dev' repo: 'mathcomp/mathcomp-dev' -- version: 'coq-8.19' +- version: 'rocq-prover-9.2' repo: 'mathcomp/mathcomp-dev' -- version: '2.2.0-coq-8.20' +- version: 'rocq-prover-9.1' + repo: 'mathcomp/mathcomp-dev' +- version: 'rocq-prover-9.0' + repo: 'mathcomp/mathcomp-dev' +- version: '2.5.0-rocq-prover-9.1' + repo: 'mathcomp/mathcomp' +- version: '2.5.0-rocq-prover-9.0' repo: 'mathcomp/mathcomp' -- version: '2.2.0-coq-8.19' +- version: '2.4.0-rocq-prover-9.1' repo: 'mathcomp/mathcomp' -- version: '2.1.0-coq-8.18' +- version: '2.4.0-rocq-prover-9.0' repo: 'mathcomp/mathcomp' dependencies: - opam: name: coq-mathcomp-ssreflect - version: '{ (>= "2.0.0" & < "2.3~") | = "dev" }' + version: '{>= "2.4"}' description: |- - [MathComp ssreflect 2.0 and later](https://math-comp.github.io) + [MathComp ssreflect 2.4 and later](https://math-comp.github.io) - opam: name: coq-mathcomp-fingroup description: |- @@ -80,9 +86,8 @@ dependencies: [MathComp field](https://math-comp.github.io) - opam: name: coq-mathcomp-real-closed - version: '{ (>= "2.0.0") | = "dev" }' description: |- - [MathComp real closed >= 2.0.0](https://github.com/math-comp/real-closed) + [MathComp real closed](https://github.com/math-comp/real-closed) namespace: Abel keywords: diff --git a/theories/abel.v b/theories/abel.v index 9126278..d08c299 100644 --- a/theories/abel.v +++ b/theories/abel.v @@ -556,7 +556,7 @@ Lemma radical_ext_solvable_ext (F0 : fieldType) (L : splittingFieldType F0) Proof. move=> charL EF. move=> [_ /pradicalext_radicalext[[/= n e pw] /towerP epwP <- FK]]. -have charF0 : [char F0] =i pred0 by move=> i; rewrite -charL char_lalg. +have charF0 : [pchar F0] =i pred0 by move=> i; rewrite -charL pchar_lalg. pose k := n; suff {FK} : solvable_ext E <>. by rewrite take_oversize ?size_tuple//; apply: sub_solvable_ext. elim: k => /= [|k IHsol]; first by rewrite take0 Fadjoin_nil. @@ -568,7 +568,7 @@ apply: solvable_ext_trans IHsol _. have := epwP (Ordinal kn); rewrite (tnth_nth 0) (tnth_nth 0%N)/=. move=> /pradicalP[pwk_prime epwEk]. apply: (pradical_solvable_ext pwk_prime) => //. -by have /charf0P-> := charF0; rewrite -lt0n prime_gt0. +by have /pcharf0P-> := charF0; rewrite -lt0n prime_gt0. Qed. (******************************************************************************) @@ -616,24 +616,24 @@ Lemma AbelGaloisPoly (F : fieldType) (p : {poly F}) : has_char0 F -> solvable_ext_poly p <-> solvable_by_radical_poly p. Proof. move=> charF; split=> + L rs pE => [/(_ L rs pE) + w w_prim|solrs]/=. - have charL : has_char0 L by move=> i; rewrite char_lalg. + have charL : has_char0 L by move=> i; rewrite pchar_lalg. have normal_rs : normalField 1 <<1 & rs>>. apply/splitting_normalField; rewrite ?sub1v//. by exists (p ^^ in_alg _); [apply/polyOver1P; exists p | exists rs]. by move=> solrs; apply/(@AbelGalois _ _ w); rewrite ?char0_solvable_extE ?normalClosure_id ?sub1v ?dimv1 ?divn1. -have charL : has_char0 L by move=> i; rewrite char_lalg. +have charL : has_char0 L by move=> i; rewrite pchar_lalg. have seprs: separable 1 <<1 & rs>> by apply/char0_separable. have normal_rs : normalField 1 <<1 & rs>>. apply/splitting_normalField; rewrite ?sub1v//. by exists (p ^^ in_alg _); [apply/polyOver1P; exists p | exists rs]. pose n := \dim <<1 & rs>>. -have nFN0 : n%:R != 0 :> F by have /charf0P-> := charF; rewrite -lt0n adim_gt0. +have nFN0 : n%:R != 0 :> F by have /pcharf0P-> := charF; rewrite -lt0n adim_gt0. apply: (@classic_cycloSplitting _ L _ nFN0) => - [L' [w [iota wL' w_prim]]]. suff: solvable_ext 1 <<1 & rs>>. by rewrite /solvable_ext seprs normalClosure_id ?sub1v. rewrite -(solvable_ext_aimg iota). -have charL' : [char L'] =i pred0 by move=> i; rewrite char_lalg. +have charL' : [pchar L'] =i pred0 by move=> i; rewrite pchar_lalg. apply/(@AbelGalois _ _ w) => //. - by rewrite limgS// sub1v. - rewrite -aimg_normalClosure //= aimg1 dimv1 divn1 dim_aimg/=. @@ -667,8 +667,8 @@ apply: classic_bind (@classic_fieldExtFor _ _ (p : {poly F^o}) p_neq0). exists S, rs; split => //=; first by rewrite -(eq_map_poly iotaF). by apply: (sol_p S rs); rewrite -(eq_map_poly iotaF). move=> L rs prs; apply: sol_p => -[M [rs' [prs']]]. -have charL : has_char0 L by move=> n; rewrite char_lalg charF. -have charM : has_char0 M by move=> n; rewrite char_lalg charF. +have charL : has_char0 L by move=> n; rewrite pchar_lalg charF. +have charM : has_char0 M by move=> n; rewrite pchar_lalg charF. pose K : fieldExtType F := subvs_of <<1 & rs>>%VS. pose rsK := map (vsproj <<1 & rs>>%VS) rs. have pKrs : p ^^ in_alg K %= \prod_(x <- rsK) ('X - x%:P). @@ -712,8 +712,8 @@ split => sol_p; last first. apply: classic_bind sol_p => -[L [rs [prs sol_p]]]; apply/classicW. exists L, rs; split => //; rewrite -galois_solvable. apply: radical_ext_solvable_ext; rewrite ?sub1v// => v. - by rewrite char_lalg charF0. - have charL : has_char0 L by move=> n; rewrite char_lalg charF0. + by rewrite pchar_lalg charF0. + have charL : has_char0 L by move=> n; rewrite pchar_lalg charF0. rewrite char0_galois// ?sub1v//. apply/splitting_normalField; rewrite ?sub1v//. by exists (p ^^ in_alg _); [apply/polyOver1P; exists p | exists rs]. @@ -730,7 +730,7 @@ pose sM := FieldExt_isSplittingField.Build F L splitL. pose S : splittingFieldType F := HB.pack L sM. pose d := \dim <<1 & (rs : seq S)>>. have /classic_cycloSplitting-/(_ S) : d%:R != 0 :> F. - by have /charf0P-> := charF0; rewrite -lt0n adim_gt0. + by have /pcharf0P-> := charF0; rewrite -lt0n adim_gt0. apply/classic_bind => -[C [w [g wg w_prim]]]; apply/classicW. have gf : g \o f =1 in_alg C by move=> v /=; rewrite fF rmorph_alg. have pgrs : p ^^ in_alg C %= \prod_(x <- [seq g i | i <- rs]) ('X - x%:P). @@ -816,7 +816,7 @@ Proof. move=> p_neq0; split. move=> /(solvable_poly_rat p_neq0)[L [_ [rs [prs rssol]]]]. by exists L, <<1 & rs>>%AS; first by exists rs. -have charrat : [char rat] =i pred0 by exact: char_num. +have charrat : [pchar rat] =i pred0 by exact: pchar_num. move=> [L [K [rs prs <-] solK]]; apply/solvable_by_radical_polyP => //. by apply/classicW; exists L, rs. Qed. @@ -835,7 +835,7 @@ Lemma numfieldP (p : {poly rat}) : p != 0 -> splittingFieldFor 1 (p ^^ in_alg (numfield p)) fullv. Proof. by rewrite /numfield; case: splitting_num_field => //= ? [? []]. Qed. -Lemma char_numfield (p : {poly rat}) : [char (numfield p)] =i pred0. +Lemma char_numfield (p : {poly rat}) : [pchar (numfield p)] =i pred0. Proof. exact: char_ext. Qed. #[global] Hint Resolve char_numfield : core. @@ -860,7 +860,7 @@ have [{p}->|p_neq0] := eqVneq p 0. rewrite numfield0 regular_fullv galvv solvable1; constructor. move=> L rs; rewrite eqp_sym rmorph0 eqp0 prodf_seq_eq0. by move=> /hasP[x _ /=]; rewrite polyXsubC_eq0. -have charrat : [char rat] =i pred0 by exact: char_num. +have charrat : [pchar rat] =i pred0 by exact: pchar_num. pose charnumfield := char_ext (numfield p). apply: (equivP idP); rewrite -AbelGaloisPoly//. have [rs prs <-] := numfieldP p_neq0. @@ -1182,7 +1182,7 @@ Definition poly_example : {poly rat} := 'X^5 - 4 *: 'X + 2. Local Definition pesimp := (coefD, coefN, coefB, coefZ, coefXn, coefX, coefC, hornerD, hornerN, hornerC, hornerZ, hornerX, hornerXn, rmorph_nat). -Lemma polyCn (R : ringType) n : n%:R%:P = n%:R :> {poly R}. +Lemma polyCn (R : nzRingType) n : n%:R%:P = n%:R :> {poly R}. Proof. by rewrite rmorph_nat. Qed. Lemma poly_exampleEint : poly_example = map_poly intr poly_example_int. @@ -1193,14 +1193,14 @@ Qed. Lemma size_poly_example_int : size poly_example_int = 6%N. Proof. -rewrite /poly_example_int -addrA size_addl ?size_polyXn//. -by rewrite size_addl ?size_opp ?size_scale ?size_polyX -?polyCn ?size_polyC. +rewrite /poly_example_int -addrA size_polyDl ?size_polyXn//. +by rewrite size_polyDl ?size_polyN ?size_scale ?size_polyX -?polyCn ?size_polyC. Qed. Lemma size_poly_example : size poly_example = 6%N. Proof. -rewrite /poly_example -addrA size_addl ?size_polyXn//. -by rewrite size_addl ?size_opp ?size_scale ?size_polyX -?polyCn ?size_polyC. +rewrite /poly_example -addrA size_polyDl ?size_polyXn//. +by rewrite size_polyDl ?size_polyN ?size_scale ?size_polyX -?polyCn ?size_polyC. Qed. Lemma poly_example_int_neq0 : poly_example_int != 0. @@ -1228,7 +1228,7 @@ rewrite separable_poly.unlock. apply/coprimepP => q /(irredp_XsubCP irreducible_example) [//| eqq]. have size_deriv_example : size poly_example^`() = 5%N. rewrite !derivCE ?mul0rn ?addr0 alg_polyC -scaler_nat. - by rewrite size_addl ?size_scale ?size_opp ?size_polyXn ?size_polyC. + by rewrite size_polyDl ?size_scale ?size_polyN ?size_polyXn ?size_polyC. rewrite gtNdvdp -?size_poly_eq0 ?size_deriv_example//. by rewrite (eqp_size eqq) ?size_poly_example. Qed. @@ -1471,7 +1471,7 @@ Lemma solvable_formula (p : {poly rat}) : p != 0 -> {in root (p ^^ ratr), forall x, exists f : algterm rat, algT_eval ratr f = x}. Proof. -have Cchar := Cchar => p_neq0; split. +have Cchar := Cpchar => p_neq0; split. move=> /solvable_poly_rat[]// L [iota [rs [prs [E rE KE]]]] x. have pirs : p ^^ ratr %= \prod_(x <- map iota rs) ('X - x%:P). have := prs; rewrite -(eqp_map iota) map_prod_XsubC => /eqp_rtrans<-. @@ -1521,7 +1521,7 @@ have Cchar := Cchar => p_neq0; split. case: IHq => // fq fq_eq. exists (fq * fu + Base (Subvs ck))%algT => /=. by rewrite rmorphD rmorphM/= map_polyX map_polyC !hornerE fq_eq. -move=> mkalg; apply/solvable_by_radical_polyP => //=; first exact: char_num. +move=> mkalg; apply/solvable_by_radical_polyP => //=; first exact: pchar_num. have [/= rsalg pE] := closed_field_poly_normal (p ^^ (ratr : _ -> algC)). have {}pE : p ^^ ratr %= \prod_(z <- rsalg) ('X - z%:P). rewrite pE (eqp_trans (eqp_scale _ _)) ?eqpxx//. @@ -1545,7 +1545,7 @@ have mp_neq0 : mp != 0. have {}mpE : mp ^^ ratr = \prod_(z <- rsmpalg) ('X - z%:P). by rewrite mpE lead_coef_map/= (eqP mp_monic) rmorph1 scale1r. have [L [iota [rsmp iota_rs rsf]]] := num_field_exists rsmpalg. -have charL : has_char0 L by move=> x; rewrite char_lalg char_num. +have charL : has_char0 L by move=> x; rewrite pchar_lalg pchar_num. have mprs : mp ^^ in_alg L %= \prod_(z <- rsmp) ('X - z%:P). rewrite -(eqp_map iota) map_prod_XsubC iota_rs -map_poly_comp -mpE. by rewrite -char0_ratrE// (eq_map_poly (fmorph_eq_rat _)) eqpxx. diff --git a/theories/xmathcomp/char0.v b/theories/xmathcomp/char0.v index 7d04d3f..3840355 100644 --- a/theories/xmathcomp/char0.v +++ b/theories/xmathcomp/char0.v @@ -10,7 +10,7 @@ Import GRing.Theory. Local Open Scope ring_scope. -Local Notation has_char0 L := ([char L] =i pred0). +Local Notation has_char0 L := ([pchar L] =i pred0). Section Char0MorphismsIdomain. @@ -23,7 +23,7 @@ Lemma char0_intr_eq0 (z : int) : ((z%:~R : R) == 0) = (z == 0). Proof. suff hPos (m : nat) : (m%:~R == 0 :> R) = (Posz m == 0). by case: z => [m | m] => //; rewrite NegzE rmorphN /= !oppr_eq0. -by rewrite [m%:~R]/(m%:R); move/charf0P: (charR0)->. +by rewrite [m%:~R]/(m%:R); move/pcharf0P: (charR0)->. Qed. Lemma char0_intr_inj : injective (fun i => i%:~R : R). @@ -85,7 +85,7 @@ Section NumberFieldsProps. Variable (L : fieldExtType rat). Lemma char_ext : has_char0 L. (* this works more generally for `lalgType rat` *) -Proof. by move=> x; rewrite char_lalg Num.Theory.char_num. Qed. +Proof. by move=> x; rewrite pchar_lalg Num.Theory.pchar_num. Qed. Hint Resolve char_ext : core. Lemma rat_extratr0 : ratr 0 = 0 :> L. @@ -170,7 +170,7 @@ set r := (_ * f + _)%R. have Nrx : ~~ root r x. rewrite /root !hornerE subrr mulr0 add0r mulf_neq0//. have -> : m.+1%:R = m.+1%:R%:P :> {poly L} by rewrite !raddfMn. - rewrite hornerC natf_neq0/= (eq_pnat _ (eq_negn charL))/=. + rewrite hornerC natf_neq0_pchar/= (eq_pnat _ (eq_negn charL))/=. by apply/andP; split => //; apply/allP. rewrite (eqp_dvdr _ (eqp_divr _ (gcdp_mul2r _ _ _))). rewrite divp_pmul2r//; last 2 first. diff --git a/theories/xmathcomp/cyclotomic_ext.v b/theories/xmathcomp/cyclotomic_ext.v index 43820a0..2b2a99e 100644 --- a/theories/xmathcomp/cyclotomic_ext.v +++ b/theories/xmathcomp/cyclotomic_ext.v @@ -64,7 +64,7 @@ pose q := \prod_(d <- rem n (divisors n)) Q d. have ePp : P n * p = 'X^n - 1 by rewrite -eP fact. have eQq : Q n * q = 'X^n - 1 by rewrite -eQ fact. have Xnsub1N0 : 'X^n - 1 != 0 :> {poly F}. - by rewrite -size_poly_gt0 size_Xn_sub_1. + by rewrite -size_poly_gt0 size_XnsubC. have pN0 : p != 0 by apply: dvdpN0 Xnsub1N0; rewrite -ePp dvdp_mulIr. have epq : p = q. case: (divisors_correct n_gt0) => uniqd sortedd dP. diff --git a/theories/xmathcomp/various.v b/theories/xmathcomp/various.v index a942b93..a4c103c 100644 --- a/theories/xmathcomp/various.v +++ b/theories/xmathcomp/various.v @@ -241,7 +241,7 @@ Qed. Import GRing.Theory. Local Open Scope ring_scope. -Notation has_char0 L := ([char L] =i pred0). +Notation has_char0 L := ([pchar L] =i pred0). (**********) (* ssralg *) @@ -250,14 +250,14 @@ Notation has_char0 L := ([char L] =i pred0). Lemma iter_addr (V : zmodType) n x y : iter n (+%R x) y = x *+ n + y :> V. Proof. by elim: n => [|n ih]; rewrite ?add0r //= ih mulrS addrA. Qed. -Lemma prodrMl {R : comRingType} {I : finType} (A : pred I) (x : R) F : +Lemma prodrMl {R : comPzRingType} {I : finType} (A : pred I) (x : R) F : \prod_(i in A) (x * F i) = x ^+ #|A| * \prod_(i in A) F i. Proof. rewrite -sum1_card; elim/big_rec3: _; first by rewrite expr0 mulr1. by move=> i y p z iA ->; rewrite mulrACA exprS. Qed. -Lemma expr_sum {R : ringType} {T : Type} (x : R) (F : T -> nat) P s : +Lemma expr_sum {R : pzRingType} {T : Type} (x : R) (F : T -> nat) P s : x ^+ (\sum_(i <- s | P i) F i) = \prod_(i <- s | P i) x ^+ (F i). Proof. by apply: big_morph; [exact: exprD | exact: expr0]. Qed. @@ -265,14 +265,14 @@ Lemma prim_root_natf_neq0 (F : fieldType) n (w : F) : n.-primitive_root w -> (n%:R != 0 :> F). Proof. have [->//|n_gt0] := posnP n => x_prim; apply/negPf/negP => nFneq0. -have /natf0_char[//|p char_p] := nFneq0. -have p_prime : prime p := charf_prime char_p. -move: nFneq0; rewrite -(dvdn_charf char_p) => dvdpn. +have /natf0_pchar[//|p char_p] := nFneq0. +have p_prime : prime p := pcharf_prime char_p. +move: nFneq0; rewrite -(dvdn_pcharf char_p) => dvdpn. have [k cpk nE] := pfactor_coprime p_prime n_gt0. have k_gt0 : (k > 0)%N by move: n_gt0; rewrite nE muln_gt0 => /andP[]. have /prim_expr_order/eqP := x_prim; rewrite nE exprM. elim: (logn p n) => [|i IHi]; last first. - rewrite expnSr exprM -subr_eq0 -Frobenius_autE -(Frobenius_aut1 char_p). + rewrite expnSr exprM -subr_eq0 -pFrobenius_autE -(pFrobenius_aut1 char_p). by rewrite -rmorphB fmorph_eq0 subr_eq0. rewrite -(prim_order_dvd x_prim) nE mulnC Gauss_dvd ?coprimeXl//. rewrite pfactor_dvdn// ltn_geF// -[k]muln1 logn_Gauss ?logn1//. @@ -299,10 +299,10 @@ End ssrnum. (* ssrint *) (**********) -Lemma dvdz_charf (R : ringType) (p : nat) : - p \in [char R] -> forall n : int, (p %| n)%Z = (n%:~R == 0 :> R). +Lemma dvdz_charf (R : nzRingType) (p : nat) : + p \in [pchar R] -> forall n : int, (p %| n)%Z = (n%:~R == 0 :> R). Proof. -move=> charRp [] n; rewrite [LHS](dvdn_charf charRp)//. +move=> charRp [] n; rewrite [LHS](dvdn_pcharf charRp)//. by rewrite NegzE abszN rmorphN// oppr_eq0. Qed. @@ -316,38 +316,39 @@ Local Notation "p ^^ f" := (map_poly f p) Lemma irredp_XaddC (F : fieldType) (x : F) : irreducible_poly ('X + x%:P). Proof. by rewrite -[x]opprK rmorphN; apply: irredp_XsubC. Qed. -Lemma lead_coef_XnsubC {R : ringType} n (c : R) : (0 < n)%N -> +Lemma lead_coef_XnsubC {R : nzRingType} n (c : R) : (0 < n)%N -> lead_coef ('X^n - c%:P) = 1. Proof. move=> gt0_n; rewrite lead_coefDl ?lead_coefXn //. -by rewrite size_opp size_polyC size_polyXn ltnS (leq_trans (leq_b1 _)). +by rewrite size_polyN size_polyC size_polyXn ltnS (leq_trans (leq_b1 _)). Qed. -Lemma lead_coef_XsubC {R : ringType} (c : R) : - lead_coef ('X - c%:P) = 1. +Lemma lead_coef_XsubC {R : nzRingType} (c : R) : lead_coef ('X - c%:P) = 1. Proof. by apply: (@lead_coef_XnsubC _ 1%N). Qed. -Lemma monic_XsubC {R : ringType} (c : R) : 'X - c%:P \is monic. +Lemma monic_XsubC {R : nzRingType} (c : R) : 'X - c%:P \is monic. Proof. by rewrite monicE lead_coef_XsubC. Qed. -Lemma monic_XnsubC {R : ringType} n (c : R) : (0 < n)%N -> 'X^n - c%:P \is monic. +Lemma monic_XnsubC {R : nzRingType} n (c : R) : + (0 < n)%N -> 'X^n - c%:P \is monic. Proof. by move=> gt0_n; rewrite monicE lead_coef_XnsubC. Qed. -Lemma size_XnsubC {R : ringType} n (c : R) : (0 < n)%N -> size ('X^n - c%:P) = n.+1. +Lemma size_XnsubC {R : nzRingType} n (c : R) : + (0 < n)%N -> size ('X^n - c%:P) = n.+1. Proof. -move=> gt0_n; rewrite size_addl ?size_polyXn //. -by rewrite size_opp size_polyC; case: (c =P 0). +move=> gt0_n; rewrite size_polyDl ?size_polyXn //. +by rewrite size_polyN size_polyC; case: (c =P 0). Qed. -Lemma map_polyXsubC (aR rR : ringType) (f : {rmorphism aR -> rR}) x : +Lemma map_polyXsubC (aR rR : nzRingType) (f : {rmorphism aR -> rR}) x : map_poly f ('X - x%:P) = 'X - (f x)%:P. Proof. by rewrite rmorphB/= map_polyX map_polyC. Qed. -Lemma poly_XsubC_over {R : ringType} c (S : subringClosed R) : +Lemma poly_XsubC_over {R : nzRingType} c (S : subringClosed R) : c \in S -> 'X - c%:P \is a polyOver S. Proof. by move=> cS; rewrite rpredB ?polyOverC ?polyOverX. Qed. -Lemma poly_XnsubC_over {R : ringType} n c (S : subringClosed R) : +Lemma poly_XnsubC_over {R : nzRingType} n c (S : subringClosed R) : c \in S -> 'X^n - c%:P \is a polyOver S. Proof. by move=> cS; rewrite rpredB ?rpredX ?polyOverX ?polyOverC. Qed. @@ -363,24 +364,24 @@ rewrite lead_coef_prod big_seq (eq_bigr (fun=> 1)) ?big1 //=. by move=> i /mapP[c _ ->]; apply: lead_coef_XsubC. Qed. -Lemma coef0M {R : ringType} (p q : {poly R}) : (p * q)`_0 = p`_0 * q`_0. +Lemma coef0M {R : nzRingType} (p q : {poly R}) : (p * q)`_0 = p`_0 * q`_0. Proof. by rewrite coefM big_ord1. Qed. -Lemma coef0_prod {R : ringType} {T : Type} (ps : seq T) (F : T -> {poly R}) P : +Lemma coef0_prod {R : nzRingType} {T : Type} (ps : seq T) (F : T -> {poly R}) P : (\prod_(p <- ps | P p) F p)`_0 = \prod_(p <- ps | P p) (F p)`_0. Proof. by apply: (big_morph (fun p : {poly R} => p`_0)); [apply: coef0M | rewrite coefC eqxx]. Qed. -Lemma map_prod_XsubC (aR rR : ringType) (f : {rmorphism aR -> rR}) rs : +Lemma map_prod_XsubC (aR rR : nzRingType) (f : {rmorphism aR -> rR}) rs : map_poly f (\prod_(x <- rs) ('X - x%:P)) = \prod_(x <- map f rs) ('X - x%:P). Proof. by rewrite rmorph_prod big_map; apply/eq_bigr => x /=; rewrite map_polyXsubC. Qed. -Lemma eq_in_map_poly_id0 (aR rR : ringType) (f g : aR -> rR) +Lemma eq_in_map_poly_id0 (aR rR : nzRingType) (f g : aR -> rR) (S : addrClosed aR) : f 0 = 0 -> g 0 = 0 -> {in S, f =1 g} -> {in polyOver S, map_poly f =1 map_poly g}. @@ -389,12 +390,12 @@ move=> f0 g0 eq_fg p pP; apply/polyP => i. by rewrite !coef_map_id0// eq_fg// (polyOverP _). Qed. -Lemma eq_in_map_poly (aR rR : ringType) (f g : {additive aR -> rR}) +Lemma eq_in_map_poly (aR rR : nzRingType) (f g : {additive aR -> rR}) (S : addrClosed aR) : {in S, f =1 g} -> {in polyOver S, map_poly f =1 map_poly g}. Proof. by move=> /eq_in_map_poly_id0; apply; rewrite //?raddf0. Qed. -Lemma mapf_root (F : fieldType) (R : ringType) (f : {rmorphism F -> R}) +Lemma mapf_root (F : fieldType) (R : nzRingType) (f : {rmorphism F -> R}) (p : {poly F}) (x : F) : root (p ^^ f) (f x) = root p x. Proof. by rewrite !rootE horner_map fmorph_eq0. Qed. @@ -527,14 +528,14 @@ rewrite size_map_poly_id0 ?intr_eq0 ?lead_coef_eq0// in fN1. have [/eqP/size_poly1P[c cN0 ->]|gN1] := eqVneq (size g) 1%N. by rewrite mulrC mul_polyC map_polyZ/= eqp_sym eqp_scale// intr_eq0. have c_neq0 : (lead_coef q)%:~R != 0 :> 'F_p - by rewrite -(dvdz_charf (char_Fp _)). + by rewrite -(dvdz_charf (pchar_Fp _)). have : map_poly (intr : int -> 'F_p) q = (lead_coef q)%:~R *: 'X^((size q).-1). apply/val_inj/(@eq_from_nth _ 0) => [|i]; rewrite size_map_poly_id0//. by rewrite size_scale// size_polyXn -polySpred. move=> i_small; rewrite coef_poly i_small coefZ coefXn lead_coefE. move: i_small; rewrite polySpred// ltnS/=. case: ltngtP => // [i_lt|->]; rewrite (mulr1, mulr0)//= => _. - by apply/eqP; rewrite -(dvdz_charf (char_Fp _))// dvd_pq. + by apply/eqP; rewrite -(dvdz_charf (pchar_Fp _))// dvd_pq. rewrite [in LHS]q_eq rmorphM/=. set c := (X in X *: _); set n := (_.-1). set pf := map_poly _ f; set pg := map_poly _ g => pfMpg. @@ -553,7 +554,7 @@ have pfN1 : size pf != 1%N by rewrite size_map_poly_id0. have pgN1 : size pg != 1%N by rewrite size_map_poly_id0. have /(dvdXn _ pgN1) /eqP : pg %| c *: 'X^n by rewrite -pfMpg dvdp_mull. have /(dvdXn _ pfN1) /eqP : pf %| c *: 'X^n by rewrite -pfMpg dvdp_mulr. -by rewrite !coef_map// -!(dvdz_charf (char_Fp _))//; apply: dvdz_mul. +by rewrite !coef_map// -!(dvdz_charf (pchar_Fp _))//; apply: dvdz_mul. Qed. (***********)