diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 0da290bf9..05ac33c91 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -21,6 +21,7 @@ jobs: - '8.20' - '9.0' - '9.1' + - '9.2' steps: - uses: actions/checkout@v2 - uses: coq-community/docker-coq-action@v1 diff --git a/.github/workflows/nix-action-rocq-9.0.yml b/.github/workflows/nix-action-rocq-9.0.yml index 78a9cc1ed..2572b932c 100644 --- a/.github/workflows/nix-action-rocq-9.0.yml +++ b/.github/workflows/nix-action-rocq-9.0.yml @@ -65,6 +65,7 @@ jobs: QuickChick: needs: - coq + - mathcomp-boot - ExtLib - simple-io runs-on: ubuntu-latest @@ -119,6 +120,10 @@ 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 != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-boot' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.0" --argstr job "mathcomp-boot" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: ExtLib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -193,6 +198,7 @@ jobs: coq-bits: needs: - coq + - mathcomp-algebra - mathcomp-algebra-tactics runs-on: ubuntu-latest steps: @@ -246,6 +252,10 @@ 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 != 'fetched' + 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 != 'fetched' name: 'Building/fetching previous CI target: mathcomp-algebra-tactics' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -261,6 +271,8 @@ jobs: coqeal: needs: - coq + - mathcomp-ssreflect + - mathcomp-algebra - multinomials - mathcomp-real-closed runs-on: ubuntu-latest @@ -315,6 +327,14 @@ 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 != '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-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 != 'fetched' name: 'Building/fetching previous CI target: bignums' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -334,6 +354,7 @@ jobs: coquelicot: needs: - coq + - mathcomp-boot runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -390,6 +411,10 @@ jobs: 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 != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-boot' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.0" --argstr job "mathcomp-boot" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -397,6 +422,7 @@ jobs: deriving: needs: - coq + - mathcomp-ssreflect runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -464,6 +490,9 @@ jobs: fourcolor: needs: - coq + - mathcomp-boot + - mathcomp-fingroup + - mathcomp-algebra runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -516,6 +545,18 @@ 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 != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-boot' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.0" --argstr job "mathcomp-boot" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-fingroup' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.0" --argstr job "mathcomp-fingroup" + - if: steps.stepCheck.outputs.status != 'fetched' + 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 != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -722,6 +763,10 @@ jobs: name: 'Building/fetching previous CI target: hierarchy-builder' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" --argstr job "hierarchy-builder" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: micromega-plugin' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.0" --argstr job "micromega-plugin" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -729,6 +774,8 @@ jobs: mathcomp-algebra-tactics: needs: - coq + - mathcomp-ssreflect + - mathcomp-algebra - mathcomp-zify runs-on: ubuntu-latest steps: @@ -786,6 +833,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 != 'fetched' + 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 != 'fetched' name: 'Building/fetching previous CI target: coq-elpi' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -800,10 +851,10 @@ jobs: "rocq-9.0" --argstr job "mathcomp-algebra-tactics" mathcomp-analysis: needs: - - rocq-core + - coq - mathcomp-reals - mathcomp-field - - mathcomp-bigenough + - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -853,9 +904,9 @@ jobs: \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' + name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.0" --argstr job "rocq-core" + "rocq-9.0" --argstr job "coq" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-reals' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -865,18 +916,19 @@ jobs: 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-bigenough' + name: 'Building/fetching previous CI target: hierarchy-builder' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.0" --argstr job "mathcomp-bigenough" + "rocq-9.0" --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 "rocq-9.0" --argstr job "mathcomp-analysis" mathcomp-analysis-stdlib: needs: - - rocq-core + - coq - mathcomp-analysis - mathcomp-reals-stdlib + - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -926,9 +978,9 @@ jobs: \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' + name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.0" --argstr job "rocq-core" + "rocq-9.0" --argstr job "coq" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-analysis' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -941,6 +993,10 @@ jobs: 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 != 'fetched' + name: 'Building/fetching previous CI target: hierarchy-builder' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.0" --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 @@ -1144,9 +1200,11 @@ jobs: "rocq-9.0" --argstr job "mathcomp-character" mathcomp-classical: needs: - - rocq-core + - coq + - mathcomp-ssreflect - mathcomp-algebra - mathcomp-finmap + - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1196,9 +1254,13 @@ jobs: \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' + name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.0" --argstr job "rocq-core" + "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-algebra' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -1207,15 +1269,19 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-finmap' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" --argstr job "mathcomp-finmap" + - 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-9.0" --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 "rocq-9.0" --argstr job "mathcomp-classical" mathcomp-experimental-reals: needs: - - rocq-core + - coq - mathcomp-reals - - mathcomp-bigenough + - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1265,17 +1331,17 @@ jobs: \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' + name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.0" --argstr job "rocq-core" + "rocq-9.0" --argstr job "coq" - if: steps.stepCheck.outputs.status != 'fetched' 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 != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-bigenough' + name: 'Building/fetching previous CI target: hierarchy-builder' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.0" --argstr job "mathcomp-bigenough" + "rocq-9.0" --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 @@ -1420,7 +1486,7 @@ jobs: "rocq-9.0" --argstr job "mathcomp-fingroup" mathcomp-finmap: needs: - - rocq-core + - coq - mathcomp-boot runs-on: ubuntu-latest steps: @@ -1471,9 +1537,9 @@ jobs: \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' + name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.0" --argstr job "rocq-core" + "rocq-9.0" --argstr job "coq" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-boot' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -1554,6 +1620,11 @@ jobs: mathcomp-real-closed: needs: - coq + - mathcomp-ssreflect + - mathcomp-algebra + - mathcomp-field + - mathcomp-fingroup + - mathcomp-solvable runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1610,14 +1681,31 @@ 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 != 'fetched' + 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 != '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-fingroup' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.0" --argstr job "mathcomp-fingroup" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-solvable' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.0" --argstr job "mathcomp-solvable" - 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-real-closed" mathcomp-reals: needs: - - rocq-core + - coq - mathcomp-classical + - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1667,21 +1755,26 @@ jobs: \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' + name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.0" --argstr job "rocq-core" + "rocq-9.0" --argstr job "coq" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-classical' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" --argstr job "mathcomp-classical" + - 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-9.0" --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 "rocq-9.0" --argstr job "mathcomp-reals" mathcomp-reals-stdlib: needs: - - rocq-core + - coq - mathcomp-reals + - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1731,9 +1824,9 @@ jobs: \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' + name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.0" --argstr job "rocq-core" + "rocq-9.0" --argstr job "coq" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-reals' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -1742,6 +1835,10 @@ jobs: 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 != 'fetched' + name: 'Building/fetching previous CI target: hierarchy-builder' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.0" --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 @@ -1806,6 +1903,10 @@ jobs: name: 'Building/fetching previous CI target: hierarchy-builder' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" --argstr job "hierarchy-builder" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: micromega-plugin' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.0" --argstr job "micromega-plugin" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -1879,9 +1980,81 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" --argstr job "mathcomp-solvable" + mathcomp-ssreflect: + needs: + - coq + - mathcomp-boot + - mathcomp-order + 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-ssreflect) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"rocq-9.0\" --argstr job \"mathcomp-ssreflect\" \\\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-boot' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.0" --argstr job "mathcomp-boot" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-order' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.0" --argstr job "mathcomp-order" + - 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-ssreflect" mathcomp-word: needs: - coq + - mathcomp-algebra + - mathcomp-ssreflect + - mathcomp-fingroup runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1934,10 +2107,18 @@ 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 != 'fetched' + 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 != '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-fingroup' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.0" --argstr job "mathcomp-fingroup" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: stdlib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -1949,6 +2130,9 @@ jobs: mathcomp-zify: needs: - coq + - mathcomp-boot + - mathcomp-algebra + - mathcomp-fingroup runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -2001,6 +2185,18 @@ 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 != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-boot' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.0" --argstr job "mathcomp-boot" + - if: steps.stepCheck.outputs.status != 'fetched' + 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 != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-fingroup' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.0" --argstr job "mathcomp-fingroup" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: stdlib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -2012,6 +2208,10 @@ jobs: multinomials: needs: - coq + - mathcomp-boot + - mathcomp-algebra + - mathcomp-finmap + - mathcomp-fingroup runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -2064,6 +2264,22 @@ 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 != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-boot' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.0" --argstr job "mathcomp-boot" + - if: steps.stepCheck.outputs.status != 'fetched' + 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 != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-finmap' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.0" --argstr job "mathcomp-finmap" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-fingroup' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.0" --argstr job "mathcomp-fingroup" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -2071,6 +2287,7 @@ jobs: odd-order: needs: - coq + - mathcomp-character runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -2123,6 +2340,10 @@ 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 != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-character' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.0" --argstr job "mathcomp-character" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -2130,6 +2351,7 @@ jobs: reglang: needs: - coq + - mathcomp-ssreflect runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout diff --git a/.github/workflows/nix-action-rocq-9.1.yml b/.github/workflows/nix-action-rocq-9.1.yml index a1fe11292..076b38873 100644 --- a/.github/workflows/nix-action-rocq-9.1.yml +++ b/.github/workflows/nix-action-rocq-9.1.yml @@ -65,6 +65,7 @@ jobs: QuickChick: needs: - coq + - mathcomp-boot - ExtLib - simple-io runs-on: ubuntu-latest @@ -119,6 +120,10 @@ jobs: 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-boot' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "mathcomp-boot" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: ExtLib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -193,6 +198,7 @@ jobs: coq-bits: needs: - coq + - mathcomp-algebra - mathcomp-algebra-tactics runs-on: ubuntu-latest steps: @@ -246,6 +252,10 @@ jobs: 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-algebra' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "mathcomp-algebra" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-algebra-tactics' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -261,6 +271,8 @@ jobs: coqeal: needs: - coq + - mathcomp-ssreflect + - mathcomp-algebra - multinomials - mathcomp-real-closed runs-on: ubuntu-latest @@ -315,6 +327,14 @@ jobs: 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-algebra' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "mathcomp-algebra" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: bignums' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -334,6 +354,7 @@ jobs: coquelicot: needs: - coq + - mathcomp-boot runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -390,6 +411,10 @@ jobs: name: 'Building/fetching previous CI target: stdlib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.1" --argstr job "stdlib" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-boot' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "mathcomp-boot" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -397,6 +422,7 @@ jobs: deriving: needs: - coq + - mathcomp-ssreflect runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -464,6 +490,9 @@ jobs: fourcolor: needs: - coq + - mathcomp-boot + - mathcomp-fingroup + - mathcomp-algebra runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -516,6 +545,18 @@ jobs: 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-boot' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "mathcomp-boot" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-fingroup' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "mathcomp-fingroup" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-algebra' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "mathcomp-algebra" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -722,6 +763,10 @@ jobs: name: 'Building/fetching previous CI target: hierarchy-builder' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.1" --argstr job "hierarchy-builder" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: micromega-plugin' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "micromega-plugin" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -729,6 +774,8 @@ jobs: mathcomp-algebra-tactics: needs: - coq + - mathcomp-ssreflect + - mathcomp-algebra - mathcomp-zify runs-on: ubuntu-latest steps: @@ -786,6 +833,10 @@ jobs: 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-algebra' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "mathcomp-algebra" - 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 @@ -800,10 +851,10 @@ jobs: "rocq-9.1" --argstr job "mathcomp-algebra-tactics" mathcomp-analysis: needs: - - rocq-core + - coq - mathcomp-reals - mathcomp-field - - mathcomp-bigenough + - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -853,9 +904,9 @@ jobs: \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' + name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "rocq-core" + "rocq-9.1" --argstr job "coq" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-reals' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -865,18 +916,19 @@ jobs: 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-bigenough' + name: 'Building/fetching previous CI target: hierarchy-builder' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "mathcomp-bigenough" + "rocq-9.1" --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 "rocq-9.1" --argstr job "mathcomp-analysis" mathcomp-analysis-stdlib: needs: - - rocq-core + - coq - mathcomp-analysis - mathcomp-reals-stdlib + - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -926,9 +978,9 @@ jobs: \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' + name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "rocq-core" + "rocq-9.1" --argstr job "coq" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-analysis' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -941,6 +993,10 @@ jobs: name: 'Building/fetching previous CI target: stdlib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.1" --argstr job "stdlib" + - 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-9.1" --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 @@ -1144,9 +1200,11 @@ jobs: "rocq-9.1" --argstr job "mathcomp-character" mathcomp-classical: needs: - - rocq-core + - coq + - mathcomp-ssreflect - mathcomp-algebra - mathcomp-finmap + - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1196,9 +1254,13 @@ jobs: \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' + name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "rocq-core" + "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-algebra' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -1207,15 +1269,19 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-finmap' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.1" --argstr job "mathcomp-finmap" + - 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-9.1" --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 "rocq-9.1" --argstr job "mathcomp-classical" mathcomp-experimental-reals: needs: - - rocq-core + - coq - mathcomp-reals - - mathcomp-bigenough + - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1265,17 +1331,17 @@ jobs: \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' + name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "rocq-core" + "rocq-9.1" --argstr job "coq" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-reals' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.1" --argstr job "mathcomp-reals" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-bigenough' + name: 'Building/fetching previous CI target: hierarchy-builder' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "mathcomp-bigenough" + "rocq-9.1" --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 @@ -1420,7 +1486,7 @@ jobs: "rocq-9.1" --argstr job "mathcomp-fingroup" mathcomp-finmap: needs: - - rocq-core + - coq - mathcomp-boot runs-on: ubuntu-latest steps: @@ -1471,9 +1537,9 @@ jobs: \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' + name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "rocq-core" + "rocq-9.1" --argstr job "coq" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-boot' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -1554,6 +1620,11 @@ jobs: mathcomp-real-closed: needs: - coq + - mathcomp-ssreflect + - mathcomp-algebra + - mathcomp-field + - mathcomp-fingroup + - mathcomp-solvable runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1610,14 +1681,31 @@ jobs: 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-algebra' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "mathcomp-algebra" + - 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-fingroup' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "mathcomp-fingroup" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-solvable' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "mathcomp-solvable" - 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-real-closed" mathcomp-reals: needs: - - rocq-core + - coq - mathcomp-classical + - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1667,21 +1755,26 @@ jobs: \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' + name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "rocq-core" + "rocq-9.1" --argstr job "coq" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-classical' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.1" --argstr job "mathcomp-classical" + - 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-9.1" --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 "rocq-9.1" --argstr job "mathcomp-reals" mathcomp-reals-stdlib: needs: - - rocq-core + - coq - mathcomp-reals + - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1731,9 +1824,9 @@ jobs: \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' + name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "rocq-core" + "rocq-9.1" --argstr job "coq" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-reals' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -1742,6 +1835,10 @@ jobs: name: 'Building/fetching previous CI target: stdlib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.1" --argstr job "stdlib" + - 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-9.1" --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 @@ -1806,6 +1903,10 @@ jobs: name: 'Building/fetching previous CI target: hierarchy-builder' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.1" --argstr job "hierarchy-builder" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: micromega-plugin' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "micromega-plugin" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -1879,9 +1980,81 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.1" --argstr job "mathcomp-solvable" + mathcomp-ssreflect: + needs: + - coq + - mathcomp-boot + - mathcomp-order + 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-ssreflect) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"rocq-9.1\" --argstr job \"mathcomp-ssreflect\" \\\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-boot' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "mathcomp-boot" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-order' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "mathcomp-order" + - 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-ssreflect" mathcomp-word: needs: - coq + - mathcomp-algebra + - mathcomp-ssreflect + - mathcomp-fingroup runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1934,10 +2107,18 @@ jobs: 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-algebra' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "mathcomp-algebra" - 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-fingroup' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "mathcomp-fingroup" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: stdlib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -1949,6 +2130,9 @@ jobs: mathcomp-zify: needs: - coq + - mathcomp-boot + - mathcomp-algebra + - mathcomp-fingroup runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -2001,6 +2185,18 @@ jobs: 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-boot' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "mathcomp-boot" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-algebra' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "mathcomp-algebra" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-fingroup' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "mathcomp-fingroup" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: stdlib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -2012,6 +2208,10 @@ jobs: multinomials: needs: - coq + - mathcomp-boot + - mathcomp-algebra + - mathcomp-finmap + - mathcomp-fingroup runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -2064,6 +2264,22 @@ jobs: 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-boot' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "mathcomp-boot" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-algebra' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "mathcomp-algebra" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-finmap' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "mathcomp-finmap" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-fingroup' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "mathcomp-fingroup" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -2071,6 +2287,7 @@ jobs: odd-order: needs: - coq + - mathcomp-character runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -2123,6 +2340,10 @@ jobs: 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-character' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "mathcomp-character" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -2130,6 +2351,7 @@ jobs: reglang: needs: - coq + - mathcomp-ssreflect runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout diff --git a/.github/workflows/nix-action-rocq-9.2.yml b/.github/workflows/nix-action-rocq-9.2.yml index 369d7ad71..9212c17ee 100644 --- a/.github/workflows/nix-action-rocq-9.2.yml +++ b/.github/workflows/nix-action-rocq-9.2.yml @@ -271,6 +271,7 @@ jobs: coqeal: needs: - coq + - mathcomp-ssreflect - mathcomp-algebra - multinomials - mathcomp-real-closed @@ -326,6 +327,10 @@ jobs: name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.2" --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.2" --argstr job "mathcomp-ssreflect" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-algebra' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -621,7 +626,7 @@ jobs: "rocq-9.2" --argstr job "hierarchy-builder" mathcomp: needs: - - coq + - rocq-core - mathcomp-character - hierarchy-builder runs-on: ubuntu-latest @@ -673,9 +678,9 @@ jobs: \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' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "coq" + "rocq-9.2" --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 @@ -690,7 +695,7 @@ jobs: "rocq-9.2" --argstr job "mathcomp" mathcomp-algebra: needs: - - coq + - rocq-core - mathcomp-order - mathcomp-fingroup - hierarchy-builder @@ -743,9 +748,9 @@ jobs: \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' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "coq" + "rocq-9.2" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-order' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -758,6 +763,10 @@ jobs: name: 'Building/fetching previous CI target: hierarchy-builder' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.2" --argstr job "hierarchy-builder" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: micromega-plugin' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.2" --argstr job "micromega-plugin" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -1063,7 +1072,7 @@ jobs: "rocq-9.2" --argstr job "mathcomp-bigenough" mathcomp-boot: needs: - - coq + - rocq-core - hierarchy-builder runs-on: ubuntu-latest steps: @@ -1114,9 +1123,9 @@ jobs: \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' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "coq" + "rocq-9.2" --argstr job "rocq-core" - 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 @@ -1127,7 +1136,7 @@ jobs: "rocq-9.2" --argstr job "mathcomp-boot" mathcomp-character: needs: - - coq + - rocq-core - mathcomp-field - hierarchy-builder runs-on: ubuntu-latest @@ -1179,9 +1188,9 @@ jobs: \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' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "coq" + "rocq-9.2" --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 @@ -1349,7 +1358,7 @@ jobs: "rocq-9.2" --argstr job "mathcomp-experimental-reals" mathcomp-field: needs: - - coq + - rocq-core - mathcomp-solvable - hierarchy-builder runs-on: ubuntu-latest @@ -1401,9 +1410,9 @@ jobs: \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' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "coq" + "rocq-9.2" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-solvable' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -1418,7 +1427,7 @@ jobs: "rocq-9.2" --argstr job "mathcomp-field" mathcomp-fingroup: needs: - - coq + - rocq-core - mathcomp-boot - hierarchy-builder runs-on: ubuntu-latest @@ -1470,9 +1479,9 @@ jobs: \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' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "coq" + "rocq-9.2" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-boot' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -1551,7 +1560,7 @@ jobs: "rocq-9.2" --argstr job "mathcomp-finmap" mathcomp-order: needs: - - coq + - rocq-core - mathcomp-boot - hierarchy-builder runs-on: ubuntu-latest @@ -1603,9 +1612,9 @@ jobs: \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' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "coq" + "rocq-9.2" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-boot' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -1850,7 +1859,9 @@ jobs: run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.2" --argstr job "mathcomp-reals-stdlib" mathcomp-single: - needs: [] + needs: + - rocq-core + - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1899,13 +1910,25 @@ jobs: ) ; 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.2" --argstr job "rocq-core" + - 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-9.2" --argstr job "hierarchy-builder" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: micromega-plugin' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.2" --argstr job "micromega-plugin" - 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.2" --argstr job "mathcomp-single" mathcomp-solvable: needs: - - coq + - rocq-core - mathcomp-algebra - hierarchy-builder runs-on: ubuntu-latest @@ -1957,9 +1980,9 @@ jobs: \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' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "coq" + "rocq-9.2" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-algebra' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -1977,7 +2000,6 @@ jobs: - coq - mathcomp-boot - mathcomp-order - - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -2038,10 +2060,6 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-order' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.2" --argstr job "mathcomp-order" - - 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-9.2" --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 diff --git a/.github/workflows/nix-action-rocq-master.yml b/.github/workflows/nix-action-rocq-master.yml index 9e4f8d86b..517bdac8b 100644 --- a/.github/workflows/nix-action-rocq-master.yml +++ b/.github/workflows/nix-action-rocq-master.yml @@ -396,6 +396,7 @@ jobs: coqeal: needs: - coq + - mathcomp-ssreflect - mathcomp-algebra - bignums - multinomials @@ -452,6 +453,10 @@ jobs: name: 'Building/fetching previous CI target: coq' 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-algebra' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -681,7 +686,7 @@ jobs: "rocq-master" --argstr job "hierarchy-builder" mathcomp: needs: - - coq + - rocq-core - mathcomp-character - hierarchy-builder runs-on: ubuntu-latest @@ -733,9 +738,9 @@ jobs: \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' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "coq" + "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 @@ -750,10 +755,11 @@ jobs: "rocq-master" --argstr job "mathcomp" mathcomp-algebra: needs: - - coq + - rocq-core - mathcomp-order - mathcomp-fingroup - hierarchy-builder + - micromega-plugin runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -803,9 +809,9 @@ jobs: \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' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "coq" + "rocq-master" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-order' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -818,6 +824,10 @@ jobs: 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 previous CI target: micromega-plugin' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-master" --argstr job "micromega-plugin" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -1125,7 +1135,7 @@ jobs: "rocq-master" --argstr job "mathcomp-bigenough" mathcomp-boot: needs: - - coq + - rocq-core - hierarchy-builder runs-on: ubuntu-latest steps: @@ -1176,9 +1186,9 @@ jobs: \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' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "coq" + "rocq-master" --argstr job "rocq-core" - 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 @@ -1189,7 +1199,7 @@ jobs: "rocq-master" --argstr job "mathcomp-boot" mathcomp-character: needs: - - coq + - rocq-core - mathcomp-field - hierarchy-builder runs-on: ubuntu-latest @@ -1241,9 +1251,9 @@ jobs: \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' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "coq" + "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 @@ -1411,7 +1421,7 @@ jobs: "rocq-master" --argstr job "mathcomp-experimental-reals" mathcomp-field: needs: - - coq + - rocq-core - mathcomp-solvable - hierarchy-builder runs-on: ubuntu-latest @@ -1463,9 +1473,9 @@ jobs: \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' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "coq" + "rocq-master" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-solvable' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -1480,7 +1490,7 @@ jobs: "rocq-master" --argstr job "mathcomp-field" mathcomp-fingroup: needs: - - coq + - rocq-core - mathcomp-boot - hierarchy-builder runs-on: ubuntu-latest @@ -1532,9 +1542,9 @@ jobs: \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' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "coq" + "rocq-master" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-boot' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -1613,7 +1623,7 @@ jobs: "rocq-master" --argstr job "mathcomp-finmap" mathcomp-order: needs: - - coq + - rocq-core - mathcomp-boot - hierarchy-builder runs-on: ubuntu-latest @@ -1665,9 +1675,9 @@ jobs: \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' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "coq" + "rocq-master" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-boot' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -1913,7 +1923,10 @@ jobs: run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master" --argstr job "mathcomp-reals-stdlib" mathcomp-single: - needs: [] + needs: + - rocq-core + - hierarchy-builder + - micromega-plugin runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1962,13 +1975,25 @@ jobs: ) ; 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: 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 previous CI target: micromega-plugin' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-master" --argstr job "micromega-plugin" - 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 "mathcomp-single" mathcomp-solvable: needs: - - coq + - rocq-core - mathcomp-algebra - hierarchy-builder runs-on: ubuntu-latest @@ -2020,9 +2045,9 @@ jobs: \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' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "coq" + "rocq-master" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-algebra' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -2040,7 +2065,6 @@ jobs: - coq - mathcomp-boot - mathcomp-order - - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -2101,10 +2125,6 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-order' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master" --argstr job "mathcomp-order" - - 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 @@ -2267,6 +2287,65 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master" --argstr job "mathcomp-zify" + micromega-plugin: + 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 (micromega-plugin) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"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: "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 + "rocq-master" --argstr job "micromega-plugin" multinomials: needs: - coq diff --git a/.nix/config.nix b/.nix/config.nix index a58daea39..58a081d3a 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -5,6 +5,9 @@ bundles = let mcHBcommon = { mathcomp.override.version = "master"; + }; + coqMcHBcommon = { + mathcomp.override.version = "master"; mathcomp.job = true; mathcomp-single.job = true; graph-theory.job = false; @@ -29,14 +32,18 @@ QuickChick.override.version = "master"; # jasmin.override.version = "main"; jasmin.job = false; # currently broken + autosubst.job = false; + ConCert.job = false; + interval.job = false; }; in { - "rocq-master" = { rocqPackages = { + "rocq-master" = { rocqPackages = mcHBcommon // { rocq-core.override.version = "master"; stdlib.override.version = "master"; rocq-elpi.override.version = "master"; + micromega-plugin.override.version = "master"; bignums.override.version = "master"; - }; coqPackages = mcHBcommon // { + }; coqPackages = coqMcHBcommon // { coq.override.version = "master"; stdlib.override.version = "master"; coq-elpi.override.version = "master"; @@ -44,21 +51,23 @@ coquelicot.job = false; }; }; - "rocq-9.2" = { rocqPackages = { + "rocq-9.2" = { rocqPackages = mcHBcommon // { rocq-core.override.version = "9.2"; - }; coqPackages = mcHBcommon // { + micromega-plugin.override.version = "master"; + micromega-plugin.job = false; + }; coqPackages = coqMcHBcommon // { coq.override.version = "9.2"; }; }; - "rocq-9.1" = { rocqPackages = { + "rocq-9.1" = { rocqPackages = mcHBcommon // { rocq-core.override.version = "9.1"; - }; coqPackages = mcHBcommon // { + }; coqPackages = coqMcHBcommon // { coq.override.version = "9.1"; }; }; - "rocq-9.0" = { rocqPackages = { + "rocq-9.0" = { rocqPackages = mcHBcommon // { rocq-core.override.version = "9.0"; - }; coqPackages = mcHBcommon // { + }; coqPackages = coqMcHBcommon // { coq.override.version = "9.0"; }; }; }; diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index a4db61a51..22ddfe2fe 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"dd3cb28d6d96d2128e4e16effc8d84d40f82f5ef" +"dd198b999f8526670a6f71a28bc1ea6ef7393cc5" diff --git a/.nix/coq-overlays/mathcomp-single/default.nix b/.nix/coq-overlays/mathcomp-single/default.nix index c58be5ba9..76a7e1c84 100644 --- a/.nix/coq-overlays/mathcomp-single/default.nix +++ b/.nix/coq-overlays/mathcomp-single/default.nix @@ -1,2 +1,2 @@ -{ mathcomp, version ? null }: -mathcomp.override {single = true; inherit version;} +{ mathcomp }: +mathcomp.override {single = true;} diff --git a/Changelog.md b/Changelog.md index 6242e7849..6d5eab3b5 100644 --- a/Changelog.md +++ b/Changelog.md @@ -1,5 +1,26 @@ # Changelog +## [1.10.3] - 2026-06-24 + +Compatible with +- Coq 8.20 with Coq-Elpi 3.0.x +- Rocq 9.0 with Rocq-Elpi 3.0.x +- Rocq 9.1 with Rocq-Elpi 3.0.x +- Rocq 9.2 with Rocq-Elpi 3.3.x + +- **Fix** Compilation on 9.2 + +## [1.10.2] - 2026-01-28 + +Compatible with +- Coq 8.20 with Coq-Elpi 3.0.x +- Rocq 9.0 with Rocq-Elpi 3.0.x +- Rocq 9.1 with Rocq-Elpi 3.0.x + +- **Fix** HB.howto +- **Change** Blacklist internal HB constants +- **Fix** Honour #[export] in HB.saturate + ## [1.10.1] - 2025-09-08 Compatible with diff --git a/rocq-hierarchy-builder.opam b/rocq-hierarchy-builder.opam index 8dcf1c25d..cd1bdb07c 100644 --- a/rocq-hierarchy-builder.opam +++ b/rocq-hierarchy-builder.opam @@ -13,7 +13,7 @@ build: [ [ make "build"] ] install: [ make "install" ] depends: [ - "rocq-core" {(>= "9.0" & < "9.2~") | = "dev"} & "rocq-elpi" {>= "3" | = "dev"} + "rocq-core" {(>= "9.0" & < "9.3~") | = "dev"} & "rocq-elpi" {>= "3" | = "dev"} ] conflicts: [ "coq-hierarchy-builder" {< "1.9~"}