From ba8f7c53f9b263a22dc82a82fe209c03331bdc54 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 24 Jun 2026 10:57:26 +0200 Subject: [PATCH 1/5] release for 9.2 --- .github/workflows/main.yml | 1 + Changelog.md | 8 ++++++++ rocq-hierarchy-builder.opam | 2 +- 3 files changed, 10 insertions(+), 1 deletion(-) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 0da290bf..05ac33c9 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/Changelog.md b/Changelog.md index 6242e784..e5064f54 100644 --- a/Changelog.md +++ b/Changelog.md @@ -1,5 +1,13 @@ # Changelog +## [1.10.2] - 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 + ## [1.10.1] - 2025-09-08 Compatible with diff --git a/rocq-hierarchy-builder.opam b/rocq-hierarchy-builder.opam index 8dcf1c25..cd1bdb07 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~"} From c69ed587c17a3dab54b2d5fb8302f59f2caee2c8 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 24 Jun 2026 11:38:25 +0200 Subject: [PATCH 2/5] bump nix --- .github/workflows/nix-action-rocq-9.0.yml | 36 +++++++++++++------- .github/workflows/nix-action-rocq-9.1.yml | 36 +++++++++++++------- .github/workflows/nix-action-rocq-9.2.yml | 5 +++ .github/workflows/nix-action-rocq-master.yml | 5 +++ .nix/coq-nix-toolbox.nix | 2 +- 5 files changed, 57 insertions(+), 27 deletions(-) diff --git a/.github/workflows/nix-action-rocq-9.0.yml b/.github/workflows/nix-action-rocq-9.0.yml index 78a9cc1e..d9e6afd7 100644 --- a/.github/workflows/nix-action-rocq-9.0.yml +++ b/.github/workflows/nix-action-rocq-9.0.yml @@ -262,7 +262,6 @@ jobs: needs: - coq - multinomials - - mathcomp-real-closed runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -315,6 +314,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-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: bignums' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -323,10 +326,6 @@ jobs: name: 'Building/fetching previous CI target: multinomials' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" --argstr job "multinomials" - - if: steps.stepCheck.outputs.status != '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 @@ -804,6 +803,7 @@ jobs: - mathcomp-reals - mathcomp-field - mathcomp-bigenough + - mathcomp-real-closed runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -868,6 +868,10 @@ jobs: 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 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 @@ -1214,7 +1218,7 @@ jobs: mathcomp-experimental-reals: needs: - rocq-core - - mathcomp-reals + - mathcomp-analysis - mathcomp-bigenough runs-on: ubuntu-latest steps: @@ -1269,9 +1273,9 @@ jobs: run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "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: mathcomp-bigenough' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -1553,7 +1557,9 @@ jobs: "rocq-9.0" --argstr job "mathcomp-order" mathcomp-real-closed: needs: - - coq + - rocq-core + - mathcomp-field + - mathcomp-bigenough runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1603,13 +1609,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-ssreflect' + 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-ssreflect" + "rocq-9.0" --argstr job "mathcomp-field" + - 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 a1fe1129..9c19b66f 100644 --- a/.github/workflows/nix-action-rocq-9.1.yml +++ b/.github/workflows/nix-action-rocq-9.1.yml @@ -262,7 +262,6 @@ jobs: needs: - coq - multinomials - - mathcomp-real-closed runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -315,6 +314,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-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: bignums' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -323,10 +326,6 @@ jobs: name: 'Building/fetching previous CI target: multinomials' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.1" --argstr job "multinomials" - - 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 @@ -804,6 +803,7 @@ jobs: - mathcomp-reals - mathcomp-field - mathcomp-bigenough + - mathcomp-real-closed runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -868,6 +868,10 @@ jobs: 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 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 @@ -1214,7 +1218,7 @@ jobs: mathcomp-experimental-reals: needs: - rocq-core - - mathcomp-reals + - mathcomp-analysis - mathcomp-bigenough runs-on: ubuntu-latest steps: @@ -1269,9 +1273,9 @@ jobs: run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "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: mathcomp-bigenough' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -1553,7 +1557,9 @@ jobs: "rocq-9.1" --argstr job "mathcomp-order" mathcomp-real-closed: needs: - - coq + - rocq-core + - mathcomp-field + - mathcomp-bigenough runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1603,13 +1609,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-ssreflect' + 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-ssreflect" + "rocq-9.1" --argstr job "mathcomp-field" + - 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 369d7ad7..023e858d 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 diff --git a/.github/workflows/nix-action-rocq-master.yml b/.github/workflows/nix-action-rocq-master.yml index 9e4f8d86..c6eb0ada 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 diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index a4db61a5..22ddfe2f 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"dd3cb28d6d96d2128e4e16effc8d84d40f82f5ef" +"dd198b999f8526670a6f71a28bc1ea6ef7393cc5" From abe326c6b6699adb54c8161e86141ab90bd1c4c9 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 24 Jun 2026 11:44:30 +0200 Subject: [PATCH 3/5] update changelog --- Changelog.md | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/Changelog.md b/Changelog.md index e5064f54..6d5eab3b 100644 --- a/Changelog.md +++ b/Changelog.md @@ -1,6 +1,6 @@ # Changelog -## [1.10.2] - 2026-06-24 +## [1.10.3] - 2026-06-24 Compatible with - Coq 8.20 with Coq-Elpi 3.0.x @@ -8,6 +8,19 @@ Compatible with - 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 From 3157f9b334f68a1025b930824152403d3ce64271 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 24 Jun 2026 14:34:45 +0200 Subject: [PATCH 4/5] [CI] Fix nix config --- .github/workflows/nix-action-rocq-9.0.yml | 290 ++++++++++++++++--- .github/workflows/nix-action-rocq-9.1.yml | 290 ++++++++++++++++--- .github/workflows/nix-action-rocq-9.2.yml | 69 +++-- .github/workflows/nix-action-rocq-master.yml | 65 +++-- .nix/config.nix | 22 +- 5 files changed, 586 insertions(+), 150 deletions(-) diff --git a/.github/workflows/nix-action-rocq-9.0.yml b/.github/workflows/nix-action-rocq-9.0.yml index d9e6afd7..675b1101 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,7 +271,10 @@ jobs: coqeal: needs: - coq + - mathcomp-ssreflect + - mathcomp-algebra - multinomials + - mathcomp-real-closed runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -318,6 +331,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: bignums' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -326,6 +343,10 @@ jobs: name: 'Building/fetching previous CI target: multinomials' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" --argstr job "multinomials" + - if: steps.stepCheck.outputs.status != '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 @@ -333,6 +354,7 @@ jobs: coquelicot: needs: - coq + - mathcomp-boot runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -389,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 @@ -396,6 +422,7 @@ jobs: deriving: needs: - coq + - mathcomp-ssreflect runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -463,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 @@ -515,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 @@ -721,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 @@ -728,6 +774,8 @@ jobs: mathcomp-algebra-tactics: needs: - coq + - mathcomp-ssreflect + - mathcomp-algebra - mathcomp-zify runs-on: ubuntu-latest steps: @@ -785,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 @@ -799,11 +851,10 @@ jobs: "rocq-9.0" --argstr job "mathcomp-algebra-tactics" mathcomp-analysis: needs: - - rocq-core + - coq - mathcomp-reals - mathcomp-field - - mathcomp-bigenough - - mathcomp-real-closed + - 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,22 +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' - 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 previous CI target: mathcomp-real-closed' + 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-real-closed" + "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 @@ -930,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 @@ -945,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 @@ -1148,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 @@ -1200,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 @@ -1211,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 - - mathcomp-analysis - - mathcomp-bigenough + - coq + - mathcomp-reals + - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1269,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-analysis' + 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-analysis" + "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 @@ -1424,7 +1486,7 @@ jobs: "rocq-9.0" --argstr job "mathcomp-fingroup" mathcomp-finmap: needs: - - rocq-core + - coq - mathcomp-boot runs-on: ubuntu-latest steps: @@ -1475,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 @@ -1557,9 +1619,12 @@ jobs: "rocq-9.0" --argstr job "mathcomp-order" mathcomp-real-closed: needs: - - rocq-core + - coq + - mathcomp-ssreflect + - mathcomp-algebra - mathcomp-field - - mathcomp-bigenough + - mathcomp-fingroup + - mathcomp-solvable runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1609,25 +1674,38 @@ 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 + "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-bigenough' + 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-bigenough" + "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 @@ -1677,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 @@ -1741,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 @@ -1752,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 @@ -1889,9 +1976,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 @@ -1944,10 +2103,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 @@ -1959,6 +2126,9 @@ jobs: mathcomp-zify: needs: - coq + - mathcomp-boot + - mathcomp-algebra + - mathcomp-fingroup runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -2011,6 +2181,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 @@ -2022,6 +2204,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 @@ -2074,6 +2260,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 @@ -2081,6 +2283,7 @@ jobs: odd-order: needs: - coq + - mathcomp-character runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -2133,6 +2336,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 @@ -2140,6 +2347,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 9c19b66f..3b0bc02a 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,7 +271,10 @@ jobs: coqeal: needs: - coq + - mathcomp-ssreflect + - mathcomp-algebra - multinomials + - mathcomp-real-closed runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -318,6 +331,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: bignums' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -326,6 +343,10 @@ jobs: name: 'Building/fetching previous CI target: multinomials' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.1" --argstr job "multinomials" + - 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 @@ -333,6 +354,7 @@ jobs: coquelicot: needs: - coq + - mathcomp-boot runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -389,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 @@ -396,6 +422,7 @@ jobs: deriving: needs: - coq + - mathcomp-ssreflect runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -463,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 @@ -515,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 @@ -721,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 @@ -728,6 +774,8 @@ jobs: mathcomp-algebra-tactics: needs: - coq + - mathcomp-ssreflect + - mathcomp-algebra - mathcomp-zify runs-on: ubuntu-latest steps: @@ -785,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 @@ -799,11 +851,10 @@ jobs: "rocq-9.1" --argstr job "mathcomp-algebra-tactics" mathcomp-analysis: needs: - - rocq-core + - coq - mathcomp-reals - mathcomp-field - - mathcomp-bigenough - - mathcomp-real-closed + - 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,22 +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' - 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 previous CI target: mathcomp-real-closed' + 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-real-closed" + "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 @@ -930,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 @@ -945,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 @@ -1148,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 @@ -1200,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 @@ -1211,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 - - mathcomp-analysis - - mathcomp-bigenough + - coq + - mathcomp-reals + - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1269,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-analysis' + 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-analysis" + "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 @@ -1424,7 +1486,7 @@ jobs: "rocq-9.1" --argstr job "mathcomp-fingroup" mathcomp-finmap: needs: - - rocq-core + - coq - mathcomp-boot runs-on: ubuntu-latest steps: @@ -1475,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 @@ -1557,9 +1619,12 @@ jobs: "rocq-9.1" --argstr job "mathcomp-order" mathcomp-real-closed: needs: - - rocq-core + - coq + - mathcomp-ssreflect + - mathcomp-algebra - mathcomp-field - - mathcomp-bigenough + - mathcomp-fingroup + - mathcomp-solvable runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1609,25 +1674,38 @@ 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 + "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-bigenough' + 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-bigenough" + "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 @@ -1677,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 @@ -1741,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 @@ -1752,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 @@ -1889,9 +1976,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 @@ -1944,10 +2103,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 @@ -1959,6 +2126,9 @@ jobs: mathcomp-zify: needs: - coq + - mathcomp-boot + - mathcomp-algebra + - mathcomp-fingroup runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -2011,6 +2181,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 @@ -2022,6 +2204,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 @@ -2074,6 +2260,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 @@ -2081,6 +2283,7 @@ jobs: odd-order: needs: - coq + - mathcomp-character runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -2133,6 +2336,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 @@ -2140,6 +2347,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 023e858d..6a7a4b12 100644 --- a/.github/workflows/nix-action-rocq-9.2.yml +++ b/.github/workflows/nix-action-rocq-9.2.yml @@ -626,7 +626,7 @@ jobs: "rocq-9.2" --argstr job "hierarchy-builder" mathcomp: needs: - - coq + - rocq-core - mathcomp-character - hierarchy-builder runs-on: ubuntu-latest @@ -678,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 @@ -695,7 +695,7 @@ jobs: "rocq-9.2" --argstr job "mathcomp" mathcomp-algebra: needs: - - coq + - rocq-core - mathcomp-order - mathcomp-fingroup - hierarchy-builder @@ -748,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 @@ -763,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 @@ -1068,7 +1072,7 @@ jobs: "rocq-9.2" --argstr job "mathcomp-bigenough" mathcomp-boot: needs: - - coq + - rocq-core - hierarchy-builder runs-on: ubuntu-latest steps: @@ -1119,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 @@ -1132,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 @@ -1184,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 @@ -1354,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 @@ -1406,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 @@ -1423,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 @@ -1475,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 @@ -1556,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 @@ -1608,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 @@ -1855,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 @@ -1904,13 +1910,21 @@ 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 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 @@ -1962,9 +1976,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 @@ -1982,7 +1996,6 @@ jobs: - coq - mathcomp-boot - mathcomp-order - - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -2043,10 +2056,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 c6eb0ada..7013521f 100644 --- a/.github/workflows/nix-action-rocq-master.yml +++ b/.github/workflows/nix-action-rocq-master.yml @@ -686,7 +686,7 @@ jobs: "rocq-master" --argstr job "hierarchy-builder" mathcomp: needs: - - coq + - rocq-core - mathcomp-character - hierarchy-builder runs-on: ubuntu-latest @@ -738,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 @@ -755,7 +755,7 @@ jobs: "rocq-master" --argstr job "mathcomp" mathcomp-algebra: needs: - - coq + - rocq-core - mathcomp-order - mathcomp-fingroup - hierarchy-builder @@ -808,9 +808,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 @@ -1130,7 +1130,7 @@ jobs: "rocq-master" --argstr job "mathcomp-bigenough" mathcomp-boot: needs: - - coq + - rocq-core - hierarchy-builder runs-on: ubuntu-latest steps: @@ -1181,9 +1181,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 @@ -1194,7 +1194,7 @@ jobs: "rocq-master" --argstr job "mathcomp-boot" mathcomp-character: needs: - - coq + - rocq-core - mathcomp-field - hierarchy-builder runs-on: ubuntu-latest @@ -1246,9 +1246,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 @@ -1416,7 +1416,7 @@ jobs: "rocq-master" --argstr job "mathcomp-experimental-reals" mathcomp-field: needs: - - coq + - rocq-core - mathcomp-solvable - hierarchy-builder runs-on: ubuntu-latest @@ -1468,9 +1468,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 @@ -1485,7 +1485,7 @@ jobs: "rocq-master" --argstr job "mathcomp-field" mathcomp-fingroup: needs: - - coq + - rocq-core - mathcomp-boot - hierarchy-builder runs-on: ubuntu-latest @@ -1537,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: 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 @@ -1618,7 +1618,7 @@ jobs: "rocq-master" --argstr job "mathcomp-finmap" mathcomp-order: needs: - - coq + - rocq-core - mathcomp-boot - hierarchy-builder runs-on: ubuntu-latest @@ -1670,9 +1670,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 @@ -1918,7 +1918,9 @@ 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 runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1967,13 +1969,21 @@ 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 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 @@ -2025,9 +2035,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 @@ -2045,7 +2055,6 @@ jobs: - coq - mathcomp-boot - mathcomp-order - - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -2106,10 +2115,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 diff --git a/.nix/config.nix b/.nix/config.nix index a58daea3..73669197 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,17 @@ 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"; bignums.override.version = "master"; - }; coqPackages = mcHBcommon // { + }; coqPackages = coqMcHBcommon // { coq.override.version = "master"; stdlib.override.version = "master"; coq-elpi.override.version = "master"; @@ -44,21 +50,21 @@ coquelicot.job = false; }; }; - "rocq-9.2" = { rocqPackages = { + "rocq-9.2" = { rocqPackages = mcHBcommon // { rocq-core.override.version = "9.2"; - }; coqPackages = mcHBcommon // { + }; 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"; }; }; }; From 3127c9e85676d2eee01a08c10400c53a13a38a3f Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 24 Jun 2026 15:55:10 +0200 Subject: [PATCH 5/5] [CI] Fix micromega and single? --- .github/workflows/nix-action-rocq-9.0.yml | 4 ++ .github/workflows/nix-action-rocq-9.1.yml | 4 ++ .github/workflows/nix-action-rocq-9.2.yml | 4 ++ .github/workflows/nix-action-rocq-master.yml | 69 +++++++++++++++++++ .nix/config.nix | 3 + .nix/coq-overlays/mathcomp-single/default.nix | 4 +- 6 files changed, 86 insertions(+), 2 deletions(-) diff --git a/.github/workflows/nix-action-rocq-9.0.yml b/.github/workflows/nix-action-rocq-9.0.yml index 675b1101..2572b932 100644 --- a/.github/workflows/nix-action-rocq-9.0.yml +++ b/.github/workflows/nix-action-rocq-9.0.yml @@ -1903,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 diff --git a/.github/workflows/nix-action-rocq-9.1.yml b/.github/workflows/nix-action-rocq-9.1.yml index 3b0bc02a..076b3887 100644 --- a/.github/workflows/nix-action-rocq-9.1.yml +++ b/.github/workflows/nix-action-rocq-9.1.yml @@ -1903,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 diff --git a/.github/workflows/nix-action-rocq-9.2.yml b/.github/workflows/nix-action-rocq-9.2.yml index 6a7a4b12..9212c17e 100644 --- a/.github/workflows/nix-action-rocq-9.2.yml +++ b/.github/workflows/nix-action-rocq-9.2.yml @@ -1918,6 +1918,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 diff --git a/.github/workflows/nix-action-rocq-master.yml b/.github/workflows/nix-action-rocq-master.yml index 7013521f..517bdac8 100644 --- a/.github/workflows/nix-action-rocq-master.yml +++ b/.github/workflows/nix-action-rocq-master.yml @@ -759,6 +759,7 @@ jobs: - mathcomp-order - mathcomp-fingroup - hierarchy-builder + - micromega-plugin runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -823,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 @@ -1921,6 +1926,7 @@ jobs: needs: - rocq-core - hierarchy-builder + - micromega-plugin runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -1977,6 +1983,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 @@ -2277,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 73669197..58a081d3 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -41,6 +41,7 @@ rocq-core.override.version = "master"; stdlib.override.version = "master"; rocq-elpi.override.version = "master"; + micromega-plugin.override.version = "master"; bignums.override.version = "master"; }; coqPackages = coqMcHBcommon // { coq.override.version = "master"; @@ -52,6 +53,8 @@ "rocq-9.2" = { rocqPackages = mcHBcommon // { rocq-core.override.version = "9.2"; + micromega-plugin.override.version = "master"; + micromega-plugin.job = false; }; coqPackages = coqMcHBcommon // { coq.override.version = "9.2"; }; }; diff --git a/.nix/coq-overlays/mathcomp-single/default.nix b/.nix/coq-overlays/mathcomp-single/default.nix index c58be5ba..76a7e1c8 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;}