From 79e5e66e4c0cf2c4f44d9f5e27a4da1b37674737 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Mon, 4 Nov 2024 13:19:09 +0100 Subject: [PATCH 1/4] Renaming coq-mathcomp-altreals to experimental-reals Following discussion during last mathcomp sharing days --- .nix/config.nix | 2 +- CHANGELOG_UNRELEASED.md | 2 +- _CoqProject | 12 ++++++------ ...eals.opam => coq-mathcomp-experimental-reals.opam | 6 +++--- {altreals => experimental_reals}/LICENSE | 0 {altreals => experimental_reals}/Make | 2 +- {altreals => experimental_reals}/Makefile | 0 {altreals => experimental_reals}/dedekind.v | 0 {altreals => experimental_reals}/discrete.v | 0 {altreals => experimental_reals}/distr.v | 0 {altreals => experimental_reals}/realseq.v | 0 {altreals => experimental_reals}/realsum.v | 0 {altreals => experimental_reals}/xfinmap.v | 0 13 files changed, 12 insertions(+), 12 deletions(-) rename coq-mathcomp-altreals.opam => coq-mathcomp-experimental-reals.opam (86%) rename {altreals => experimental_reals}/LICENSE (100%) rename {altreals => experimental_reals}/Make (88%) rename {altreals => experimental_reals}/Makefile (100%) rename {altreals => experimental_reals}/dedekind.v (100%) rename {altreals => experimental_reals}/discrete.v (100%) rename {altreals => experimental_reals}/distr.v (100%) rename {altreals => experimental_reals}/realseq.v (100%) rename {altreals => experimental_reals}/realsum.v (100%) rename {altreals => experimental_reals}/xfinmap.v (100%) diff --git a/.nix/config.nix b/.nix/config.nix index 4041d330f..ef948d907 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -3,7 +3,7 @@ let mathcomp-classical.job = true; mathcomp-reals.job = true; mathcomp-analysis.job = true; - mathcomp-altreals.job = true; + mathcomp-experimental-reals.job = true; mathcomp-reals-stdlib.job = true; mathcomp-analysis-stdlib.job = true; ssprove.job = false; diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 2b9213098..743c396cc 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -20,7 +20,7 @@ - in file `separation_axioms.v`, + new lemmas `compact_normal_local`, and `compact_normal`. -- package `coq-mathcomp-altreals` depending on `coq-mathcomp-reals` +- package `coq-mathcomp-experimental-reals` depending on `coq-mathcomp-reals` with files + `xfinmap.v` + `discrete.v` diff --git a/_CoqProject b/_CoqProject index 4a9bd2415..febad3bd7 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,7 +1,7 @@ -Q classical mathcomp.classical -Q reals mathcomp.reals -Q reals_stdlib mathcomp.reals_stdlib --Q altreals mathcomp.altreals +-Q experimental_reals mathcomp.experimental_reals -Q theories mathcomp.analysis -Q analysis_stdlib mathcomp.analysis_stdlib @@ -32,11 +32,11 @@ reals/itv.v reals/prodnormedzmodule.v reals/nsatz_realtype.v reals/all_reals.v -altreals/xfinmap.v -altreals/discrete.v -altreals/realseq.v -altreals/realsum.v -altreals/distr.v +experimental_reals/xfinmap.v +experimental_reals/discrete.v +experimental_reals/realseq.v +experimental_reals/realsum.v +experimental_reals/distr.v reals_stdlib/Rstruct.v theories/all_analysis.v theories/landau.v diff --git a/coq-mathcomp-altreals.opam b/coq-mathcomp-experimental-reals.opam similarity index 86% rename from coq-mathcomp-altreals.opam rename to coq-mathcomp-experimental-reals.opam index 41c7c1a1e..017951fdc 100644 --- a/coq-mathcomp-altreals.opam +++ b/coq-mathcomp-experimental-reals.opam @@ -12,8 +12,8 @@ description: """ This repository contains a library for alternative real numbers for the Coq proof-assistant and using the Mathematical Components library.""" -build: [make "-C" "altreals" "-j%{jobs}%"] -install: [make "-C" "altreals" "install"] +build: [make "-C" "experimental_reals" "-j%{jobs}%"] +install: [make "-C" "experimental_reals" "install"] depends: [ "coq-mathcomp-reals" { = version} "coq-mathcomp-bigenough" { (>= "1.0.0") } @@ -23,7 +23,7 @@ tags: [ "category:Mathematics/Real Numbers" "keyword:real numbers" "keyword:reals" - "logpath:mathcomp.altreals" + "logpath:mathcomp.experimental_reals" ] authors: [ "Reynald Affeldt" diff --git a/altreals/LICENSE b/experimental_reals/LICENSE similarity index 100% rename from altreals/LICENSE rename to experimental_reals/LICENSE diff --git a/altreals/Make b/experimental_reals/Make similarity index 88% rename from altreals/Make rename to experimental_reals/Make index 85e6747e8..5d0d192b8 100644 --- a/altreals/Make +++ b/experimental_reals/Make @@ -1,4 +1,4 @@ --Q . mathcomp.altreals +-Q . mathcomp.experimental_reals -arg -w -arg -parsing -arg -w -arg +undeclared-scope diff --git a/altreals/Makefile b/experimental_reals/Makefile similarity index 100% rename from altreals/Makefile rename to experimental_reals/Makefile diff --git a/altreals/dedekind.v b/experimental_reals/dedekind.v similarity index 100% rename from altreals/dedekind.v rename to experimental_reals/dedekind.v diff --git a/altreals/discrete.v b/experimental_reals/discrete.v similarity index 100% rename from altreals/discrete.v rename to experimental_reals/discrete.v diff --git a/altreals/distr.v b/experimental_reals/distr.v similarity index 100% rename from altreals/distr.v rename to experimental_reals/distr.v diff --git a/altreals/realseq.v b/experimental_reals/realseq.v similarity index 100% rename from altreals/realseq.v rename to experimental_reals/realseq.v diff --git a/altreals/realsum.v b/experimental_reals/realsum.v similarity index 100% rename from altreals/realsum.v rename to experimental_reals/realsum.v diff --git a/altreals/xfinmap.v b/experimental_reals/xfinmap.v similarity index 100% rename from altreals/xfinmap.v rename to experimental_reals/xfinmap.v From 25e9676f53309843b5445a88f099ad9f8740a12c Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Mon, 4 Nov 2024 13:26:51 +0100 Subject: [PATCH 2/4] Update OPAM package descriptions --- coq-mathcomp-analysis-stdlib.opam | 2 +- coq-mathcomp-analysis.opam | 4 +--- coq-mathcomp-classical.opam | 1 + coq-mathcomp-experimental-reals.opam | 7 +++++-- coq-mathcomp-reals-stdlib.opam | 2 +- coq-mathcomp-reals.opam | 3 ++- 6 files changed, 11 insertions(+), 8 deletions(-) diff --git a/coq-mathcomp-analysis-stdlib.opam b/coq-mathcomp-analysis-stdlib.opam index 8bd287f1c..ef8ac571e 100644 --- a/coq-mathcomp-analysis-stdlib.opam +++ b/coq-mathcomp-analysis-stdlib.opam @@ -9,7 +9,7 @@ license: "CECILL-C" synopsis: "A library to link real numbers from mathematical components and Stdlib" description: """ -This repository contains a library to link real numbers for +This package contains a library to link real numbers for the Coq proof-assistant using the Mathematical Components library and Stdlib.""" build: [make "-C" "analysis_stdlib" "-j%{jobs}%"] diff --git a/coq-mathcomp-analysis.opam b/coq-mathcomp-analysis.opam index 1e3613fb2..a0890eb50 100644 --- a/coq-mathcomp-analysis.opam +++ b/coq-mathcomp-analysis.opam @@ -9,7 +9,7 @@ license: "CECILL-C" synopsis: "An analysis library for mathematical components" description: """ -This repository contains an experimental library for real analysis for +This package contains a library for real analysis for the Coq proof-assistant and using the Mathematical Components library.""" build: [make "-C" "theories" "-j%{jobs}%"] @@ -24,8 +24,6 @@ depends: [ tags: [ "category:Mathematics/Real Calculus and Topology" "keyword:analysis" - "keyword:extended real numbers" - "keyword:filter" "keyword:Cantor" "keyword:topology" "keyword:real numbers" diff --git a/coq-mathcomp-classical.opam b/coq-mathcomp-classical.opam index 0db81a86d..4de111457 100644 --- a/coq-mathcomp-classical.opam +++ b/coq-mathcomp-classical.opam @@ -31,6 +31,7 @@ tags: [ "keyword:set theory" "keyword:function" "keyword:cardinal" + "keyword:filter" "logpath:mathcomp.classical" ] authors: [ diff --git a/coq-mathcomp-experimental-reals.opam b/coq-mathcomp-experimental-reals.opam index 017951fdc..b9053fef9 100644 --- a/coq-mathcomp-experimental-reals.opam +++ b/coq-mathcomp-experimental-reals.opam @@ -9,8 +9,11 @@ license: "CECILL-C" synopsis: "A library for alternative real numbers for mathematical components" description: """ -This repository contains a library for alternative real numbers for -the Coq proof-assistant and using the Mathematical Components library.""" +This package contains an experiment along real numbers +made at the beginning of the MathComp-Analysis library +(which now offers the coq-mathcomp-reals package). + +Beware that this still contains a few Admitted.""" build: [make "-C" "experimental_reals" "-j%{jobs}%"] install: [make "-C" "experimental_reals" "install"] diff --git a/coq-mathcomp-reals-stdlib.opam b/coq-mathcomp-reals-stdlib.opam index e57613a6c..afba7ee5a 100644 --- a/coq-mathcomp-reals-stdlib.opam +++ b/coq-mathcomp-reals-stdlib.opam @@ -9,7 +9,7 @@ license: "CECILL-C" synopsis: "A library to link real numbers from mathematical components and Stdlib" description: """ -This repository contains a library to link real numbers for +This package contains a library to link real numbers for the Coq proof-assistant using the Mathematical Components library and Stdlib.""" build: [make "-C" "reals_stdlib" "-j%{jobs}%"] diff --git a/coq-mathcomp-reals.opam b/coq-mathcomp-reals.opam index f7e0955c2..e718a176e 100644 --- a/coq-mathcomp-reals.opam +++ b/coq-mathcomp-reals.opam @@ -9,7 +9,7 @@ license: "CECILL-C" synopsis: "A library for real numbers for mathematical components" description: """ -This repository contains a library for real numbers for +This package contains a library for real numbers for the Coq proof-assistant and using the Mathematical Components library.""" build: [make "-C" "reals" "-j%{jobs}%"] @@ -22,6 +22,7 @@ tags: [ "category:Mathematics/Real Numbers" "keyword:real numbers" "keyword:reals" + "keyword:extended real numbers" "logpath:mathcomp.reals" ] authors: [ From 2e0c66572ae5223debdb3a261cc8fb34ff1e969b Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Mon, 4 Nov 2024 13:19:33 +0100 Subject: [PATCH 3/4] Update MANIFEST --- MANIFEST | 32 ++++++++++++++++++++++++++++---- 1 file changed, 28 insertions(+), 4 deletions(-) diff --git a/MANIFEST b/MANIFEST index fe2cb62c8..60c7193e5 100644 --- a/MANIFEST +++ b/MANIFEST @@ -10,18 +10,42 @@ NIX.md Licence_CeCILL-C_V1-en.txt # Build and meta data +reals_stdlib/Make +reals_stdlib/Makefile +analysis_stdlib/Make +analysis_stdlib/Makefile +classical/Make +classical/Makefile +Makefile.common +experimental_reals/Make +experimental_reals/Makefile +theories/Make +theories/Makefile +reals/Make +reals/Makefile Makefile Makefile.common _CoqProject .gitignore .travis.yml -opam -shell.nix +coq-mathcomp-analysis-stdlib.opam +coq-mathcomp-analysis.opam +coq-mathcomp-classical.opam +coq-mathcomp-experimental-reals.opam +coq-mathcomp-reals-stdlib.opam +coq-mathcomp-reals.opam +default.nix # Theory files +analysis_stdlib/*.v +analysis_stdlib/showcase/*.v +classical/*.v +experimental_reals/*.v +reals/*.v +reals_stdlib/*.v theories/*.v -theories/altreals/*.v -theories/misc/*.v +theories/showcase/*.v +theories/topology_theory/*.v # Build scripts scripts/install-sh From ed78b09c41051a6beefa4f0e0ffb134f6970117d Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Mon, 4 Nov 2024 13:43:22 +0100 Subject: [PATCH 4/4] [CI] Update Nix toolbox --- .github/workflows/nix-action-8.19.yml | 352 ++++++++--------- .github/workflows/nix-action-8.20.yml | 352 ++++++++--------- .github/workflows/nix-action-master.yml | 484 ++++++++++++------------ .nix/coq-nix-toolbox.nix | 2 +- 4 files changed, 595 insertions(+), 595 deletions(-) diff --git a/.github/workflows/nix-action-8.19.yml b/.github/workflows/nix-action-8.19.yml index 840838ce5..1a2eee686 100644 --- a/.github/workflows/nix-action-8.19.yml +++ b/.github/workflows/nix-action-8.19.yml @@ -4,23 +4,23 @@ jobs: 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" + 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@v4 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" + 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@v4 with: @@ -38,8 +38,8 @@ jobs: name: math-comp - id: stepCheck name: Checking presence of CI target coq - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.19\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\ + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"8.19\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' @@ -52,23 +52,23 @@ jobs: 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" + 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@v4 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" + 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@v4 with: @@ -86,8 +86,8 @@ jobs: name: math-comp - id: stepCheck name: Checking presence of CI target mathcomp - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.19\" --argstr job \"mathcomp\" \\\n --dry-run 2>&1 > /dev/null)\n\ + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"8.19\" --argstr job \"mathcomp\" \\\n --dry-run 2>&1 > /dev/null)\n echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' @@ -126,30 +126,30 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr job "mathcomp" - mathcomp-altreals: + mathcomp-analysis: needs: - coq - mathcomp-reals 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" + 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@v4 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" + 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@v4 with: @@ -166,11 +166,11 @@ jobs: extraPullNames: coq, coq-community name: math-comp - id: stepCheck - name: Checking presence of CI target mathcomp-altreals - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.19\" --argstr job \"mathcomp-altreals\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\ - built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" + name: Checking presence of CI target mathcomp-analysis + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"8.19\" --argstr job \"mathcomp-analysis\" \\\n --dry-run 2>&1 > + /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\"\ + \ | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr @@ -179,6 +179,10 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-reals' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr job "mathcomp-reals" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-field' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp-field" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-bigenough' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr @@ -190,31 +194,30 @@ jobs: - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr - job "mathcomp-altreals" - mathcomp-analysis: + job "mathcomp-analysis" + mathcomp-analysis-single: needs: - coq - - mathcomp-reals 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" + 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@v4 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" + 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@v4 with: @@ -231,19 +234,27 @@ jobs: extraPullNames: coq, coq-community name: math-comp - id: stepCheck - name: Checking presence of CI target mathcomp-analysis - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.19\" --argstr job \"mathcomp-analysis\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\ - built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" + name: Checking presence of CI target mathcomp-analysis-single + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"8.19\" --argstr job \"mathcomp-analysis-single\" \\\n --dry-run + 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep + \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr job "coq" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-reals' + name: 'Building/fetching previous CI target: mathcomp-algebra' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr - job "mathcomp-reals" + job "mathcomp-algebra" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-finmap' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp-finmap" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-bigenough' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr + job "mathcomp-bigenough" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-field' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr @@ -259,30 +270,32 @@ jobs: - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr - job "mathcomp-analysis" - mathcomp-analysis-single: + job "mathcomp-analysis-single" + mathcomp-analysis-stdlib: needs: - coq + - mathcomp-analysis + - mathcomp-reals-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" + 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@v4 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" + 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@v4 with: @@ -299,35 +312,23 @@ jobs: extraPullNames: coq, coq-community name: math-comp - id: stepCheck - name: Checking presence of CI target mathcomp-analysis-single - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.19\" --argstr job \"mathcomp-analysis-single\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" + name: Checking presence of CI target mathcomp-analysis-stdlib + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"8.19\" --argstr job \"mathcomp-analysis-stdlib\" \\\n --dry-run + 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep + \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr job "coq" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr - job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-finmap' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr - job "mathcomp-finmap" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-bigenough' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr - job "mathcomp-bigenough" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' + name: 'Building/fetching previous CI target: mathcomp-analysis' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr - job "mathcomp-field" + job "mathcomp-analysis" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-bigenough' + name: 'Building/fetching previous CI target: mathcomp-reals-stdlib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr - job "mathcomp-bigenough" + job "mathcomp-reals-stdlib" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: hierarchy-builder' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr @@ -335,32 +336,30 @@ jobs: - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr - job "mathcomp-analysis-single" - mathcomp-analysis-stdlib: + job "mathcomp-analysis-stdlib" + mathcomp-classical: needs: - coq - - mathcomp-analysis - - mathcomp-reals-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" + 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@v4 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" + 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@v4 with: @@ -377,23 +376,23 @@ jobs: extraPullNames: coq, coq-community name: math-comp - id: stepCheck - name: Checking presence of CI target mathcomp-analysis-stdlib - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.19\" --argstr job \"mathcomp-analysis-stdlib\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" + name: Checking presence of CI target mathcomp-classical + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"8.19\" --argstr job \"mathcomp-classical\" \\\n --dry-run 2>&1 + > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\"\ + \ | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr job "coq" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-analysis' + name: 'Building/fetching previous CI target: mathcomp-algebra' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr - job "mathcomp-analysis" + job "mathcomp-algebra" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-reals-stdlib' + name: 'Building/fetching previous CI target: mathcomp-finmap' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr - job "mathcomp-reals-stdlib" + job "mathcomp-finmap" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: hierarchy-builder' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr @@ -401,30 +400,31 @@ jobs: - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr - job "mathcomp-analysis-stdlib" - mathcomp-classical: + job "mathcomp-classical" + mathcomp-experimental-reals: needs: - coq + - mathcomp-reals 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" + 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@v4 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" + 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@v4 with: @@ -441,23 +441,23 @@ jobs: extraPullNames: coq, coq-community name: math-comp - id: stepCheck - name: Checking presence of CI target mathcomp-classical - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.19\" --argstr job \"mathcomp-classical\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\ - built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" + name: Checking presence of CI target mathcomp-experimental-reals + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"8.19\" --argstr job \"mathcomp-experimental-reals\" \\\n --dry-run + 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep + \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr job "coq" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' + name: 'Building/fetching previous CI target: mathcomp-reals' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr - job "mathcomp-algebra" + job "mathcomp-reals" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-finmap' + name: 'Building/fetching previous CI target: mathcomp-bigenough' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr - job "mathcomp-finmap" + job "mathcomp-bigenough" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: hierarchy-builder' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr @@ -465,7 +465,7 @@ jobs: - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr - job "mathcomp-classical" + job "mathcomp-experimental-reals" mathcomp-reals: needs: - coq @@ -473,23 +473,23 @@ jobs: 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" + 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@v4 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" + 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@v4 with: @@ -507,10 +507,10 @@ jobs: name: math-comp - id: stepCheck name: Checking presence of CI target mathcomp-reals - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.19\" --argstr job \"mathcomp-reals\" \\\n --dry-run 2>&1 >\ - \ /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\"\ - \ | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"8.19\" --argstr job \"mathcomp-reals\" \\\n --dry-run 2>&1 > /dev/null)\n + echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ + s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr @@ -534,23 +534,23 @@ jobs: 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" + 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@v4 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" + 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@v4 with: @@ -568,10 +568,10 @@ jobs: name: math-comp - id: stepCheck name: Checking presence of CI target mathcomp-reals-stdlib - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.19\" --argstr job \"mathcomp-reals-stdlib\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"8.19\" --argstr job \"mathcomp-reals-stdlib\" \\\n --dry-run 2>&1 + > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\"\ + \ | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr @@ -589,7 +589,7 @@ jobs: run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr job "mathcomp-reals-stdlib" name: Nix CI for bundle 8.19 -'on': +on: pull_request: paths: - .github/workflows/nix-action-8.19.yml diff --git a/.github/workflows/nix-action-8.20.yml b/.github/workflows/nix-action-8.20.yml index a22145e9a..df3067981 100644 --- a/.github/workflows/nix-action-8.20.yml +++ b/.github/workflows/nix-action-8.20.yml @@ -4,23 +4,23 @@ jobs: 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" + 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@v4 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" + 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@v4 with: @@ -38,8 +38,8 @@ jobs: name: math-comp - id: stepCheck name: Checking presence of CI target coq - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.20\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\ + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"8.20\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' @@ -52,23 +52,23 @@ jobs: 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" + 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@v4 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" + 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@v4 with: @@ -86,8 +86,8 @@ jobs: name: math-comp - id: stepCheck name: Checking presence of CI target mathcomp - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.20\" --argstr job \"mathcomp\" \\\n --dry-run 2>&1 > /dev/null)\n\ + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"8.20\" --argstr job \"mathcomp\" \\\n --dry-run 2>&1 > /dev/null)\n echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' @@ -126,30 +126,30 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr job "mathcomp" - mathcomp-altreals: + mathcomp-analysis: needs: - coq - mathcomp-reals 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" + 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@v4 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" + 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@v4 with: @@ -166,11 +166,11 @@ jobs: extraPullNames: coq, coq-community name: math-comp - id: stepCheck - name: Checking presence of CI target mathcomp-altreals - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.20\" --argstr job \"mathcomp-altreals\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\ - built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" + name: Checking presence of CI target mathcomp-analysis + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"8.20\" --argstr job \"mathcomp-analysis\" \\\n --dry-run 2>&1 > + /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\"\ + \ | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr @@ -179,6 +179,10 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-reals' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr job "mathcomp-reals" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-field' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr + job "mathcomp-field" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-bigenough' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr @@ -190,31 +194,30 @@ jobs: - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr - job "mathcomp-altreals" - mathcomp-analysis: + job "mathcomp-analysis" + mathcomp-analysis-single: needs: - coq - - mathcomp-reals 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" + 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@v4 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" + 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@v4 with: @@ -231,19 +234,27 @@ jobs: extraPullNames: coq, coq-community name: math-comp - id: stepCheck - name: Checking presence of CI target mathcomp-analysis - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.20\" --argstr job \"mathcomp-analysis\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\ - built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" + name: Checking presence of CI target mathcomp-analysis-single + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"8.20\" --argstr job \"mathcomp-analysis-single\" \\\n --dry-run + 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep + \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr job "coq" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-reals' + name: 'Building/fetching previous CI target: mathcomp-algebra' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr - job "mathcomp-reals" + job "mathcomp-algebra" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-finmap' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr + job "mathcomp-finmap" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-bigenough' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr + job "mathcomp-bigenough" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: mathcomp-field' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr @@ -259,30 +270,32 @@ jobs: - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr - job "mathcomp-analysis" - mathcomp-analysis-single: + job "mathcomp-analysis-single" + mathcomp-analysis-stdlib: needs: - coq + - mathcomp-analysis + - mathcomp-reals-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" + 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@v4 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" + 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@v4 with: @@ -299,35 +312,23 @@ jobs: extraPullNames: coq, coq-community name: math-comp - id: stepCheck - name: Checking presence of CI target mathcomp-analysis-single - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.20\" --argstr job \"mathcomp-analysis-single\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" + name: Checking presence of CI target mathcomp-analysis-stdlib + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"8.20\" --argstr job \"mathcomp-analysis-stdlib\" \\\n --dry-run + 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep + \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr job "coq" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr - job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-finmap' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr - job "mathcomp-finmap" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-bigenough' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr - job "mathcomp-bigenough" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' + name: 'Building/fetching previous CI target: mathcomp-analysis' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr - job "mathcomp-field" + job "mathcomp-analysis" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-bigenough' + name: 'Building/fetching previous CI target: mathcomp-reals-stdlib' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr - job "mathcomp-bigenough" + job "mathcomp-reals-stdlib" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: hierarchy-builder' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr @@ -335,32 +336,30 @@ jobs: - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr - job "mathcomp-analysis-single" - mathcomp-analysis-stdlib: + job "mathcomp-analysis-stdlib" + mathcomp-classical: needs: - coq - - mathcomp-analysis - - mathcomp-reals-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" + 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@v4 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" + 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@v4 with: @@ -377,23 +376,23 @@ jobs: extraPullNames: coq, coq-community name: math-comp - id: stepCheck - name: Checking presence of CI target mathcomp-analysis-stdlib - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.20\" --argstr job \"mathcomp-analysis-stdlib\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" + name: Checking presence of CI target mathcomp-classical + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"8.20\" --argstr job \"mathcomp-classical\" \\\n --dry-run 2>&1 + > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\"\ + \ | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr job "coq" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-analysis' + name: 'Building/fetching previous CI target: mathcomp-algebra' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr - job "mathcomp-analysis" + job "mathcomp-algebra" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-reals-stdlib' + name: 'Building/fetching previous CI target: mathcomp-finmap' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr - job "mathcomp-reals-stdlib" + job "mathcomp-finmap" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: hierarchy-builder' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr @@ -401,30 +400,31 @@ jobs: - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr - job "mathcomp-analysis-stdlib" - mathcomp-classical: + job "mathcomp-classical" + mathcomp-experimental-reals: needs: - coq + - mathcomp-reals 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" + 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@v4 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" + 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@v4 with: @@ -441,23 +441,23 @@ jobs: extraPullNames: coq, coq-community name: math-comp - id: stepCheck - name: Checking presence of CI target mathcomp-classical - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.20\" --argstr job \"mathcomp-classical\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\ - built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" + name: Checking presence of CI target mathcomp-experimental-reals + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"8.20\" --argstr job \"mathcomp-experimental-reals\" \\\n --dry-run + 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep + \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr job "coq" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' + name: 'Building/fetching previous CI target: mathcomp-reals' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr - job "mathcomp-algebra" + job "mathcomp-reals" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-finmap' + name: 'Building/fetching previous CI target: mathcomp-bigenough' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr - job "mathcomp-finmap" + job "mathcomp-bigenough" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: hierarchy-builder' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr @@ -465,7 +465,7 @@ jobs: - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr - job "mathcomp-classical" + job "mathcomp-experimental-reals" mathcomp-reals: needs: - coq @@ -473,23 +473,23 @@ jobs: 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" + 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@v4 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" + 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@v4 with: @@ -507,10 +507,10 @@ jobs: name: math-comp - id: stepCheck name: Checking presence of CI target mathcomp-reals - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.20\" --argstr job \"mathcomp-reals\" \\\n --dry-run 2>&1 >\ - \ /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\"\ - \ | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"8.20\" --argstr job \"mathcomp-reals\" \\\n --dry-run 2>&1 > /dev/null)\n + echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ + s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr @@ -534,23 +534,23 @@ jobs: 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" + 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@v4 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" + 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@v4 with: @@ -568,10 +568,10 @@ jobs: name: math-comp - id: stepCheck name: Checking presence of CI target mathcomp-reals-stdlib - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"8.20\" --argstr job \"mathcomp-reals-stdlib\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"8.20\" --argstr job \"mathcomp-reals-stdlib\" \\\n --dry-run 2>&1 + > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\"\ + \ | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr @@ -589,7 +589,7 @@ jobs: run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr job "mathcomp-reals-stdlib" name: Nix CI for bundle 8.20 -'on': +on: pull_request: paths: - .github/workflows/nix-action-8.20.yml diff --git a/.github/workflows/nix-action-master.yml b/.github/workflows/nix-action-master.yml index cbf298442..6145c9e2d 100644 --- a/.github/workflows/nix-action-master.yml +++ b/.github/workflows/nix-action-master.yml @@ -4,23 +4,23 @@ jobs: 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" + 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@v4 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" + 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@v4 with: @@ -38,8 +38,8 @@ jobs: name: math-comp - id: stepCheck name: Checking presence of CI target coq - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"master\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\ + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"master\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' @@ -52,23 +52,23 @@ jobs: 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" + 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@v4 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" + 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@v4 with: @@ -86,8 +86,8 @@ jobs: name: math-comp - id: stepCheck name: Checking presence of CI target coq-elpi - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"master\" --argstr job \"coq-elpi\" \\\n --dry-run 2>&1 > /dev/null)\n\ + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"master\" --argstr job \"coq-elpi\" \\\n --dry-run 2>&1 > /dev/null)\n echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' @@ -105,23 +105,23 @@ jobs: 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" + 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@v4 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" + 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@v4 with: @@ -139,10 +139,10 @@ jobs: name: math-comp - id: stepCheck name: Checking presence of CI target hierarchy-builder - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"master\" --argstr job \"hierarchy-builder\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\ - built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"master\" --argstr job \"hierarchy-builder\" \\\n --dry-run 2>&1 + > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\"\ + \ | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" @@ -162,23 +162,23 @@ jobs: 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" + 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@v4 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" + 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@v4 with: @@ -196,8 +196,8 @@ jobs: name: math-comp - id: stepCheck name: Checking presence of CI target mathcomp - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"master\" --argstr job \"mathcomp\" \\\n --dry-run 2>&1 > /dev/null)\n\ + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"master\" --argstr job \"mathcomp\" \\\n --dry-run 2>&1 > /dev/null)\n echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' @@ -236,73 +236,6 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" --argstr job "mathcomp" - mathcomp-altreals: - needs: - - coq - - mathcomp-reals - - mathcomp-bigenough - - hierarchy-builder - 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@v4 - 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@v4 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v27 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup math-comp - uses: cachix/cachix-action@v15 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community - name: math-comp - - id: stepCheck - name: Checking presence of CI target mathcomp-altreals - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"master\" --argstr job \"mathcomp-altreals\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\ - built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-reals' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" - --argstr job "mathcomp-reals" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-bigenough' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" - --argstr job "mathcomp-bigenough" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: hierarchy-builder' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" - --argstr job "hierarchy-builder" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" - --argstr job "mathcomp-altreals" mathcomp-analysis: needs: - coq @@ -312,23 +245,23 @@ jobs: 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" + 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@v4 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" + 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@v4 with: @@ -346,10 +279,10 @@ jobs: name: math-comp - id: stepCheck name: Checking presence of CI target mathcomp-analysis - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"master\" --argstr job \"mathcomp-analysis\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\ - built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"master\" --argstr job \"mathcomp-analysis\" \\\n --dry-run 2>&1 + > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\"\ + \ | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" @@ -384,23 +317,23 @@ jobs: 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" + 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@v4 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" + 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@v4 with: @@ -418,10 +351,10 @@ jobs: name: math-comp - id: stepCheck name: Checking presence of CI target mathcomp-analysis-single - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"master\" --argstr job \"mathcomp-analysis-single\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"master\" --argstr job \"mathcomp-analysis-single\" \\\n --dry-run + 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep + \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" @@ -463,23 +396,23 @@ jobs: 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" + 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@v4 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" + 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@v4 with: @@ -497,10 +430,10 @@ jobs: name: math-comp - id: stepCheck name: Checking presence of CI target mathcomp-analysis-stdlib - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"master\" --argstr job \"mathcomp-analysis-stdlib\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"master\" --argstr job \"mathcomp-analysis-stdlib\" \\\n --dry-run + 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep + \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" @@ -527,23 +460,23 @@ jobs: 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" + 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@v4 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" + 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@v4 with: @@ -561,10 +494,10 @@ jobs: name: math-comp - id: stepCheck name: Checking presence of CI target mathcomp-bigenough - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"master\" --argstr job \"mathcomp-bigenough\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\ - built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"master\" --argstr job \"mathcomp-bigenough\" \\\n --dry-run 2>&1 + > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\"\ + \ | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" @@ -585,23 +518,23 @@ jobs: 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" + 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@v4 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" + 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@v4 with: @@ -619,10 +552,10 @@ jobs: name: math-comp - id: stepCheck name: Checking presence of CI target mathcomp-classical - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"master\" --argstr job \"mathcomp-classical\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\ - built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"master\" --argstr job \"mathcomp-classical\" \\\n --dry-run 2>&1 + > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\"\ + \ | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" @@ -643,29 +576,96 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" --argstr job "mathcomp-classical" + mathcomp-experimental-reals: + needs: + - coq + - mathcomp-reals + - mathcomp-bigenough + - hierarchy-builder + 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@v4 + 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@v4 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v27 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v15 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target mathcomp-experimental-reals + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"master\" --argstr job \"mathcomp-experimental-reals\" \\\n --dry-run + 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep + \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: coq' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-reals' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "mathcomp-reals" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: mathcomp-bigenough' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "mathcomp-bigenough" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: hierarchy-builder' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "hierarchy-builder" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" + --argstr job "mathcomp-experimental-reals" mathcomp-finmap: needs: - coq 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" + 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@v4 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" + 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@v4 with: @@ -683,10 +683,10 @@ jobs: name: math-comp - id: stepCheck name: Checking presence of CI target mathcomp-finmap - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"master\" --argstr job \"mathcomp-finmap\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\ - built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"master\" --argstr job \"mathcomp-finmap\" \\\n --dry-run 2>&1 > + /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\"\ + \ | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" @@ -707,23 +707,23 @@ jobs: 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" + 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@v4 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" + 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@v4 with: @@ -741,10 +741,10 @@ jobs: name: math-comp - id: stepCheck name: Checking presence of CI target mathcomp-reals - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"master\" --argstr job \"mathcomp-reals\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\ - built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"master\" --argstr job \"mathcomp-reals\" \\\n --dry-run 2>&1 > + /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\"\ + \ | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" @@ -769,23 +769,23 @@ jobs: 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" + 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@v4 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" + 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@v4 with: @@ -803,10 +803,10 @@ jobs: name: math-comp - id: stepCheck name: Checking presence of CI target mathcomp-reals-stdlib - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"master\" --argstr job \"mathcomp-reals-stdlib\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr + bundle \"master\" --argstr job \"mathcomp-reals-stdlib\" \\\n --dry-run + 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep + \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - if: steps.stepCheck.outputs.status == 'built' name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" @@ -824,7 +824,7 @@ jobs: run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "master" --argstr job "mathcomp-reals-stdlib" name: Nix CI for bundle master -'on': +on: pull_request: paths: - .github/workflows/nix-action-master.yml diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index 3c1a56a7c..57c8d2bdf 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"37d20f7c53fc3ee7de52eece3f0f23044ec32546" +"7ff53c990ee876ed8aa55361cbf30a163702a13d"