Skip to content

Commit f9d94e3

Browse files
proux01proux01
committed
Add overlays
1 parent a65c430 commit f9d94e3

6 files changed

Lines changed: 23 additions & 556 deletions

File tree

‎.github/workflows/nix-action-rocq-9.1.yml‎

Lines changed: 11 additions & 388 deletions
Large diffs are not rendered by default.

‎.github/workflows/nix-action-rocq-9.2.yml‎

Lines changed: 0 additions & 78 deletions
Original file line numberDiff line numberDiff line change
@@ -2509,84 +2509,6 @@ jobs:
25092509
name: Building/fetching current CI target
25102510
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
25112511
"rocq-9.2" --argstr job "mathcomp-algebra"
2512-
mathcomp-algebra-tactics:
2513-
needs:
2514-
- coq
2515-
- mathcomp-algebra
2516-
- coq-elpi
2517-
- mathcomp-zify
2518-
runs-on: ubuntu-latest
2519-
steps:
2520-
- name: Determine which commit to initially checkout
2521-
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{
2522-
github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha
2523-
}}\" >> $GITHUB_ENV\nfi\n"
2524-
- name: Git checkout
2525-
uses: actions/checkout@v6
2526-
with:
2527-
fetch-depth: 0
2528-
ref: ${{ env.target_commit }}
2529-
- name: Determine which commit to test
2530-
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{
2531-
github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url
2532-
}} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git
2533-
merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
2534-
2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\
2535-
\ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha
2536-
}}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
2537-
\ fi\nfi\n"
2538-
- name: Git checkout
2539-
uses: actions/checkout@v6
2540-
with:
2541-
fetch-depth: 0
2542-
ref: ${{ env.tested_commit }}
2543-
- name: Cachix install
2544-
uses: cachix/install-nix-action@v31
2545-
with:
2546-
nix_path: nixpkgs=channel:nixpkgs-unstable
2547-
- name: Cachix setup coq
2548-
uses: cachix/cachix-action@v16
2549-
with:
2550-
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
2551-
extraPullNames: coq-community, math-comp
2552-
name: coq
2553-
- id: stepGetDerivation
2554-
name: Getting derivation for current job (mathcomp-algebra-tactics)
2555-
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
2556-
\"rocq-9.2\" --argstr job \"mathcomp-algebra-tactics\" \\\n --dry-run 2>
2557-
err > out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"\
2558-
Error: getting derivation failed\"; exit 1; fi\n"
2559-
- id: stepCheck
2560-
name: Checking presence of CI target for current job
2561-
run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs
2562-
actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\
2563-
) ; then\n echo \"waiting a bit for derivations that should be in cache\"\
2564-
\n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\
2565-
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
2566-
- if: steps.stepCheck.outputs.status != 'fetched'
2567-
name: 'Building/fetching previous CI target: coq'
2568-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
2569-
"rocq-9.2" --argstr job "coq"
2570-
- if: steps.stepCheck.outputs.status != 'fetched'
2571-
name: 'Building/fetching previous CI target: mathcomp-ssreflect'
2572-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
2573-
"rocq-9.2" --argstr job "mathcomp-ssreflect"
2574-
- if: steps.stepCheck.outputs.status != 'fetched'
2575-
name: 'Building/fetching previous CI target: mathcomp-algebra'
2576-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
2577-
"rocq-9.2" --argstr job "mathcomp-algebra"
2578-
- if: steps.stepCheck.outputs.status != 'fetched'
2579-
name: 'Building/fetching previous CI target: coq-elpi'
2580-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
2581-
"rocq-9.2" --argstr job "coq-elpi"
2582-
- if: steps.stepCheck.outputs.status != 'fetched'
2583-
name: 'Building/fetching previous CI target: mathcomp-zify'
2584-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
2585-
"rocq-9.2" --argstr job "mathcomp-zify"
2586-
- if: steps.stepCheck.outputs.status != 'fetched'
2587-
name: Building/fetching current CI target
2588-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
2589-
"rocq-9.2" --argstr job "mathcomp-algebra-tactics"
25902512
mathcomp-analysis:
25912513
needs:
25922514
- coq

‎.github/workflows/nix-action-rocq-master.yml‎

Lines changed: 0 additions & 83 deletions
Original file line numberDiff line numberDiff line change
@@ -3636,84 +3636,6 @@ jobs:
36363636
name: Building/fetching current CI target
36373637
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
36383638
"rocq-master" --argstr job "mathcomp-algebra"
3639-
mathcomp-algebra-tactics:
3640-
needs:
3641-
- coq
3642-
- mathcomp-algebra
3643-
- coq-elpi
3644-
- mathcomp-zify
3645-
runs-on: ubuntu-latest
3646-
steps:
3647-
- name: Determine which commit to initially checkout
3648-
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{
3649-
github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha
3650-
}}\" >> $GITHUB_ENV\nfi\n"
3651-
- name: Git checkout
3652-
uses: actions/checkout@v6
3653-
with:
3654-
fetch-depth: 0
3655-
ref: ${{ env.target_commit }}
3656-
- name: Determine which commit to test
3657-
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{
3658-
github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url
3659-
}} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git
3660-
merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
3661-
2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\
3662-
\ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha
3663-
}}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
3664-
\ fi\nfi\n"
3665-
- name: Git checkout
3666-
uses: actions/checkout@v6
3667-
with:
3668-
fetch-depth: 0
3669-
ref: ${{ env.tested_commit }}
3670-
- name: Cachix install
3671-
uses: cachix/install-nix-action@v31
3672-
with:
3673-
nix_path: nixpkgs=channel:nixpkgs-unstable
3674-
- name: Cachix setup coq
3675-
uses: cachix/cachix-action@v16
3676-
with:
3677-
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
3678-
extraPullNames: coq-community, math-comp
3679-
name: coq
3680-
- id: stepGetDerivation
3681-
name: Getting derivation for current job (mathcomp-algebra-tactics)
3682-
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
3683-
\"rocq-master\" --argstr job \"mathcomp-algebra-tactics\" \\\n --dry-run
3684-
2> err > out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo
3685-
\"Error: getting derivation failed\"; exit 1; fi\n"
3686-
- id: stepCheck
3687-
name: Checking presence of CI target for current job
3688-
run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs
3689-
actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\
3690-
) ; then\n echo \"waiting a bit for derivations that should be in cache\"\
3691-
\n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\
3692-
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
3693-
- if: steps.stepCheck.outputs.status != 'fetched'
3694-
name: 'Building/fetching previous CI target: coq'
3695-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
3696-
"rocq-master" --argstr job "coq"
3697-
- if: steps.stepCheck.outputs.status != 'fetched'
3698-
name: 'Building/fetching previous CI target: mathcomp-ssreflect'
3699-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
3700-
"rocq-master" --argstr job "mathcomp-ssreflect"
3701-
- if: steps.stepCheck.outputs.status != 'fetched'
3702-
name: 'Building/fetching previous CI target: mathcomp-algebra'
3703-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
3704-
"rocq-master" --argstr job "mathcomp-algebra"
3705-
- if: steps.stepCheck.outputs.status != 'fetched'
3706-
name: 'Building/fetching previous CI target: coq-elpi'
3707-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
3708-
"rocq-master" --argstr job "coq-elpi"
3709-
- if: steps.stepCheck.outputs.status != 'fetched'
3710-
name: 'Building/fetching previous CI target: mathcomp-zify'
3711-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
3712-
"rocq-master" --argstr job "mathcomp-zify"
3713-
- if: steps.stepCheck.outputs.status != 'fetched'
3714-
name: Building/fetching current CI target
3715-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
3716-
"rocq-master" --argstr job "mathcomp-algebra-tactics"
37173639
mathcomp-analysis:
37183640
needs:
37193641
- coq
@@ -7127,7 +7049,6 @@ jobs:
71277049
stdlib-test:
71287050
needs:
71297051
- rocq-core
7130-
- stdlib
71317052
runs-on: ubuntu-latest
71327053
steps:
71337054
- name: Determine which commit to initially checkout
@@ -7180,10 +7101,6 @@ jobs:
71807101
name: 'Building/fetching previous CI target: rocq-core'
71817102
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
71827103
"rocq-master" --argstr job "rocq-core"
7183-
- if: steps.stepCheck.outputs.status != 'fetched'
7184-
name: 'Building/fetching previous CI target: stdlib'
7185-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
7186-
"rocq-master" --argstr job "stdlib"
71877104
- if: steps.stepCheck.outputs.status != 'fetched'
71887105
name: Building/fetching current CI target
71897106
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle

‎.nix/config.nix‎

Lines changed: 9 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -156,7 +156,6 @@ with builtins; with (import <nixpkgs> {}).lib;
156156
"itree-io"
157157
"json"
158158
"kami"
159-
"mathcomp-algebra-tactics"
160159
"mathcomp-analysis"
161160
"mathcomp-classical"
162161
"mathcomp-reals"
@@ -227,14 +226,18 @@ with builtins; with (import <nixpkgs> {}).lib;
227226
"metacoq-translations"
228227
"metacoq-utils"
229228
"metarocq"
229+
"metarocq-common"
230230
"metarocq-erasure"
231231
"metarocq-erasure-plugin"
232232
"metarocq-pcuic"
233233
"metarocq-quotation"
234234
"metarocq-safechecker"
235235
"metarocq-safechecker-plugin"
236236
"metarocq-template-pcuic"
237+
"metarocq-template-rocq"
237238
"metarocq-test"
239+
"metarocq-translations"
240+
"metarocq-utils"
238241
"rewriter"
239242
"riscvcoq"
240243
"rupicola"
@@ -258,6 +261,7 @@ with builtins; with (import <nixpkgs> {}).lib;
258261
iris-examples.job = false; # Currently broken
259262
jasmin.job = false; # Currently broken, c.f., https://github.com/rocq-prover/rocq/pull/20589
260263
CakeMLExtraction.job = false; # not in Rocq CI
264+
verified-extraction.job = false; # not in Rocq CI
261265
ceres-bs.job = false; # not in Rocq CI
262266
CertiRocq.job = false; # not in Rocq CI
263267
ConCert.job = false; # not in Rocq CI
@@ -280,6 +284,9 @@ with builtins; with (import <nixpkgs> {}).lib;
280284
# for a complete list of Coq packages available in Nix
281285
# * <github_login>:<branch> is such that this will use the branch <branch>
282286
# from https://github.com/<github_login>/<repository>
287+
smtcoq.override.version = "proux01:stdlib251";
288+
metarocq.override.version = "proux01:stdlib251";
289+
metarocq-test.override.version = "proux01:stdlib251";
283290
sf.job = false; # temporarily disactivated in Rocq CI
284291
trakt.job = false; # temporarily disactivated in Rocq CI
285292
smtcoq-trakt.job = false; # temporarily disactivated in Rocq CI
@@ -349,14 +356,12 @@ with builtins; with (import <nixpkgs> {}).lib;
349356
equations.override.version = "2137c8e7081f2d47ab903de0cc09fd6a05bfab01";
350357
equations-test.job = false;
351358
fiat-parsers.job = false; # broken
352-
metarocq.override.version = "2995003b88f3812e5649cfdd0f9a4c44ceaf0700";
353-
metarocq-test.override.version = "2995003b88f3812e5649cfdd0f9a4c44ceaf0700";
354359
mtac2.override.version = "bcbefa79406fc113f878eb5f89758de241d81433";
355360
paramcoq-test.override.version = "937537d416bc5f7b81937d4223d7783d0e687239";
356361
relation-algebra.override.version = "4db15229396abfd8913685be5ffda4f0fdb593d9";
357362
rewriter.override.version = "9496defb8b236f442d11372f6e0b5e48aa38acfc";
358363
rocq-lean-import.override.version = "c3546102f242aaa1e9af921c78bdb1132522e444";
359-
smtcoq.override.version = "5c6033c906249fcf98a48b4112f6996053124514";
364+
# smtcoq.override.version = "5c6033c906249fcf98a48b4112f6996053124514";
360365
# smtcoq-trakt.override.version = "9392f7446a174b770110445c155a07b183cdca3d";
361366
stalmarck-tactic.override.version = "d32acd3c477c57b48dd92bdd96d53fb8fa628512";
362367
unicoq.override.version = "28ec18aef35877829535316fc09825a25be8edf1";

‎.nix/coq-nix-toolbox.nix‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
"3b7baf61aa95441d62332d7fdad562a61a125f80"
1+
"dbe1a94a64c014990c7530234af845344be04b51"

‎default.nix‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,8 +4,8 @@
44
bundle ? null, job ? null, inNixShell ? null, src ? ./.,
55
}@args:
66
let auto = fetchGit {
7-
url = "https://github.com/rocq-community/coq-nix-toolbox.git";
8-
ref = "master";
7+
url = "https://github.com/proux01/coq-nix-toolbox.git";
8+
ref = "micromega";
99
rev = import .nix/coq-nix-toolbox.nix;
1010
};
1111
in

0 commit comments

Comments
 (0)