From 0478ef3553f8e82358a5537aba34031d4120c20e Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Mon, 3 Feb 2025 10:57:48 +0100 Subject: [PATCH] [CI] Readd coqeal Now that it compiles on Coq >= 9 thanks to the replacement of paramcoq by elpi derive.param2. --- .github/workflows/nix-action-coq-8.20.yml | 81 +++++++++++++ .github/workflows/nix-action-coq-master.yml | 73 ++++++++++++ .github/workflows/nix-action-rocq-9.0.yml | 77 ++++++++++++ .nix/config.nix | 1 - .nix/coq-overlays/coqeal/default.nix | 124 ++++++++++++++++++++ 5 files changed, 355 insertions(+), 1 deletion(-) create mode 100644 .nix/coq-overlays/coqeal/default.nix diff --git a/.github/workflows/nix-action-coq-8.20.yml b/.github/workflows/nix-action-coq-8.20.yml index 5a78557e4..317d43e0f 100644 --- a/.github/workflows/nix-action-coq-8.20.yml +++ b/.github/workflows/nix-action-coq-8.20.yml @@ -248,6 +248,87 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20" --argstr job "coq-elpi" + coqeal: + needs: + - coq + - mathcomp-algebra + - multinomials + - 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 coq-elpi + uses: cachix/cachix-action@v15 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepGetDerivation + name: Getting derivation for current job (coqeal) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"coq-8.20\" --argstr job \"coqeal\" \\\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-8.20" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-algebra' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20" + --argstr job "mathcomp-algebra" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: bignums' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20" + --argstr 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 "coq-8.20" + --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 "coq-8.20" + --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 "coq-8.20" + --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-8.20" + --argstr job "coqeal" coquelicot: needs: - coq diff --git a/.github/workflows/nix-action-coq-master.yml b/.github/workflows/nix-action-coq-master.yml index 1e7639b1e..47db9aa26 100644 --- a/.github/workflows/nix-action-coq-master.yml +++ b/.github/workflows/nix-action-coq-master.yml @@ -115,6 +115,79 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" --argstr job "coq-elpi" + coqeal: + needs: + - coq + - mathcomp-algebra + - multinomials + - 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 coq-elpi + uses: cachix/cachix-action@v15 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepGetDerivation + name: Getting derivation for current job (coqeal) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"coq-master\" --argstr job \"coqeal\" \\\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-master" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-algebra' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" + --argstr job "mathcomp-algebra" + - 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 "coq-master" + --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 "coq-master" + --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-master" + --argstr job "coqeal" hierarchy-builder: needs: - coq diff --git a/.github/workflows/nix-action-rocq-9.0.yml b/.github/workflows/nix-action-rocq-9.0.yml index b1a8777df..e8806b78f 100644 --- a/.github/workflows/nix-action-rocq-9.0.yml +++ b/.github/workflows/nix-action-rocq-9.0.yml @@ -248,6 +248,83 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" --argstr job "coq-elpi" + coqeal: + needs: + - coq + - mathcomp-algebra + - multinomials + - 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 coq-elpi + uses: cachix/cachix-action@v15 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community, math-comp + name: coq-elpi + - id: stepGetDerivation + name: Getting derivation for current job (coqeal) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"rocq-9.0\" --argstr job \"coqeal\" \\\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 "rocq-9.0" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-algebra' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" + --argstr job "mathcomp-algebra" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: bignums' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" + --argstr job "bignums" + - 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 "rocq-9.0" + --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 "rocq-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 "rocq-9.0" + --argstr job "coqeal" hierarchy-builder: needs: - coq diff --git a/.nix/config.nix b/.nix/config.nix index 0cc210669..ec2a0d172 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -17,7 +17,6 @@ let master = [ mathcomp-single-planB-src.job = false; mathcomp-single-planB.job = false; mathcomp-single.job = false; - coqeal.job = false; # broken in master, c.f. https://github.com/coq/coq/pull/19228 deriving.job = false; reglang.job = false; diff --git a/.nix/coq-overlays/coqeal/default.nix b/.nix/coq-overlays/coqeal/default.nix new file mode 100644 index 000000000..d748b956c --- /dev/null +++ b/.nix/coq-overlays/coqeal/default.nix @@ -0,0 +1,124 @@ +{ + coq, + mkCoqDerivation, + mathcomp, + bignums, + paramcoq, + multinomials, + mathcomp-real-closed, + lib, + version ? null, +}: + +let +derivation = mkCoqDerivation { + + pname = "CoqEAL"; + + inherit version; + defaultVersion = + with lib.versions; + lib.switch + [ coq.version mathcomp.version ] + [ + { + cases = [ + (range "8.16" "8.20") + (isGe "2.1.0") + ]; + out = "2.0.3"; + } + { + cases = [ + (range "8.16" "8.20") + (isGe "2.0.0") + ]; + out = "2.0.1"; + } + { + cases = [ + (range "8.16" "8.17") + (isGe "2.0.0") + ]; + out = "2.0.0"; + } + { + cases = [ + (range "8.15" "8.18") + (range "1.15.0" "1.18.0") + ]; + out = "1.1.3"; + } + { + cases = [ + (range "8.13" "8.17") + (range "1.13.0" "1.18.0") + ]; + out = "1.1.1"; + } + { + cases = [ + (range "8.10" "8.15") + (range "1.12.0" "1.18.0") + ]; + out = "1.1.0"; + } + { + cases = [ + (isGe "8.10") + (range "1.11.0" "1.12.0") + ]; + out = "1.0.5"; + } + { + cases = [ + (isGe "8.7") + "1.11.0" + ]; + out = "1.0.4"; + } + { + cases = [ + (isGe "8.7") + "1.10.0" + ]; + out = "1.0.3"; + } + ] + null; + + release."2.0.3".sha256 = "sha256-5lDq7IWlEW0EkNzYPu+dA6KOvRgy53W/alikpDr/Kd0="; + release."2.0.1".sha256 = "sha256-d/IQ4IdS2tpyPewcGobj2S6m2HU+iXQmlvR+ITNIcjI="; + release."2.0.0".sha256 = "sha256-SG/KVnRJz2P+ZxkWVp1dDOnc/JVgigoexKfRUh1Y0GM"; + release."1.1.3".sha256 = "sha256-xhqWpg86xbU1GbDtXXInNCTArjjPnWZctWiiasq1ScU="; + release."1.1.1".sha256 = "sha256-ExAdC3WuArNxS+Sa1r4x5aT7ylbCvP/BZXfkdQNAvZ8="; + release."1.1.0".sha256 = "1vyhfna5frkkq2fl1fkg2mwzpg09k3sbzxxpyp14fjay81xajrxr"; + release."1.0.6".sha256 = "0lqkyfj4qbq8wr3yk8qgn7mclw582n3fjl9l19yp8cnchspzywx0"; + release."1.0.5".sha256 = "0cmvky8glb5z2dy3q62aln6qbav4lrf2q1589f6h1gn5bgjrbzkm"; + release."1.0.4".sha256 = "1g5m26lr2lwxh6ld2gykailhay4d0ayql4bfh0aiwqpmmczmxipk"; + release."1.0.3".sha256 = "0hc63ny7phzbihy8l7wxjvn3haxx8jfnhi91iw8hkq8n29i23v24"; + + propagatedBuildInputs = [ + mathcomp.algebra + bignums + multinomials + ]; + + meta = { + description = "CoqEAL - The Coq Effective Algebra Library"; + license = lib.licenses.mit; + }; +}; +patched-derivation1 = derivation.overrideAttrs + (o: { + propagatedBuildInputs = + o.propagatedBuildInputs + ++ lib.optional (lib.versions.isGe "1.1" o.version || o.version == "dev") mathcomp-real-closed; + }); +patched-derivation = patched-derivation1.overrideAttrs + (o: { + propagatedBuildInputs = + o.propagatedBuildInputs + ++ lib.optional (lib.versions.isLe "2.0.3" o.version && o.version != "dev") paramcoq; + }); +in patched-derivation