From c7e61ea4991f2827f4988df92a7b2909ecdf102a Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Mon, 23 Mar 2026 12:41:05 +0100 Subject: [PATCH] [CI] Update Nix toolbox --- .github/workflows/nix-action-rocq-9.1.yml | 40 +++++++ .github/workflows/nix-action-rocq-master.yml | 120 +++++++++++++++++++ .nix/config.nix | 4 +- .nix/coq-nix-toolbox.nix | 2 +- 4 files changed, 164 insertions(+), 2 deletions(-) diff --git a/.github/workflows/nix-action-rocq-9.1.yml b/.github/workflows/nix-action-rocq-9.1.yml index 107ad041d3..2a8c222ec5 100644 --- a/.github/workflows/nix-action-rocq-9.1.yml +++ b/.github/workflows/nix-action-rocq-9.1.yml @@ -3664,6 +3664,8 @@ jobs: needs: - coq - equations + - ExtLib + - stdlib - metarocq-utils runs-on: ubuntu-latest steps: @@ -3721,6 +3723,14 @@ jobs: name: 'Building/fetching previous CI target: equations' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.1" --argstr job "equations" + - 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 + "rocq-9.1" --argstr job "ExtLib" + - 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 + "rocq-9.1" --argstr job "stdlib" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: metarocq-utils' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -3733,6 +3743,8 @@ jobs: needs: - coq - equations + - ExtLib + - stdlib - metarocq-common runs-on: ubuntu-latest steps: @@ -3790,6 +3802,14 @@ jobs: name: 'Building/fetching previous CI target: equations' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.1" --argstr job "equations" + - 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 + "rocq-9.1" --argstr job "ExtLib" + - 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 + "rocq-9.1" --argstr job "stdlib" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: metarocq-common' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -3802,6 +3822,8 @@ jobs: needs: - coq - equations + - ExtLib + - stdlib - metarocq-template-rocq runs-on: ubuntu-latest steps: @@ -3859,6 +3881,14 @@ jobs: name: 'Building/fetching previous CI target: equations' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.1" --argstr job "equations" + - 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 + "rocq-9.1" --argstr job "ExtLib" + - 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 + "rocq-9.1" --argstr job "stdlib" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: metarocq-template-rocq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -3871,6 +3901,8 @@ jobs: needs: - coq - equations + - ExtLib + - stdlib runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -3927,6 +3959,14 @@ jobs: name: 'Building/fetching previous CI target: equations' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.1" --argstr job "equations" + - 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 + "rocq-9.1" --argstr job "ExtLib" + - 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 + "rocq-9.1" --argstr job "stdlib" - 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 2f36486b45..493e8b1119 100644 --- a/.github/workflows/nix-action-rocq-master.yml +++ b/.github/workflows/nix-action-rocq-master.yml @@ -4791,6 +4791,8 @@ jobs: needs: - coq - equations + - ExtLib + - stdlib - metarocq-safechecker-plugin - metarocq-erasure-plugin - metarocq-translations @@ -4851,6 +4853,14 @@ jobs: name: 'Building/fetching previous CI target: equations' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master" --argstr job "equations" + - 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 + "rocq-master" --argstr job "ExtLib" + - 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 + "rocq-master" --argstr job "stdlib" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: metarocq-safechecker-plugin' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -4875,6 +4885,8 @@ jobs: needs: - coq - equations + - ExtLib + - stdlib - metarocq-utils runs-on: ubuntu-latest steps: @@ -4932,6 +4944,14 @@ jobs: name: 'Building/fetching previous CI target: equations' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master" --argstr job "equations" + - 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 + "rocq-master" --argstr job "ExtLib" + - 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 + "rocq-master" --argstr job "stdlib" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: metarocq-utils' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -4944,6 +4964,8 @@ jobs: needs: - coq - equations + - ExtLib + - stdlib - metarocq-safechecker - metarocq-template-pcuic runs-on: ubuntu-latest @@ -5002,6 +5024,14 @@ jobs: name: 'Building/fetching previous CI target: equations' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master" --argstr job "equations" + - 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 + "rocq-master" --argstr job "ExtLib" + - 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 + "rocq-master" --argstr job "stdlib" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: metarocq-safechecker' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -5018,6 +5048,8 @@ jobs: needs: - coq - equations + - ExtLib + - stdlib - metarocq-template-pcuic - metarocq-erasure runs-on: ubuntu-latest @@ -5076,6 +5108,14 @@ jobs: name: 'Building/fetching previous CI target: equations' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master" --argstr job "equations" + - 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 + "rocq-master" --argstr job "ExtLib" + - 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 + "rocq-master" --argstr job "stdlib" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: metarocq-template-pcuic' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -5092,6 +5132,8 @@ jobs: needs: - coq - equations + - ExtLib + - stdlib - metarocq-common runs-on: ubuntu-latest steps: @@ -5149,6 +5191,14 @@ jobs: name: 'Building/fetching previous CI target: equations' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master" --argstr job "equations" + - 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 + "rocq-master" --argstr job "ExtLib" + - 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 + "rocq-master" --argstr job "stdlib" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: metarocq-common' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -5161,6 +5211,8 @@ jobs: needs: - coq - equations + - ExtLib + - stdlib - metarocq-template-rocq - metarocq-pcuic - metarocq-template-pcuic @@ -5220,6 +5272,14 @@ jobs: name: 'Building/fetching previous CI target: equations' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master" --argstr job "equations" + - 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 + "rocq-master" --argstr job "ExtLib" + - 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 + "rocq-master" --argstr job "stdlib" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: metarocq-template-rocq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -5240,6 +5300,8 @@ jobs: needs: - coq - equations + - ExtLib + - stdlib - metarocq-pcuic runs-on: ubuntu-latest steps: @@ -5297,6 +5359,14 @@ jobs: name: 'Building/fetching previous CI target: equations' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master" --argstr job "equations" + - 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 + "rocq-master" --argstr job "ExtLib" + - 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 + "rocq-master" --argstr job "stdlib" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: metarocq-pcuic' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -5309,6 +5379,8 @@ jobs: needs: - coq - equations + - ExtLib + - stdlib - metarocq-template-pcuic - metarocq-safechecker runs-on: ubuntu-latest @@ -5367,6 +5439,14 @@ jobs: name: 'Building/fetching previous CI target: equations' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master" --argstr job "equations" + - 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 + "rocq-master" --argstr job "ExtLib" + - 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 + "rocq-master" --argstr job "stdlib" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: metarocq-template-pcuic' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -5383,6 +5463,8 @@ jobs: needs: - coq - equations + - ExtLib + - stdlib - metarocq-template-rocq - metarocq-pcuic runs-on: ubuntu-latest @@ -5441,6 +5523,14 @@ jobs: name: 'Building/fetching previous CI target: equations' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master" --argstr job "equations" + - 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 + "rocq-master" --argstr job "ExtLib" + - 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 + "rocq-master" --argstr job "stdlib" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: metarocq-template-rocq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -5457,6 +5547,8 @@ jobs: needs: - coq - equations + - ExtLib + - stdlib - metarocq-common runs-on: ubuntu-latest steps: @@ -5514,6 +5606,14 @@ jobs: name: 'Building/fetching previous CI target: equations' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master" --argstr job "equations" + - 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 + "rocq-master" --argstr job "ExtLib" + - 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 + "rocq-master" --argstr job "stdlib" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: metarocq-common' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -5590,6 +5690,8 @@ jobs: needs: - coq - equations + - ExtLib + - stdlib - metarocq-template-rocq runs-on: ubuntu-latest steps: @@ -5647,6 +5749,14 @@ jobs: name: 'Building/fetching previous CI target: equations' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master" --argstr job "equations" + - 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 + "rocq-master" --argstr job "ExtLib" + - 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 + "rocq-master" --argstr job "stdlib" - if: steps.stepCheck.outputs.status != 'fetched' name: 'Building/fetching previous CI target: metarocq-template-rocq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle @@ -5659,6 +5769,8 @@ jobs: needs: - coq - equations + - ExtLib + - stdlib runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -5715,6 +5827,14 @@ jobs: name: 'Building/fetching previous CI target: equations' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master" --argstr job "equations" + - 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 + "rocq-master" --argstr job "ExtLib" + - 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 + "rocq-master" --argstr job "stdlib" - 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 3d0dc0c4e5..272c34bd26 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -250,14 +250,16 @@ with builtins; with (import {}).lib; { name = p; value.override.version = "main"; })) // { coq-elpi.override.version = "master"; - coq-elpi.override.elpi-version = "3.6.1"; + coq-elpi.override.elpi-version = "3.6.2"; tlc.override.version = "master-for-coq-ci"; smtcoq-trakt.override.version = "with-trakt-coq-master"; coq-tools.override.version = "proux01:coq_19955"; stdlib-refman-html.job = true; iris-examples.job = false; # Currently broken jasmin.job = false; # Currently broken, c.f., https://github.com/rocq-prover/rocq/pull/20589 + CakeMLExtraction.job = false; # not in Rocq CI ceres-bs.job = false; # not in Rocq CI + CertiRocq.job = false; # not in Rocq CI ConCert.job = false; # not in Rocq CI ElmExtraction.job = false; # not in Rocq CI RustExtraction.job = false; # not in Rocq CI diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index 019107584e..b6d32e70df 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"307b3a341ab73125c1c9e65603b7d6b7447539e4" +"3b7baf61aa95441d62332d7fdad562a61a125f80"