From 89c3331a7fe4a3551b79fdfcb977665b9e706459 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 19 Jun 2026 08:28:04 +0200 Subject: [PATCH 1/2] Adapt to rocq/21743 (readd Jasmin in CI) Adapt to https://github.com/rocq-prover/rocq/pull/21743 --- .github/workflows/nix-action-rocq-master.yml | 69 ++++++++++++++++++++ .nix/config.nix | 2 +- 2 files changed, 70 insertions(+), 1 deletion(-) diff --git a/.github/workflows/nix-action-rocq-master.yml b/.github/workflows/nix-action-rocq-master.yml index e2de313a82..e08284fdf4 100644 --- a/.github/workflows/nix-action-rocq-master.yml +++ b/.github/workflows/nix-action-rocq-master.yml @@ -2762,6 +2762,75 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master" --argstr job "itree-io" + jasmin: + needs: + - coq + - mathcomp-word + - ITree + 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 coq + uses: cachix/cachix-action@v16 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq-community, math-comp + name: coq + - id: stepGetDerivation + name: Getting derivation for current job (jasmin) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"rocq-master\" --argstr job \"jasmin\" \\\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-master" --argstr job "coq" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: mathcomp-word' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-master" --argstr job "mathcomp-word" + - if: steps.stepCheck.outputs.status != 'fetched' + name: 'Building/fetching previous CI target: ITree' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-master" --argstr job "ITree" + - 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 "jasmin" json: needs: - coq diff --git a/.nix/config.nix b/.nix/config.nix index cfd3e56dc7..df251242a2 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -186,6 +186,7 @@ with builtins; with (import {}).lib; { "fiat-crypto-ocaml" "iris" "iris-examples" + "jasmin" "metacoq" "metacoq-common" "metacoq-erasure" @@ -224,7 +225,6 @@ with builtins; with (import {}).lib; { stdlib-refman-html.job = true; rocq-elpi.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 From 23a80e8886006bc571b51755b1e4d20160d2253e Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 19 Jun 2026 08:25:27 +0200 Subject: [PATCH 2/2] Adapt to rocq/22137 (add Trakt to CI) Adapt to https://github.com/rocq-prover/rocq/pull/22137 --- .github/workflows/nix-action-rocq-9.1.yml | 68 +++++++++++++++++++ .github/workflows/nix-action-rocq-9.2.yml | 68 +++++++++++++++++++ .github/workflows/nix-action-rocq-master.yml | 69 ++++++++++++++++++++ .nix/config.nix | 3 +- 4 files changed, 206 insertions(+), 2 deletions(-) diff --git a/.github/workflows/nix-action-rocq-9.1.yml b/.github/workflows/nix-action-rocq-9.1.yml index 0542c3d343..4b655c446c 100644 --- a/.github/workflows/nix-action-rocq-9.1.yml +++ b/.github/workflows/nix-action-rocq-9.1.yml @@ -3795,6 +3795,74 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.1" --argstr job "stdpp" + trakt: + needs: + - coq + - stdlib + 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 coq + uses: cachix/cachix-action@v16 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq-community, math-comp + name: coq + - id: stepGetDerivation + name: Getting derivation for current job (trakt) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"rocq-9.1\" --argstr job \"trakt\" \\\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: coq-elpi' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle + "rocq-9.1" --argstr job "coq-elpi" + - 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 + "rocq-9.1" --argstr job "trakt" unicoq: needs: - coq diff --git a/.github/workflows/nix-action-rocq-9.2.yml b/.github/workflows/nix-action-rocq-9.2.yml index 3dadfc983b..2564d3ef92 100644 --- a/.github/workflows/nix-action-rocq-9.2.yml +++ b/.github/workflows/nix-action-rocq-9.2.yml @@ -2352,6 +2352,74 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.2" --argstr job "stdpp" + trakt: + needs: + - coq + - stdlib + 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 coq + uses: cachix/cachix-action@v16 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq-community, math-comp + name: coq + - id: stepGetDerivation + name: Getting derivation for current job (trakt) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"rocq-9.2\" --argstr job \"trakt\" \\\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.2" --argstr job "coq" + - 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 + "rocq-9.2" --argstr job "coq-elpi" + - 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.2" --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 + "rocq-9.2" --argstr job "trakt" unicoq: needs: - coq diff --git a/.github/workflows/nix-action-rocq-master.yml b/.github/workflows/nix-action-rocq-master.yml index e08284fdf4..ecda28fa9f 100644 --- a/.github/workflows/nix-action-rocq-master.yml +++ b/.github/workflows/nix-action-rocq-master.yml @@ -6082,6 +6082,75 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-master" --argstr job "stdpp" + trakt: + needs: + - coq + - coq-elpi + - stdlib + 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 coq + uses: cachix/cachix-action@v16 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq-community, math-comp + name: coq + - id: stepGetDerivation + name: Getting derivation for current job (trakt) + run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle + \"rocq-master\" --argstr job \"trakt\" \\\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-master" --argstr job "coq" + - 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 + "rocq-master" --argstr job "coq-elpi" + - 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 + "rocq-master" --argstr job "trakt" unicoq: needs: - coq diff --git a/.nix/config.nix b/.nix/config.nix index df251242a2..6b50cdb2ca 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -156,6 +156,7 @@ with builtins; with (import {}).lib; { "sf" "simple-io" "stdpp" + "trakt" "unicoq" "VST" ]; @@ -268,8 +269,6 @@ with builtins; with (import {}).lib; { # * : is such that this will use the branch # from https://github.com// sf.job = false; # temporarily disactivated in Rocq CI - trakt.job = false; # temporarily disactivated in Rocq CI - smtcoq-trakt.job = false; # temporarily disactivated in Rocq CI }; common-bundles = listToAttrs (forEach rocq-master (p: { name = p; value.override.version = "master"; }));