From 577fa143eaeb30f1b956f6402843bf7d94b4cc60 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Tue, 25 Feb 2025 13:39:21 +0100 Subject: [PATCH] [CI] Update Nix toolbox --- .github/workflows/nix-action-coq-8.20.yml | 201 +++++++++++++++--- .github/workflows/nix-action-coq-master.yml | 45 +--- .github/workflows/nix-action-rocq-9.0.yml | 118 +++++++--- .nix/config.nix | 22 +- .nix/coq-nix-toolbox.nix | 2 +- .nix/coq-overlays/coq-elpi/default.nix | 123 ----------- .../hierarchy-builder/default.nix | 51 ----- 7 files changed, 277 insertions(+), 285 deletions(-) delete mode 100644 .nix/coq-overlays/coq-elpi/default.nix delete mode 100644 .nix/coq-overlays/hierarchy-builder/default.nix diff --git a/.github/workflows/nix-action-coq-8.20.yml b/.github/workflows/nix-action-coq-8.20.yml index a7dd61e26..3be6dd224 100644 --- a/.github/workflows/nix-action-coq-8.20.yml +++ b/.github/workflows/nix-action-coq-8.20.yml @@ -74,6 +74,7 @@ jobs: needs: - coq - mathcomp-ssreflect + - stdlib runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -129,6 +130,10 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-ssreflect' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20" --argstr job "mathcomp-ssreflect" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: stdlib' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20" + --argstr job "stdlib" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20" @@ -382,6 +387,7 @@ jobs: coquelicot: needs: - coq + - stdlib - mathcomp-ssreflect runs-on: ubuntu-latest steps: @@ -434,6 +440,10 @@ jobs: 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: stdlib' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20" + --argstr job "stdlib" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-ssreflect' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20" @@ -442,6 +452,77 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20" --argstr job "coquelicot" + corn: + 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 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 (corn) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"coq-8.20\" --argstr job \"corn\" \\\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: 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: math-classes' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20" + --argstr job "math-classes" + - 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-8.20" + --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 "coq-8.20" + --argstr job "corn" hierarchy-builder: needs: - coq @@ -589,7 +670,6 @@ jobs: mathcomp: needs: - coq - - stdlib - mathcomp-ssreflect - mathcomp-fingroup - mathcomp-algebra @@ -648,10 +728,6 @@ jobs: 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: stdlib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20" - --argstr job "stdlib" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-ssreflect' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20" @@ -687,7 +763,6 @@ jobs: mathcomp-algebra: needs: - coq - - stdlib - mathcomp-ssreflect - mathcomp-fingroup - hierarchy-builder @@ -742,10 +817,6 @@ jobs: 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: stdlib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20" - --argstr job "stdlib" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-ssreflect' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20" @@ -845,6 +916,7 @@ jobs: - coq - mathcomp-analysis - mathcomp-reals-stdlib + - stdlib - hierarchy-builder runs-on: ubuntu-latest steps: @@ -905,6 +977,10 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-reals-stdlib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20" --argstr job "mathcomp-reals-stdlib" + - 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-8.20" + --argstr job "stdlib" - 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 "coq-8.20" @@ -979,7 +1055,6 @@ jobs: mathcomp-character: needs: - coq - - stdlib - mathcomp-ssreflect - mathcomp-fingroup - mathcomp-algebra @@ -1037,10 +1112,6 @@ jobs: 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: stdlib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20" - --argstr job "stdlib" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-ssreflect' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20" @@ -1218,7 +1289,6 @@ jobs: mathcomp-field: needs: - coq - - stdlib - mathcomp-ssreflect - mathcomp-fingroup - mathcomp-algebra @@ -1275,10 +1345,6 @@ jobs: 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: stdlib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20" - --argstr job "stdlib" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-ssreflect' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20" @@ -1306,7 +1372,6 @@ jobs: mathcomp-fingroup: needs: - coq - - stdlib - mathcomp-ssreflect - hierarchy-builder runs-on: ubuntu-latest @@ -1360,10 +1425,6 @@ jobs: 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: stdlib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20" - --argstr job "stdlib" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-ssreflect' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20" @@ -1599,6 +1660,7 @@ jobs: needs: - coq - mathcomp-reals + - stdlib - hierarchy-builder runs-on: ubuntu-latest steps: @@ -1655,6 +1717,10 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-reals' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20" --argstr job "mathcomp-reals" + - 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-8.20" + --argstr job "stdlib" - 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 "coq-8.20" @@ -1666,7 +1732,6 @@ jobs: mathcomp-solvable: needs: - coq - - stdlib - mathcomp-ssreflect - mathcomp-fingroup - mathcomp-algebra @@ -1722,10 +1787,6 @@ jobs: 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: stdlib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20" - --argstr job "stdlib" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-ssreflect' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20" @@ -1749,7 +1810,6 @@ jobs: mathcomp-ssreflect: needs: - coq - - stdlib - hierarchy-builder runs-on: ubuntu-latest steps: @@ -1802,10 +1862,6 @@ jobs: 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: stdlib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20" - --argstr job "stdlib" - 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 "coq-8.20" @@ -2115,6 +2171,81 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20" --argstr job "stdlib" + vcfloat: + needs: + - coq + - interval + 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 (vcfloat) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"coq-8.20\" --argstr job \"vcfloat\" \\\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: interval' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20" + --argstr job "interval" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: compcert' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20" + --argstr job "compcert" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: flocq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20" + --argstr job "flocq" + - 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 current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20" + --argstr job "vcfloat" name: Nix CI for bundle coq-8.20 on: pull_request: diff --git a/.github/workflows/nix-action-coq-master.yml b/.github/workflows/nix-action-coq-master.yml index 6fe5ad316..25f48b8e6 100644 --- a/.github/workflows/nix-action-coq-master.yml +++ b/.github/workflows/nix-action-coq-master.yml @@ -438,7 +438,6 @@ jobs: mathcomp: needs: - coq - - stdlib - mathcomp-ssreflect - mathcomp-fingroup - mathcomp-algebra @@ -497,10 +496,6 @@ jobs: 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' name: 'Building/fetching previous CI target: mathcomp-ssreflect' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" @@ -536,7 +531,6 @@ jobs: mathcomp-algebra: needs: - coq - - stdlib - mathcomp-ssreflect - mathcomp-fingroup - hierarchy-builder @@ -591,10 +585,6 @@ jobs: 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' name: 'Building/fetching previous CI target: mathcomp-ssreflect' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" @@ -694,6 +684,7 @@ jobs: - coq - mathcomp-analysis - mathcomp-reals-stdlib + - stdlib - hierarchy-builder runs-on: ubuntu-latest steps: @@ -754,6 +745,10 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-reals-stdlib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" --argstr job "mathcomp-reals-stdlib" + - 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' name: 'Building/fetching previous CI target: hierarchy-builder' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" @@ -828,7 +823,6 @@ jobs: mathcomp-character: needs: - coq - - stdlib - mathcomp-ssreflect - mathcomp-fingroup - mathcomp-algebra @@ -886,10 +880,6 @@ jobs: 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' name: 'Building/fetching previous CI target: mathcomp-ssreflect' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" @@ -1067,7 +1057,6 @@ jobs: mathcomp-field: needs: - coq - - stdlib - mathcomp-ssreflect - mathcomp-fingroup - mathcomp-algebra @@ -1124,10 +1113,6 @@ jobs: 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' name: 'Building/fetching previous CI target: mathcomp-ssreflect' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" @@ -1155,7 +1140,6 @@ jobs: mathcomp-fingroup: needs: - coq - - stdlib - mathcomp-ssreflect - hierarchy-builder runs-on: ubuntu-latest @@ -1209,10 +1193,6 @@ jobs: 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' name: 'Building/fetching previous CI target: mathcomp-ssreflect' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" @@ -1448,6 +1428,7 @@ jobs: needs: - coq - mathcomp-reals + - stdlib - hierarchy-builder runs-on: ubuntu-latest steps: @@ -1504,6 +1485,10 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-reals' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" --argstr job "mathcomp-reals" + - 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' name: 'Building/fetching previous CI target: hierarchy-builder' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" @@ -1515,7 +1500,6 @@ jobs: mathcomp-solvable: needs: - coq - - stdlib - mathcomp-ssreflect - mathcomp-fingroup - mathcomp-algebra @@ -1571,10 +1555,6 @@ jobs: 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' name: 'Building/fetching previous CI target: mathcomp-ssreflect' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" @@ -1598,7 +1578,6 @@ jobs: mathcomp-ssreflect: needs: - coq - - stdlib - hierarchy-builder runs-on: ubuntu-latest steps: @@ -1651,10 +1630,6 @@ jobs: 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' name: 'Building/fetching previous CI target: hierarchy-builder' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" diff --git a/.github/workflows/nix-action-rocq-9.0.yml b/.github/workflows/nix-action-rocq-9.0.yml index b097485af..3583703ba 100644 --- a/.github/workflows/nix-action-rocq-9.0.yml +++ b/.github/workflows/nix-action-rocq-9.0.yml @@ -74,6 +74,7 @@ jobs: needs: - coq - mathcomp-ssreflect + - stdlib runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -129,6 +130,10 @@ jobs: 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 == 'built' + name: 'Building/fetching previous CI target: stdlib' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-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 "rocq-9.0" @@ -442,6 +447,74 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" --argstr job "coqeal" + coquelicot: + needs: + - coq + - stdlib + - mathcomp-ssreflect + 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 (coquelicot) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"rocq-9.0\" --argstr job \"coquelicot\" \\\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: stdlib' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" + --argstr job "stdlib" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-ssreflect' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-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 "rocq-9.0" + --argstr job "coquelicot" hierarchy-builder: needs: - coq @@ -508,7 +581,6 @@ jobs: mathcomp: needs: - coq - - stdlib - mathcomp-ssreflect - mathcomp-fingroup - mathcomp-algebra @@ -567,10 +639,6 @@ jobs: 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: stdlib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" - --argstr job "stdlib" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-ssreflect' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" @@ -606,7 +674,6 @@ jobs: mathcomp-algebra: needs: - coq - - stdlib - mathcomp-ssreflect - mathcomp-fingroup - hierarchy-builder @@ -661,10 +728,6 @@ jobs: 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: stdlib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" - --argstr job "stdlib" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-ssreflect' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" @@ -764,6 +827,7 @@ jobs: - coq - mathcomp-analysis - mathcomp-reals-stdlib + - stdlib - hierarchy-builder runs-on: ubuntu-latest steps: @@ -824,6 +888,10 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-reals-stdlib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" --argstr job "mathcomp-reals-stdlib" + - 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 "rocq-9.0" + --argstr job "stdlib" - 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 "rocq-9.0" @@ -898,7 +966,6 @@ jobs: mathcomp-character: needs: - coq - - stdlib - mathcomp-ssreflect - mathcomp-fingroup - mathcomp-algebra @@ -956,10 +1023,6 @@ jobs: 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: stdlib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" - --argstr job "stdlib" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-ssreflect' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" @@ -1137,7 +1200,6 @@ jobs: mathcomp-field: needs: - coq - - stdlib - mathcomp-ssreflect - mathcomp-fingroup - mathcomp-algebra @@ -1194,10 +1256,6 @@ jobs: 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: stdlib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" - --argstr job "stdlib" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-ssreflect' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" @@ -1225,7 +1283,6 @@ jobs: mathcomp-fingroup: needs: - coq - - stdlib - mathcomp-ssreflect - hierarchy-builder runs-on: ubuntu-latest @@ -1279,10 +1336,6 @@ jobs: 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: stdlib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" - --argstr job "stdlib" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-ssreflect' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" @@ -1518,6 +1571,7 @@ jobs: needs: - coq - mathcomp-reals + - stdlib - hierarchy-builder runs-on: ubuntu-latest steps: @@ -1574,6 +1628,10 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-reals' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" --argstr job "mathcomp-reals" + - 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 "rocq-9.0" + --argstr job "stdlib" - 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 "rocq-9.0" @@ -1585,7 +1643,6 @@ jobs: mathcomp-solvable: needs: - coq - - stdlib - mathcomp-ssreflect - mathcomp-fingroup - mathcomp-algebra @@ -1641,10 +1698,6 @@ jobs: 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: stdlib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" - --argstr job "stdlib" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-ssreflect' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" @@ -1668,7 +1721,6 @@ jobs: mathcomp-ssreflect: needs: - coq - - stdlib - hierarchy-builder runs-on: ubuntu-latest steps: @@ -1721,10 +1773,6 @@ jobs: 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: stdlib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" - --argstr job "stdlib" - 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 "rocq-9.0" diff --git a/.nix/config.nix b/.nix/config.nix index 616056962..79f6812fb 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -17,6 +17,7 @@ let master = [ coq-elpi-tests.job = true; stdlib.job = true; coq-elpi-tests-stdlib.job = true; + rocq-elpi.job = false; mathcomp-single-planB-src.job = false; mathcomp-single-planB.job = false; @@ -27,7 +28,8 @@ let master = [ }; in { format = "1.0.0"; - attribute = "coq-elpi"; + attribute = "rocq-elpi"; + coq-attribute = "coq-elpi"; default-bundle = "coq-8.20"; bundles = { @@ -42,20 +44,30 @@ let master = [ coq-elpi.override.elpi-version = "2.0.7"; }; - "coq-master".coqPackages = common-bundles // { + "coq-master" = { rocqPackages = { + rocq-core.override.version = "master"; + rocq-elpi.override.elpi-version = "2.0.7"; + stdlib.override.version = "master"; + bignums.override.version = "master"; + }; coqPackages = common-bundles // { coq.override.version = "master"; coq-elpi.override.elpi-version = "2.0.7"; stdlib.override.version = "master"; bignums.override.version = "master"; - }; + }; }; /* uncomment bundle below if min and max elpi version start to differ - "coq-master-min-elpi"coqPackages = common-bundles // { + "coq-master-min-elpi" = { rocqPackages = { + rocq-core.override.version = "master"; + rocq-elpi.override.elpi-version = "2.0.7"; + stdlib.override.version = "master"; + bignums.override.version = "master"; + }; coqPackages = common-bundles // { coq.override.version = "master"; coq-elpi.override.elpi-version = "2.0.7"; stdlib.override.version = "master"; bignums.override.version = "master"; - }; */ + }; }; */ }; diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index d2d4acaf3..a0ff59561 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"d914139ccc501c967eb97ea995f9765f4094d228" +"b598891e5323d9e68fcb1c2483c2e0a046e6de54" diff --git a/.nix/coq-overlays/coq-elpi/default.nix b/.nix/coq-overlays/coq-elpi/default.nix deleted file mode 100644 index 85c5e89e8..000000000 --- a/.nix/coq-overlays/coq-elpi/default.nix +++ /dev/null @@ -1,123 +0,0 @@ -{ - lib, - mkCoqDerivation, - which, - coq, - version ? null, - elpi-version ? null, -}: - -let -default-elpi-version = if elpi-version != null then elpi-version else ( - lib.switch coq.coq-version [ - { case = "8.11"; out = "1.11.4"; } - { case = "8.12"; out = "1.12.0"; } - { case = "8.13"; out = "1.13.7"; } - { case = "8.14"; out = "1.13.7"; } - { case = "8.15"; out = "1.15.0"; } - { case = "8.16"; out = "1.17.0"; } - { case = "8.17"; out = "1.17.0"; } - { case = "8.18"; out = "1.18.1"; } - { case = "8.19"; out = "1.18.1"; } - { case = "8.20"; out = "1.19.2"; } - { case = "9.0"; out = "2.0.7"; } - ] { } -); -elpi = coq.ocamlPackages.elpi.override { version = default-elpi-version; }; -propagatedBuildInputs_wo_elpi = [ - coq.ocamlPackages.findlib -]; -derivation = mkCoqDerivation { - pname = "elpi"; - repo = "coq-elpi"; - owner = "LPCIC"; - opam-name = "rocq-elpi"; - inherit version; - defaultVersion = lib.switch coq.coq-version [ - { case = "9.0"; out = "2.4.0"; } - { case = "8.20"; out = "2.2.0"; } - { case = "8.19"; out = "2.0.1"; } - { case = "8.18"; out = "2.0.0"; } - { case = "8.17"; out = "1.18.0"; } - { case = "8.16"; out = "1.15.6"; } - { case = "8.15"; out = "1.14.0"; } - { case = "8.14"; out = "1.11.2"; } - { case = "8.13"; out = "1.11.1"; } - { case = "8.12"; out = "1.8.3_8.12"; } - { case = "8.11"; out = "1.6.3_8.11"; } - ] null; - release."2.4.0".sha256 = "sha256-W2+vVGExLLux8e0nSZESSoMVvrLxhL6dmXkb+JuKiqc="; - release."2.2.0".sha256 = "sha256-rADEoqTXM7/TyYkUKsmCFfj6fjpWdnZEOK++5oLfC/I="; - release."2.0.1".sha256 = "sha256-cuoPsEJ+JRLVc9Golt2rJj4P7lKltTrrmQijjoViooc="; - release."2.0.0".sha256 = "sha256-A/cH324M21k3SZ7+YWXtaYEbu6dZQq3K0cb1RMKjbsM="; - release."1.19.0".sha256 = "sha256-kGoo61nJxeG/BqV+iQaV3iinwPStND+7+fYMxFkiKrQ="; - release."1.18.0".sha256 = "sha256-2fCOlhqi4YkiL5n8SYHuc3pLH+DArf9zuMH7IhpBc2Y="; - release."1.17.0".sha256 = "sha256-J8GatRKFU0ekNCG3V5dBI+FXypeHcLgC5QJYGYzFiEM="; - release."1.15.6".sha256 = "sha256-qc0q01tW8NVm83801HHOBHe/7H1/F2WGDbKO6nCXfno="; - release."1.15.1".sha256 = "sha256-NT2RlcIsFB9AvBhMxil4ZZIgx+KusMqDflj2HgQxsZg="; - release."1.14.0".sha256 = "sha256:1v2p5dlpviwzky2i14cj7gcgf8cr0j54bdm9fl5iz1ckx60j6nvp"; - release."1.13.0".sha256 = "1j7s7dlnjbw222gnbrsjgmjck1yrx7h6hwm8zikcyxi0zys17w7n"; - release."1.12.1".sha256 = "sha256-4mO6/co7NcIQSGIQJyoO8lNWXr6dqz+bIYPO/G0cPkY="; - release."1.11.2".sha256 = "0qk5cfh15y2zrja7267629dybd3irvxk1raz7z8qfir25a81ckd4"; - release."1.11.1".sha256 = "10j076vc2hdcbm15m6s7b6xdzibgfcbzlkgjnlkr2vv9k13qf8kc"; - release."1.10.1".sha256 = "1zsyx26dvj7pznfd2msl2w7zbw51q1nsdw0bdvdha6dga7ijf7xk"; - release."1.9.7".sha256 = "0rvn12h9dpk9s4pxy32p8j0a1h7ib7kg98iv1cbrdg25y5vs85n1"; - release."1.9.5".sha256 = "0gjdwmb6bvb5gh0a6ra48bz5fb3pr5kpxijb7a8mfydvar5i9qr6"; - release."1.9.4".sha256 = "0nii7238mya74f9g6147qmpg6gv6ic9b54x5v85nb6q60d9jh0jq"; - release."1.9.3".sha256 = "198irm800fx3n8n56vx1c6f626cizp1d7jfkrc6ba4iqhb62ma0z"; - release."1.9.2".sha256 = "1rr2fr8vjkc0is7vh1461aidz2iwkigdkp6bqss4hhv0c3ijnn07"; - release."1.8.3_8.12".sha256 = "15z2l4zy0qpw0ws7bvsmpmyv543aqghrfnl48nlwzn9q0v89p557"; - release."1.8.3_8.12".version = "1.8.3"; - release."1.8.2_8.12".sha256 = "1n6jwcdazvjgj8vsv2r9zgwpw5yqr5a1ndc2pwhmhqfl04b5dk4y"; - release."1.8.2_8.12".version = "1.8.2"; - release."1.8.1".sha256 = "1fbbdccdmr8g4wwpihzp4r2xacynjznf817lhijw6kqfav75zd0r"; - release."1.8.0".sha256 = "13ywjg94zkbki22hx7s4gfm9rr87r4ghsgan23xyl3l9z8q0idd1"; - release."1.7.0".sha256 = "1ws5cqr0xawv69prgygbl3q6dgglbaw0vc397h9flh90kxaqgyh8"; - release."1.6.3_8.11".sha256 = "1j340cr2bv95clzzkkfmsjkklham1mj84cmiyprzwv20q89zr1hp"; - release."1.6.3_8.11".version = "1.6.3"; - release."1.6.2_8.11".sha256 = "06xrx0ljilwp63ik2sxxr7h617dgbch042xfcnfpy5x96br147rn"; - release."1.6.2_8.11".version = "1.6.2"; - release."1.6.1_8.11".sha256 = "0yyyh35i1nb3pg4hw7cak15kj4y6y9l84nwar9k1ifdsagh5zq53"; - release."1.6.1_8.11".version = "1.6.1"; - release."1.6.0_8.11".sha256 = "0ahxjnzmd7kl3gl38kyjqzkfgllncr2ybnw8bvgrc6iddgga7bpq"; - release."1.6.0_8.11".version = "1.6.0"; - release."1.6.0".sha256 = "0kf99i43mlf750fr7fric764mm495a53mg5kahnbp6zcjcxxrm0b"; - releaseRev = v: "v${v}"; - - buildFlags = [ "OCAMLWARN=" ]; - - mlPlugin = true; - useDuneifVersion = v: lib.versions.isGe "2.2.0" v || v == "dev"; - - propagatedBuildInputs = propagatedBuildInputs_wo_elpi ++ [ elpi ]; - - preConfigure = '' - make elpi/dune || true - make dune-files || true - ''; - - meta = { - description = "Coq plugin embedding ELPI"; - maintainers = [ lib.maintainers.cohencyril ]; - license = lib.licenses.lgpl21Plus; - }; -}; -patched-derivation1 = derivation.overrideAttrs - ( - o: - lib.optionalAttrs (o ? elpi-version) - { - propagatedBuildInputs = propagatedBuildInputs_wo_elpi ++ [ - (coq.ocamlPackages.elpi.override { version = o.elpi-version; }) - ]; - } - ); -patched-derivation2 = patched-derivation1.overrideAttrs - ( - o: - lib.optionalAttrs (o.version != null && (o.version == "dev" || lib.versions.isGe "2.2.0" o.version)) - { - propagatedBuildInputs = o.propagatedBuildInputs ++ [ coq.ocamlPackages.ppx_optcomp ]; - } - ); -in patched-derivation2 diff --git a/.nix/coq-overlays/hierarchy-builder/default.nix b/.nix/coq-overlays/hierarchy-builder/default.nix deleted file mode 100644 index 084cc9f7f..000000000 --- a/.nix/coq-overlays/hierarchy-builder/default.nix +++ /dev/null @@ -1,51 +0,0 @@ -{ lib, mkCoqDerivation, coq, coq-elpi, stdlib, version ? null }: - -let hb = mkCoqDerivation { - pname = "hierarchy-builder"; - owner = "math-comp"; - inherit version; - defaultVersion = with lib.versions; lib.switch coq.coq-version [ - { case = range "9.0" "9.0"; out = "1.8.1"; } - { case = range "8.19" "8.20"; out = "1.8.0"; } - { case = range "8.18" "8.20"; out = "1.7.1"; } - { case = range "8.16" "8.18"; out = "1.6.0"; } - { case = range "8.15" "8.18"; out = "1.5.0"; } - { case = range "8.15" "8.17"; out = "1.4.0"; } - { case = range "8.13" "8.14"; out = "1.2.0"; } - { case = range "8.12" "8.13"; out = "1.1.0"; } - { case = isEq "8.11"; out = "0.10.0"; } - ] null; - release."1.8.1".sha256 = "sha256-Z0WAHDyycqgL+Le/zNfEAoLWzFb7WIL+3G3vEBExlb4="; - release."1.8.0".sha256 = "sha256-4s/4ZZKj5tiTtSHGIM8Op/Pak4Vp52WVOpd4l9m19fY="; - release."1.7.1".sha256 = "sha256-MCmOzMh/SBTFAoPbbIQ7aqd3hMcSMpAKpiZI7dbRaGs="; - release."1.7.0".sha256 = "sha256-WqSeuJhmqicJgXw/xGjGvbRzfyOK7rmkVRb6tPDTAZg="; - release."1.6.0".sha256 = "sha256-E8s20veOuK96knVQ7rEDSt8VmbtYfPgItD0dTY/mckg="; - release."1.5.0".sha256 = "sha256-Lia3o156Pbe8rDHOA1IniGYsG5/qzZkzDKdHecfmS+c="; - release."1.4.0".sha256 = "sha256-tOed9UU3kMw6KWHJ5LVLUFEmzHx1ImutXQvZ0ldW9rw="; - release."1.3.0".sha256 = "17k7rlxdx43qda6i1yafpgc64na8br285cb0mbxy5wryafcdrkrc"; - release."1.2.1".sha256 = "sha256-pQYZJ34YzvdlRSGLwsrYgPdz3p/l5f+KhJjkYT08Mj0="; - release."1.2.0".sha256 = "0sk01rvvk652d86aibc8rik2m8iz7jn6mw9hh6xkbxlsvh50719d"; - release."1.1.0".sha256 = "sha256-spno5ty4kU4WWiOfzoqbXF8lWlNSlySWcRReR3zE/4Q="; - release."1.0.0".sha256 = "0yykygs0z6fby6vkiaiv3azy1i9yx4rqg8xdlgkwnf2284hffzpp"; - release."0.10.0".sha256 = "1a3vry9nzavrlrdlq3cys3f8kpq3bz447q8c4c7lh2qal61wb32h"; - releaseRev = v: "v${v}"; - - propagatedBuildInputs = [ coq-elpi stdlib ]; - - mlPlugin = true; - - meta = with lib; { - description = "High level commands to declare a hierarchy based on packed classes"; - maintainers = with maintainers; [ cohencyril siraben ]; - license = licenses.mit; - }; -}; in -hb.overrideAttrs (o: - lib.optionalAttrs (lib.versions.isGe "1.2.0" o.version || o.version == "dev") - { buildPhase = "make build"; } - // - (if lib.versions.isGe "1.1.0" o.version || o.version == "dev" then - { installFlags = [ "DESTDIR=$(out)" ] ++ o.installFlags; } - else - { installFlags = [ "VFILES=structures.v" ] ++ o.installFlags; }) -)