diff --git a/.github/workflows/nix-action-rocq-9.0.yml b/.github/workflows/nix-action-rocq-9.0.yml index 1fb2652c..78ed1aad 100644 --- a/.github/workflows/nix-action-rocq-9.0.yml +++ b/.github/workflows/nix-action-rocq-9.0.yml @@ -279,7 +279,6 @@ jobs: coqeal: needs: - coq - - mathcomp-ssreflect - mathcomp-algebra - multinomials - mathcomp-real-closed @@ -337,10 +336,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 != '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 @@ -875,10 +870,11 @@ jobs: "rocq-9.0" --argstr job "mathcomp-algebra-tactics" mathcomp-analysis: needs: - - coq + - rocq-core - mathcomp-reals - mathcomp-field - - hierarchy-builder + - mathcomp-bigenough + - mathcomp-real-closed runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -930,9 +926,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.0" --argstr job "coq" + "rocq-9.0" --argstr job "rocq-core" - 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 @@ -942,19 +938,22 @@ 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: hierarchy-builder' + name: 'Building/fetching previous CI target: mathcomp-bigenough' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.0" --argstr job "hierarchy-builder" + "rocq-9.0" --argstr job "mathcomp-bigenough" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-real-closed' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.0" --argstr job "mathcomp-real-closed" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" --argstr job "mathcomp-analysis" mathcomp-analysis-stdlib: needs: - - coq + - rocq-core - mathcomp-analysis - mathcomp-reals-stdlib - - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1006,9 +1005,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.0" --argstr job "coq" + "rocq-9.0" --argstr job "rocq-core" - 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 @@ -1021,10 +1020,6 @@ 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 @@ -1234,11 +1229,9 @@ jobs: "rocq-9.0" --argstr job "mathcomp-character" mathcomp-classical: needs: - - coq - - mathcomp-ssreflect + - rocq-core - mathcomp-algebra - mathcomp-finmap - - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1290,13 +1283,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' - 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' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.0" --argstr job "mathcomp-ssreflect" + "rocq-9.0" --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 @@ -1305,19 +1294,15 @@ 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: - - coq - - mathcomp-reals - - hierarchy-builder + - rocq-core + - mathcomp-analysis + - mathcomp-bigenough runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1369,17 +1354,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: coq' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.0" --argstr job "coq" + "rocq-9.0" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-reals' + name: 'Building/fetching previous CI target: mathcomp-analysis' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.0" --argstr job "mathcomp-reals" + "rocq-9.0" --argstr job "mathcomp-analysis" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: hierarchy-builder' + name: 'Building/fetching previous CI target: mathcomp-bigenough' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.0" --argstr job "hierarchy-builder" + "rocq-9.0" --argstr job "mathcomp-bigenough" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -1528,7 +1513,7 @@ jobs: "rocq-9.0" --argstr job "mathcomp-fingroup" mathcomp-finmap: needs: - - coq + - rocq-core - mathcomp-boot runs-on: ubuntu-latest steps: @@ -1581,9 +1566,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.0" --argstr job "coq" + "rocq-9.0" --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 @@ -1665,12 +1650,9 @@ jobs: "rocq-9.0" --argstr job "mathcomp-order" mathcomp-real-closed: needs: - - coq - - mathcomp-ssreflect - - mathcomp-algebra + - rocq-core - mathcomp-field - - mathcomp-fingroup - - mathcomp-solvable + - mathcomp-bigenough runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1722,38 +1704,25 @@ 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' - 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' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.0" --argstr job "mathcomp-algebra" + "rocq-9.0" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-field' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" --argstr job "mathcomp-field" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-fingroup' + name: 'Building/fetching previous CI target: mathcomp-bigenough' 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" + "rocq-9.0" --argstr job "mathcomp-bigenough" - 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: - - coq + - rocq-core - mathcomp-classical - - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1805,26 +1774,21 @@ 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.0" --argstr job "coq" + "rocq-9.0" --argstr job "rocq-core" - 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: - - coq + - rocq-core - mathcomp-reals - - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1876,9 +1840,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.0" --argstr job "coq" + "rocq-9.0" --argstr job "rocq-core" - 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 @@ -1887,10 +1851,6 @@ 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 @@ -2274,6 +2234,7 @@ jobs: - mathcomp-algebra - mathcomp-finmap - mathcomp-fingroup + - mathcomp-bigenough runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -2344,6 +2305,10 @@ jobs: 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-bigenough' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.0" --argstr job "mathcomp-bigenough" - 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-9.1.yml b/.github/workflows/nix-action-rocq-9.1.yml index c78c24c7..d9d7d6d2 100644 --- a/.github/workflows/nix-action-rocq-9.1.yml +++ b/.github/workflows/nix-action-rocq-9.1.yml @@ -279,7 +279,6 @@ jobs: coqeal: needs: - coq - - mathcomp-ssreflect - mathcomp-algebra - multinomials - mathcomp-real-closed @@ -337,10 +336,6 @@ 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 @@ -875,10 +870,11 @@ jobs: "rocq-9.1" --argstr job "mathcomp-algebra-tactics" mathcomp-analysis: needs: - - coq + - rocq-core - mathcomp-reals - mathcomp-field - - hierarchy-builder + - mathcomp-bigenough + - mathcomp-real-closed runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -930,9 +926,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.1" --argstr job "coq" + "rocq-9.1" --argstr job "rocq-core" - 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 @@ -942,19 +938,22 @@ 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: hierarchy-builder' + name: 'Building/fetching previous CI target: mathcomp-bigenough' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "hierarchy-builder" + "rocq-9.1" --argstr job "mathcomp-bigenough" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-real-closed' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "mathcomp-real-closed" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.1" --argstr job "mathcomp-analysis" mathcomp-analysis-stdlib: needs: - - coq + - rocq-core - mathcomp-analysis - mathcomp-reals-stdlib - - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1006,9 +1005,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.1" --argstr job "coq" + "rocq-9.1" --argstr job "rocq-core" - 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 @@ -1021,10 +1020,6 @@ 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 @@ -1234,11 +1229,9 @@ jobs: "rocq-9.1" --argstr job "mathcomp-character" mathcomp-classical: needs: - - coq - - mathcomp-ssreflect + - rocq-core - mathcomp-algebra - mathcomp-finmap - - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1290,13 +1283,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' - 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' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "mathcomp-ssreflect" + "rocq-9.1" --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 @@ -1305,19 +1294,15 @@ 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: - - coq - - mathcomp-reals - - hierarchy-builder + - rocq-core + - mathcomp-analysis + - mathcomp-bigenough runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1369,17 +1354,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: coq' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "coq" + "rocq-9.1" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-reals' + name: 'Building/fetching previous CI target: mathcomp-analysis' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "mathcomp-reals" + "rocq-9.1" --argstr job "mathcomp-analysis" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: hierarchy-builder' + name: 'Building/fetching previous CI target: mathcomp-bigenough' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "hierarchy-builder" + "rocq-9.1" --argstr job "mathcomp-bigenough" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -1528,7 +1513,7 @@ jobs: "rocq-9.1" --argstr job "mathcomp-fingroup" mathcomp-finmap: needs: - - coq + - rocq-core - mathcomp-boot runs-on: ubuntu-latest steps: @@ -1581,9 +1566,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.1" --argstr job "coq" + "rocq-9.1" --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 @@ -1665,12 +1650,9 @@ jobs: "rocq-9.1" --argstr job "mathcomp-order" mathcomp-real-closed: needs: - - coq - - mathcomp-ssreflect - - mathcomp-algebra + - rocq-core - mathcomp-field - - mathcomp-fingroup - - mathcomp-solvable + - mathcomp-bigenough runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1722,38 +1704,25 @@ 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' - 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' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.1" --argstr job "mathcomp-algebra" + "rocq-9.1" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-field' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.1" --argstr job "mathcomp-field" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-fingroup' + name: 'Building/fetching previous CI target: mathcomp-bigenough' 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" + "rocq-9.1" --argstr job "mathcomp-bigenough" - 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: - - coq + - rocq-core - mathcomp-classical - - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1805,26 +1774,21 @@ 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.1" --argstr job "coq" + "rocq-9.1" --argstr job "rocq-core" - 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: - - coq + - rocq-core - mathcomp-reals - - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1876,9 +1840,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.1" --argstr job "coq" + "rocq-9.1" --argstr job "rocq-core" - 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 @@ -1887,10 +1851,6 @@ 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 @@ -2274,6 +2234,7 @@ jobs: - mathcomp-algebra - mathcomp-finmap - mathcomp-fingroup + - mathcomp-bigenough runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -2344,6 +2305,10 @@ jobs: 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-bigenough' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "mathcomp-bigenough" - 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-9.2.yml b/.github/workflows/nix-action-rocq-9.2.yml index 52f92097..87c42231 100644 --- a/.github/workflows/nix-action-rocq-9.2.yml +++ b/.github/workflows/nix-action-rocq-9.2.yml @@ -279,7 +279,6 @@ jobs: coqeal: needs: - coq - - mathcomp-ssreflect - mathcomp-algebra - multinomials - mathcomp-real-closed @@ -337,10 +336,6 @@ 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 @@ -875,10 +870,11 @@ jobs: "rocq-9.2" --argstr job "mathcomp-algebra-tactics" mathcomp-analysis: needs: - - coq + - rocq-core - mathcomp-reals - mathcomp-field - - hierarchy-builder + - mathcomp-bigenough + - mathcomp-real-closed runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -930,9 +926,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-reals' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -942,19 +938,22 @@ jobs: run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.2" --argstr job "mathcomp-field" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: hierarchy-builder' + name: 'Building/fetching previous CI target: mathcomp-bigenough' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "hierarchy-builder" + "rocq-9.2" --argstr job "mathcomp-bigenough" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-real-closed' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.2" --argstr job "mathcomp-real-closed" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.2" --argstr job "mathcomp-analysis" mathcomp-analysis-stdlib: needs: - - coq + - rocq-core - mathcomp-analysis - mathcomp-reals-stdlib - - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1006,9 +1005,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-analysis' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -1021,10 +1020,6 @@ jobs: name: 'Building/fetching previous CI target: stdlib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.2" --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.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 @@ -1234,11 +1229,9 @@ jobs: "rocq-9.2" --argstr job "mathcomp-character" mathcomp-classical: needs: - - coq - - mathcomp-ssreflect + - rocq-core - mathcomp-algebra - mathcomp-finmap - - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1290,13 +1283,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' - 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' + 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 "mathcomp-ssreflect" + "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 @@ -1305,19 +1294,15 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-finmap' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.2" --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.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 "rocq-9.2" --argstr job "mathcomp-classical" mathcomp-experimental-reals: needs: - - coq - - mathcomp-reals - - hierarchy-builder + - rocq-core + - mathcomp-analysis + - mathcomp-bigenough runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1369,17 +1354,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: 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-reals' + name: 'Building/fetching previous CI target: mathcomp-analysis' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "mathcomp-reals" + "rocq-9.2" --argstr job "mathcomp-analysis" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: hierarchy-builder' + name: 'Building/fetching previous CI target: mathcomp-bigenough' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --argstr job "hierarchy-builder" + "rocq-9.2" --argstr job "mathcomp-bigenough" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -1528,7 +1513,7 @@ jobs: "rocq-9.2" --argstr job "mathcomp-fingroup" mathcomp-finmap: needs: - - coq + - rocq-core - mathcomp-boot runs-on: ubuntu-latest steps: @@ -1581,9 +1566,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 @@ -1665,12 +1650,9 @@ jobs: "rocq-9.2" --argstr job "mathcomp-order" mathcomp-real-closed: needs: - - coq - - mathcomp-ssreflect - - mathcomp-algebra + - rocq-core - mathcomp-field - - mathcomp-fingroup - - mathcomp-solvable + - mathcomp-bigenough runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1722,38 +1704,25 @@ 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' - 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' + 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 "mathcomp-algebra" + "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 "rocq-9.2" --argstr job "mathcomp-field" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-fingroup' + name: 'Building/fetching previous CI target: mathcomp-bigenough' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-9.2" --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.2" --argstr job "mathcomp-solvable" + "rocq-9.2" --argstr job "mathcomp-bigenough" - 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-real-closed" mathcomp-reals: needs: - - coq + - rocq-core - mathcomp-classical - - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1805,26 +1774,21 @@ 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-classical' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.2" --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.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 "rocq-9.2" --argstr job "mathcomp-reals" mathcomp-reals-stdlib: needs: - - coq + - rocq-core - mathcomp-reals - - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1876,9 +1840,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-reals' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -1887,10 +1851,6 @@ jobs: name: 'Building/fetching previous CI target: stdlib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.2" --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.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 @@ -2274,6 +2234,7 @@ jobs: - mathcomp-algebra - mathcomp-finmap - mathcomp-fingroup + - mathcomp-bigenough runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -2344,6 +2305,10 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-fingroup' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.2" --argstr job "mathcomp-fingroup" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-bigenough' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.2" --argstr job "mathcomp-bigenough" - 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 56efe9b0..c42f19b3 100644 --- a/.github/workflows/nix-action-rocq-master.yml +++ b/.github/workflows/nix-action-rocq-master.yml @@ -408,7 +408,6 @@ jobs: coqeal: needs: - coq - - mathcomp-ssreflect - mathcomp-algebra - bignums - multinomials @@ -467,10 +466,6 @@ 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 @@ -939,11 +934,11 @@ jobs: "rocq-master" --argstr job "mathcomp-algebra-tactics" mathcomp-analysis: needs: - - coq + - rocq-core - mathcomp-reals - mathcomp-field - mathcomp-bigenough - - hierarchy-builder + - mathcomp-real-closed runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -995,9 +990,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-reals' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -1011,20 +1006,19 @@ jobs: run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master" --argstr job "mathcomp-bigenough" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: hierarchy-builder' + name: 'Building/fetching previous CI target: mathcomp-real-closed' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "hierarchy-builder" + "rocq-master" --argstr job "mathcomp-real-closed" - if: steps.stepCheck.outputs.status != 'fetched' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master" --argstr job "mathcomp-analysis" mathcomp-analysis-stdlib: needs: - - coq + - rocq-core - mathcomp-analysis - mathcomp-reals-stdlib - stdlib - - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1076,9 +1070,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-analysis' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -1091,17 +1085,13 @@ jobs: name: 'Building/fetching previous CI target: stdlib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master" --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-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 "rocq-master" --argstr job "mathcomp-analysis-stdlib" mathcomp-bigenough: needs: - - coq + - rocq-core - mathcomp-boot runs-on: ubuntu-latest steps: @@ -1154,9 +1144,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 @@ -1304,11 +1294,9 @@ jobs: "rocq-master" --argstr job "mathcomp-character" mathcomp-classical: needs: - - coq - - mathcomp-ssreflect + - rocq-core - mathcomp-algebra - mathcomp-finmap - - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1360,13 +1348,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' - 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' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "mathcomp-ssreflect" + "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 @@ -1375,20 +1359,15 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-finmap' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master" --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-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 "rocq-master" --argstr job "mathcomp-classical" mathcomp-experimental-reals: needs: - - coq - - mathcomp-reals + - rocq-core + - mathcomp-analysis - mathcomp-bigenough - - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1440,21 +1419,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: 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-reals' + name: 'Building/fetching previous CI target: mathcomp-analysis' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "mathcomp-reals" + "rocq-master" --argstr job "mathcomp-analysis" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-bigenough' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master" --argstr job "mathcomp-bigenough" - - 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 @@ -1603,7 +1578,7 @@ jobs: "rocq-master" --argstr job "mathcomp-fingroup" mathcomp-finmap: needs: - - coq + - rocq-core - mathcomp-boot runs-on: ubuntu-latest steps: @@ -1656,9 +1631,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 @@ -1740,12 +1715,8 @@ jobs: "rocq-master" --argstr job "mathcomp-order" mathcomp-real-closed: needs: - - coq - - mathcomp-ssreflect - - mathcomp-algebra + - rocq-core - mathcomp-field - - mathcomp-fingroup - - mathcomp-solvable - mathcomp-bigenough runs-on: ubuntu-latest steps: @@ -1798,29 +1769,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: 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' + name: 'Building/fetching previous CI target: rocq-core' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --argstr job "mathcomp-algebra" + "rocq-master" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-field' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master" --argstr job "mathcomp-field" - - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-fingroup' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "rocq-master" --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-master" --argstr job "mathcomp-solvable" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-bigenough' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -1831,9 +1786,8 @@ jobs: "rocq-master" --argstr job "mathcomp-real-closed" mathcomp-reals: needs: - - coq + - rocq-core - mathcomp-classical - - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1885,27 +1839,22 @@ 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-classical' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master" --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-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 "rocq-master" --argstr job "mathcomp-reals" mathcomp-reals-stdlib: needs: - - coq + - rocq-core - mathcomp-reals - stdlib - - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1957,9 +1906,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-reals' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -1968,10 +1917,6 @@ jobs: name: 'Building/fetching previous CI target: stdlib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master" --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-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 diff --git a/.nix/config.nix b/.nix/config.nix index 58a081d3..79323bac 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -5,6 +5,10 @@ bundles = let mcHBcommon = { mathcomp.override.version = "master"; + mathcomp-bigenough.override.version = "master"; + mathcomp-finmap.override.version = "master"; + mathcomp-real-closed.override.version = "master"; + mathcomp-analysis.override.version = "master"; }; coqMcHBcommon = { mathcomp.override.version = "master"; diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index 87979758..65b0398f 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"991ce22c6edb5246e52987e0717372b0189d360a" +"be5f4606e338f3ae99e4cfd2be51a8e871ddd390" diff --git a/Makefile b/Makefile index ddb7d560..f1127601 100644 --- a/Makefile +++ b/Makefile @@ -13,10 +13,10 @@ # # # Additionally, the following variables may be customized: # SUBDIRS?= -COQBIN?=$(dir $(shell command -v coqtop || command -v rocq)) -COQTOP=$(shell command -v coqtop || echo "$(COQBIN)rocq repl") -COQMAKEFILE?=$(shell command -v coq_makefile || echo "$(COQBIN)rocq makefile") -COQDEP?=$(COQBIN)coqdep +COQBIN?=$(dir $(shell command -v rocq)) +COQTOP=$(shell echo "$(COQBIN)rocq repl") +COQMAKEFILE?=$(shell echo "$(COQBIN)rocq makefile") +COQDEP?=$(shell echo "$(COQBIN)rocq dep") COQPROJECT?=_CoqProject COQMAKEOPTIONS?= COQMAKEFILEOPTIONS?= @@ -93,23 +93,6 @@ distclean: sub-distclean this-distclean # Local config, build, clean and distclean --------------------------- .PHONY: this-config this-build this-only this-test-suite this-test-suite-stdlib this-distclean this-clean -this-config:: __always__ - @if $$(command -v coqc >/dev/null) ; then \ - if [ -e config.stamp -a "`coqc --print-version`" = "`cat config.stamp 2>/dev/null`" ] ; then \ - echo 'already configured';\ - else\ - coqc --print-version > config.stamp;\ - echo 'configuring for ' `coqc --print-version`;\ - if (coqc --version | grep -q '8.20') ; then \ - echo '*****************************************************************';\ - echo 'old coq version detected, double check the diff before committing';\ - echo '*****************************************************************';\ - sed -i.bak -e 's/From Corelib/From Coq/' `find . -name \*.v` ; \ - sed -i.bak -e 's/IntDef/ZArith/' `find . -name \*.v` ; \ - fi;\ - fi ; fi - # Remove all of the above when requiring Rocq >= 9.0 - this-build:: this-config Makefile.coq +$(COQMAKE)