From 4f1a14d4366119b5380aff3b93b038e0c61db8ee Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 10 Jun 2026 15:12:14 +0900 Subject: [PATCH 1/3] Fix nix-shell --- .github/workflows/nix-action-9.0-master.yml | 6 +++--- .github/workflows/nix-action-9.1-master.yml | 6 +++--- .github/workflows/nix-action-master.yml | 6 +++--- .nix/coq-nix-toolbox.nix | 2 +- .nix/rocq-overlays/mathcomp-analysis-single/default.nix | 2 +- 5 files changed, 11 insertions(+), 11 deletions(-) diff --git a/.github/workflows/nix-action-9.0-master.yml b/.github/workflows/nix-action-9.0-master.yml index 758425db49..421f683bf0 100644 --- a/.github/workflows/nix-action-9.0-master.yml +++ b/.github/workflows/nix-action-9.0-master.yml @@ -491,7 +491,7 @@ jobs: mathcomp-experimental-reals: needs: - rocq-core - - mathcomp-reals + - mathcomp-analysis - mathcomp-bigenough runs-on: ubuntu-latest steps: @@ -546,9 +546,9 @@ jobs: run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-master" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-reals' + name: 'Building/fetching previous CI target: mathcomp-analysis' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "9.0-master" --argstr job "mathcomp-reals" + "9.0-master" --argstr job "mathcomp-analysis" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-bigenough' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle diff --git a/.github/workflows/nix-action-9.1-master.yml b/.github/workflows/nix-action-9.1-master.yml index 9424a3bb46..2209b9519e 100644 --- a/.github/workflows/nix-action-9.1-master.yml +++ b/.github/workflows/nix-action-9.1-master.yml @@ -491,7 +491,7 @@ jobs: mathcomp-experimental-reals: needs: - rocq-core - - mathcomp-reals + - mathcomp-analysis - mathcomp-bigenough runs-on: ubuntu-latest steps: @@ -546,9 +546,9 @@ jobs: run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.1-master" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-reals' + name: 'Building/fetching previous CI target: mathcomp-analysis' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "9.1-master" --argstr job "mathcomp-reals" + "9.1-master" --argstr job "mathcomp-analysis" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-bigenough' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle diff --git a/.github/workflows/nix-action-master.yml b/.github/workflows/nix-action-master.yml index 56b4542f8c..adb5918eec 100644 --- a/.github/workflows/nix-action-master.yml +++ b/.github/workflows/nix-action-master.yml @@ -617,7 +617,7 @@ jobs: mathcomp-experimental-reals: needs: - rocq-core - - mathcomp-reals + - mathcomp-analysis - mathcomp-bigenough runs-on: ubuntu-latest steps: @@ -672,9 +672,9 @@ jobs: run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" --argstr job "rocq-core" - if: steps.stepCheck.outputs.status != 'fetched' - name: 'Building/fetching previous CI target: mathcomp-reals' + name: 'Building/fetching previous CI target: mathcomp-analysis' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle - "master" --argstr job "mathcomp-reals" + "master" --argstr job "mathcomp-analysis" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: mathcomp-bigenough' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index ff570aeca7..e70ee2f134 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"6b32b8cd491ec44b75da86fb17e4353f2f102328" +"4a441c50de5618ef066128f9f6f84e6bc13066da" diff --git a/.nix/rocq-overlays/mathcomp-analysis-single/default.nix b/.nix/rocq-overlays/mathcomp-analysis-single/default.nix index 9b8ebde669..1232b4bf47 100644 --- a/.nix/rocq-overlays/mathcomp-analysis-single/default.nix +++ b/.nix/rocq-overlays/mathcomp-analysis-single/default.nix @@ -1,2 +1,2 @@ -{ mathcomp-analysis }: +{ mathcomp-analysis, ... }: mathcomp-analysis.override {single = true;} From 993d0fbde56014347563ae52918f9b8848c5f2d2 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 10 Jun 2026 17:21:51 +0900 Subject: [PATCH 2/3] override coq.mathcomp too --- .github/workflows/nix-action-9.0-master.yml | 4 ---- .github/workflows/nix-action-9.1-master.yml | 4 ---- .nix/config.nix | 6 ++++++ 3 files changed, 6 insertions(+), 8 deletions(-) diff --git a/.github/workflows/nix-action-9.0-master.yml b/.github/workflows/nix-action-9.0-master.yml index 421f683bf0..aba868db3f 100644 --- a/.github/workflows/nix-action-9.0-master.yml +++ b/.github/workflows/nix-action-9.0-master.yml @@ -680,10 +680,6 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-analysis-stdlib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0-master" --argstr job "mathcomp-analysis-stdlib" - - 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 - "9.0-master" --argstr job "mathcomp-algebra-tactics" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: interval' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle diff --git a/.github/workflows/nix-action-9.1-master.yml b/.github/workflows/nix-action-9.1-master.yml index 2209b9519e..185797a8ee 100644 --- a/.github/workflows/nix-action-9.1-master.yml +++ b/.github/workflows/nix-action-9.1-master.yml @@ -680,10 +680,6 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-analysis-stdlib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.1-master" --argstr job "mathcomp-analysis-stdlib" - - 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 - "9.1-master" --argstr job "mathcomp-algebra-tactics" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: interval' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle diff --git a/.nix/config.nix b/.nix/config.nix index eff51f0ffb..9aae2b1be1 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -59,6 +59,9 @@ in { }; coqPackages = common-bundle // { coq.override.version = "9.0"; + mathcomp.override.version = "master"; + mathcomp-bigenough.override.version = "master"; + mathcomp-finmap.override.version = "master"; ssprove.job = false; # not yet available for 9.1 }; }; @@ -84,6 +87,9 @@ in { }; coqPackages = common-bundle // { coq.override.version = "9.1"; + mathcomp.override.version = "master"; + mathcomp-bigenough.override.version = "master"; + mathcomp-finmap.override.version = "master"; ssprove.job = false; # not yet available for 9.1 }; }; From 2c09c413f5d7d684dd0b15b0424d532e8273bb7c Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 10 Jun 2026 17:21:51 +0900 Subject: [PATCH 3/3] override more too --- .nix/config.nix | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.nix/config.nix b/.nix/config.nix index 9aae2b1be1..7c48a67da2 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -8,6 +8,8 @@ let mathcomp-analysis-stdlib.job = true; ssprove.override.version = "main"; mathcomp-infotheo.override.version = "master"; + interval.override.version = "master"; + coquelicot.override.version = "master"; }; in { ## DO NOT CHANGE THIS