From 469585a4563ee50be27306d2a6693933010d18e8 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Mon, 28 Aug 2023 15:37:24 +0200 Subject: [PATCH] Update CI --- .github/workflows/docker-action.yml | 20 +-- .github/workflows/nix-action-8.16.yml | 173 ++++++++++++++++++++++-- .github/workflows/nix-action-8.17.yml | 95 +++++++++++-- .github/workflows/nix-action-master.yml | 37 +++-- .nix/config.nix | 6 +- .nix/coq-nix-toolbox.nix | 2 +- .nix/coq-overlays/mathcomp/default.nix | 122 ----------------- 7 files changed, 264 insertions(+), 191 deletions(-) delete mode 100644 .nix/coq-overlays/mathcomp/default.nix diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index d180462..279e845 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -17,24 +17,8 @@ jobs: strategy: matrix: image: - - 'mathcomp/mathcomp:1.13.0-coq-8.13' - - 'mathcomp/mathcomp:1.13.0-coq-8.14' - - 'mathcomp/mathcomp:1.13.0-coq-8.15' - - 'mathcomp/mathcomp:1.14.0-coq-8.13' - - 'mathcomp/mathcomp:1.14.0-coq-8.14' - - 'mathcomp/mathcomp:1.14.0-coq-8.15' - - 'mathcomp/mathcomp:1.15.0-coq-8.13' - - 'mathcomp/mathcomp:1.15.0-coq-8.14' - - 'mathcomp/mathcomp:1.15.0-coq-8.15' - - 'mathcomp/mathcomp:1.15.0-coq-8.16' - - 'mathcomp/mathcomp:1.16.0-coq-8.13' - - 'mathcomp/mathcomp:1.16.0-coq-8.14' - - 'mathcomp/mathcomp:1.16.0-coq-8.15' - - 'mathcomp/mathcomp:1.16.0-coq-8.16' - - 'mathcomp/mathcomp:1.16.0-coq-8.17' - - 'mathcomp/mathcomp-dev:coq-8.13' - - 'mathcomp/mathcomp-dev:coq-8.14' - - 'mathcomp/mathcomp-dev:coq-8.15' + - 'mathcomp/mathcomp:2.0.0-coq-8.16' + - 'mathcomp/mathcomp:2.0.0-coq-8.17' - 'mathcomp/mathcomp-dev:coq-8.16' - 'mathcomp/mathcomp-dev:coq-8.17' - 'mathcomp/mathcomp-dev:coq-dev' diff --git a/.github/workflows/nix-action-8.16.yml b/.github/workflows/nix-action-8.16.yml index bf392e0..593e0be 100644 --- a/.github/workflows/nix-action-8.16.yml +++ b/.github/workflows/nix-action-8.16.yml @@ -40,15 +40,16 @@ jobs: name: Checking presence of CI target coq run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"8.16\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\")\n" + echo $nb_dry_run\necho name=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 "8.16" --argstr job "coq" - mathcomp: + coqeal: needs: - coq + - mathcomp-real-closed runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -85,23 +86,87 @@ jobs: extraPullNames: coq, coq-community name: math-comp - id: stepCheck - name: Checking presence of CI target mathcomp + name: Checking presence of CI target coqeal run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.16\" --argstr job \"mathcomp\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\")\n" + \ bundle \"8.16\" --argstr job \"coqeal\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho name=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 "8.16" --argstr job "coq" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq-elpi' + name: 'Building/fetching previous CI target: mathcomp-algebra' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr - job "coq-elpi" + job "mathcomp-algebra" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: hierarchy-builder' + name: 'Building/fetching previous CI target: bignums' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr - job "hierarchy-builder" + job "bignums" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: paramcoq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr + job "paramcoq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: multinomials' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr + job "multinomials" + - 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 "8.16" --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 "8.16" --argstr + job "coqeal" + mathcomp: + needs: + - coq + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@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@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target mathcomp + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"8.16\" --argstr job \"mathcomp\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho name=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 "8.16" --argstr + job "coq" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-ssreflect' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr @@ -126,10 +191,92 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-character' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr job "mathcomp-character" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: hierarchy-builder' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr + job "hierarchy-builder" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr job "mathcomp" + mathcomp-apery: + needs: + - coq + - coqeal + - 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@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target mathcomp-apery + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"8.16\" --argstr job \"mathcomp-apery\" \\\n --dry-run 2>&1 >\ + \ /dev/null)\necho $nb_dry_run\necho name=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 "8.16" --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 "8.16" --argstr + job "mathcomp-field" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coqeal' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr + job "coqeal" + - 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 "8.16" --argstr + job "mathcomp-real-closed" + - 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 "8.16" --argstr + job "mathcomp-bigenough" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-zify' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr + job "mathcomp-zify" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-algebra-tactics' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr + job "mathcomp-algebra-tactics" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.16" --argstr + job "mathcomp-apery" mathcomp-real-closed: needs: - coq @@ -172,8 +319,8 @@ jobs: 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 \"8.16\" --argstr job \"mathcomp-real-closed\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ - \ | grep \"built:\" | sed \"s/.*/built/\")\n" + \ > /dev/null)\necho $nb_dry_run\necho name=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 "8.16" --argstr diff --git a/.github/workflows/nix-action-8.17.yml b/.github/workflows/nix-action-8.17.yml index 21450ec..8ce7671 100644 --- a/.github/workflows/nix-action-8.17.yml +++ b/.github/workflows/nix-action-8.17.yml @@ -40,15 +40,16 @@ jobs: name: Checking presence of CI target coq run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"8.17\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\")\n" + echo $nb_dry_run\necho name=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 "8.17" --argstr job "coq" - mathcomp: + coqeal: needs: - coq + - mathcomp-real-closed runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -85,23 +86,87 @@ jobs: extraPullNames: coq, coq-community name: math-comp - id: stepCheck - name: Checking presence of CI target mathcomp + name: Checking presence of CI target coqeal run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.17\" --argstr job \"mathcomp\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\")\n" + \ bundle \"8.17\" --argstr job \"coqeal\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho name=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 "8.17" --argstr job "coq" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq-elpi' + name: 'Building/fetching previous CI target: mathcomp-algebra' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr - job "coq-elpi" + job "mathcomp-algebra" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: hierarchy-builder' + name: 'Building/fetching previous CI target: bignums' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr - job "hierarchy-builder" + job "bignums" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: paramcoq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr + job "paramcoq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: multinomials' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr + job "multinomials" + - 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 "8.17" --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 "8.17" --argstr + job "coqeal" + mathcomp: + needs: + - coq + runs-on: ubuntu-latest + steps: + - name: Determine which commit to initially checkout + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\ + \ }}\" >> $GITHUB_ENV\nfi\n" + - name: Git checkout + uses: actions/checkout@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@v20 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v12 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target mathcomp + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"8.17\" --argstr job \"mathcomp\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho name=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 "8.17" --argstr + job "coq" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-ssreflect' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr @@ -126,6 +191,10 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-character' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr job "mathcomp-character" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: hierarchy-builder' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr + job "hierarchy-builder" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.17" --argstr @@ -172,8 +241,8 @@ jobs: 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 \"8.17\" --argstr job \"mathcomp-real-closed\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ - \ | grep \"built:\" | sed \"s/.*/built/\")\n" + \ > /dev/null)\necho $nb_dry_run\necho name=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 "8.17" --argstr diff --git a/.github/workflows/nix-action-master.yml b/.github/workflows/nix-action-master.yml index 5dd573b..1d41e5e 100644 --- a/.github/workflows/nix-action-master.yml +++ b/.github/workflows/nix-action-master.yml @@ -40,8 +40,8 @@ jobs: name: Checking presence of CI target coq run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"master\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\")\n" + echo $nb_dry_run\necho name=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 "master" @@ -88,8 +88,8 @@ jobs: name: Checking presence of CI target coq-elpi run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"master\" --argstr job \"coq-elpi\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\")\n" + echo $nb_dry_run\necho name=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 "master" @@ -141,8 +141,8 @@ jobs: name: Checking presence of CI target hierarchy-builder run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"master\" --argstr job \"hierarchy-builder\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ - \ | grep \"built:\" | sed \"s/.*/built/\")\n" + \ > /dev/null)\necho $nb_dry_run\necho name=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 "master" @@ -158,7 +158,6 @@ jobs: mathcomp: needs: - coq - - coq-elpi - hierarchy-builder runs-on: ubuntu-latest steps: @@ -199,20 +198,12 @@ jobs: name: Checking presence of CI target mathcomp run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"master\" --argstr job \"mathcomp\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\")\n" + echo $nb_dry_run\necho name=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 "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 "master" - --argstr job "coq-elpi" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: hierarchy-builder' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" - --argstr job "hierarchy-builder" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-ssreflect' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" @@ -237,6 +228,10 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-character' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" --argstr job "mathcomp-character" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: hierarchy-builder' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "hierarchy-builder" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" @@ -283,8 +278,8 @@ jobs: name: Checking presence of CI target mathcomp-bigenough run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ \ bundle \"master\" --argstr job \"mathcomp-bigenough\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ - \ | grep \"built:\" | sed \"s/.*/built/\")\n" + \ > /dev/null)\necho $nb_dry_run\necho name=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 "master" @@ -340,8 +335,8 @@ jobs: 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 \"master\" --argstr job \"mathcomp-real-closed\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho name=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 "master" diff --git a/.nix/config.nix b/.nix/config.nix index f59a089..f2b2c96 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -39,16 +39,16 @@ ## will be created per bundle bundles."8.16".coqPackages = { coq.override.version = "8.16"; - mathcomp.override.version = "mathcomp-2.0.0"; + mathcomp.override.version = "2.0.0"; }; bundles."8.17".coqPackages = { coq.override.version = "8.17"; - mathcomp.override.version = "mathcomp-2.0.0"; + mathcomp.override.version = "2.0.0"; }; bundles."master".coqPackages = { coq.override.version = "master"; coq-elpi.override.version = "coq-master"; - hierarchy-builder.override.version = "proux01:coq-master"; + hierarchy-builder.override.version = "coq-master"; mathcomp.override.version = "master"; mathcomp-bigenough.override.version = "1.0.1"; }; diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index 3836be9..a12748c 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"8893994e8efdbbf72ec4e3eaf84ea676b77ef38f" +"575258fdeb76c712740f30f23ccf5ed1918c2332" diff --git a/.nix/coq-overlays/mathcomp/default.nix b/.nix/coq-overlays/mathcomp/default.nix deleted file mode 100644 index dbaf587..0000000 --- a/.nix/coq-overlays/mathcomp/default.nix +++ /dev/null @@ -1,122 +0,0 @@ -############################################################################ -# This file mainly provides the `mathcomp` derivation, which is # -# essentially a meta-package containing all core mathcomp libraries # -# (ssreflect fingroup algebra solvable field character). They can be # -# accessed individually through the passthrough attributes of mathcomp # -# bearing the same names (mathcomp.ssreflect, etc). # -############################################################################ -# Compiling a custom version of mathcomp using `mathcomp.override`. # -# This is the replacement for the former `mathcomp_ config` function. # -# See the documentation at doc/languages-frameworks/coq.section.md. # -############################################################################ - -{ lib, ncurses, graphviz, lua, fetchzip, - coq-elpi, hierarchy-builder, - mkCoqDerivation, recurseIntoAttrs, withDoc ? false, single ? false, - coqPackages, coq, version ? null }@args: -with builtins // lib; -let - repo = "math-comp"; - owner = "math-comp"; - withDoc = single && (args.withDoc or false); - defaultVersion = with versions; switch coq.coq-version [ - { case = isGe "8.11"; out = "1.14.0"; } - { case = range "8.11" "8.15"; out = "1.13.0"; } - { case = range "8.10" "8.13"; out = "1.12.0"; } - { case = range "8.7" "8.12"; out = "1.11.0"; } - { case = range "8.7" "8.11"; out = "1.10.0"; } - { case = range "8.7" "8.11"; out = "1.9.0"; } - { case = range "8.7" "8.9"; out = "1.8.0"; } - { case = range "8.6" "8.9"; out = "1.7.0"; } - { case = range "8.5" "8.7"; out = "1.6.4"; } - ] null; - release = { - "1.14.0".sha256 = "07yamlp1c0g5nahkd2gpfhammcca74ga2s6qr7a3wm6y6j5pivk9"; - "1.13.0".sha256 = "0j4cz2y1r1aw79snkcf1pmicgzf8swbaf9ippz0vg99a572zqzri"; - "1.12.0".sha256 = "1ccfny1vwgmdl91kz5xlmhq4wz078xm4z5wpd0jy5rn890dx03wp"; - "1.11.0".sha256 = "06a71d196wd5k4wg7khwqb7j7ifr7garhwkd54s86i0j7d6nhl3c"; - "1.10.0".sha256 = "1b9m6pwxxyivw7rgx82gn5kmgv2mfv3h3y0mmjcjfypi8ydkrlbv"; - "1.9.0".sha256 = "0lid9zaazdi3d38l8042lczb02pw5m9wq0yysiilx891hgq2p81r"; - "1.8.0".sha256 = "07l40is389ih8bi525gpqs3qp4yb2kl11r9c8ynk1ifpjzpnabwp"; - "1.7.0".sha256 = "0wnhj9nqpx2bw6n1l4i8jgrw3pjajvckvj3lr4vzjb3my2lbxdd1"; - "1.6.4".sha256 = "09ww48qbjsvpjmy1g9yhm0rrkq800ffq21p6fjkbwd34qvd82raz"; - "1.6.1".sha256 = "1ilw6vm4dlsdv9cd7kmf0vfrh2kkzr45wrqr8m37miy0byzr4p9i"; - }; - releaseRev = v: "mathcomp-${v}"; - - # list of core mathcomp packages sorted by dependency order - packages = [ "ssreflect" "fingroup" "algebra" "solvable" "field" "character" "all" ]; - - mathcomp_ = package: let - mathcomp-deps = if package == "single" then [] - else map mathcomp_ (head (splitList (pred.equal package) packages)); - pkgpath = if package == "single" then "mathcomp" else "mathcomp/${package}"; - pname = if package == "single" then "mathcomp" else "mathcomp-${package}"; - pkgallMake = '' - echo "all.v" > Make - echo "-I ." >> Make - echo "-R . mathcomp.all" >> Make - ''; - derivation = mkCoqDerivation ({ - inherit version pname defaultVersion release releaseRev repo owner; - - mlPlugin = versions.isLe "8.6" coq.coq-version; - nativeBuildInputs = optionals withDoc [ graphviz lua ]; - buildInputs = [ ncurses ]; - propagatedBuildInputs = [ coq-elpi hierarchy-builder ] ++ mathcomp-deps; - - buildFlags = optional withDoc "doc"; - - preBuild = '' - if [[ -f etc/utils/ssrcoqdep ]] - then patchShebangs etc/utils/ssrcoqdep - fi - if [[ -f etc/buildlibgraph ]] - then patchShebangs etc/buildlibgraph - fi - '' + '' - cd ${pkgpath} - '' + optionalString (package == "all") pkgallMake; - - meta = { - homepage = "https://math-comp.github.io/"; - license = licenses.cecill-b; - maintainers = with maintainers; [ vbgl jwiegley cohencyril ]; - }; - } // optionalAttrs (package != "single") - { passthru = genAttrs packages mathcomp_; } - // optionalAttrs withDoc { - htmldoc_template = - fetchzip { - url = "https://github.com/math-comp/math-comp.github.io/archive/doc-1.12.0.zip"; - sha256 = "0y1352ha2yy6k2dl375sb1r68r1qi9dyyy7dyzj5lp9hxhhq69x8"; - }; - postBuild = '' - cp -rf _build_doc/* . - rm -r _build_doc - ''; - postInstall = - let tgt = "$out/share/coq/${coq.coq-version}/"; in - optionalString withDoc '' - mkdir -p ${tgt} - cp -r htmldoc ${tgt} - cp -r $htmldoc_template/htmldoc_template/* ${tgt}/htmldoc/ - ''; - buildTargets = "doc"; - extraInstallFlags = [ "-f Makefile.coq" ]; - }); - patched-derivation1 = derivation.overrideAttrs (o: - optionalAttrs (o.pname != null && o.pname == "mathcomp-all" && - o.version != null && o.version != "dev" && versions.isLt "1.7" o.version) - { preBuild = ""; buildPhase = ""; installPhase = "echo doing nothing"; } - ); - patched-derivation = patched-derivation1.overrideAttrs (o: - optionalAttrs (versions.isLe "8.7" coq.coq-version || - (o.version != "dev" && versions.isLe "1.7" o.version)) - { - installFlags = o.installFlags ++ [ "-f Makefile.coq" ]; - } - ); - in patched-derivation; -in -mathcomp_ (if single then "single" else "all")