Skip to content

Commit 04d385c

Browse files
proux01proux01
committed
Add overlay
1 parent 7773253 commit 04d385c

7 files changed

Lines changed: 689 additions & 53 deletions

File tree

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

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -61,7 +61,6 @@ jobs:
6161
mathcomp-algebra:
6262
needs:
6363
- rocq-core
64-
- micromega-plugin
6564
runs-on: ubuntu-latest
6665
steps:
6766
- name: Determine which commit to initially checkout
@@ -126,10 +125,6 @@ jobs:
126125
name: 'Building/fetching previous CI target: hierarchy-builder'
127126
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
128127
"rocq-9.0" --argstr job "hierarchy-builder"
129-
- if: steps.stepCheck.outputs.status != 'fetched'
130-
name: 'Building/fetching previous CI target: micromega-plugin'
131-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
132-
"rocq-9.0" --argstr job "micromega-plugin"
133128
- if: steps.stepCheck.outputs.status != 'fetched'
134129
name: Building/fetching current CI target
135130
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle

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

Lines changed: 483 additions & 4 deletions
Large diffs are not rendered by default.

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

Lines changed: 196 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,68 @@
11
jobs:
2+
bignums:
3+
needs:
4+
- rocq-core
5+
- stdlib
6+
runs-on: ubuntu-latest
7+
steps:
8+
- name: Determine which commit to initially checkout
9+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{
10+
github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha
11+
}}\" >> $GITHUB_ENV\nfi\n"
12+
- name: Git checkout
13+
uses: actions/checkout@v6
14+
with:
15+
fetch-depth: 0
16+
ref: ${{ env.target_commit }}
17+
- name: Determine which commit to test
18+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{
19+
github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url
20+
}} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git
21+
merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
22+
2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\
23+
\ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha
24+
}}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
25+
\ fi\nfi\n"
26+
- name: Git checkout
27+
uses: actions/checkout@v6
28+
with:
29+
fetch-depth: 0
30+
ref: ${{ env.tested_commit }}
31+
- name: Cachix install
32+
uses: cachix/install-nix-action@v31
33+
with:
34+
nix_path: nixpkgs=channel:nixpkgs-unstable
35+
- name: Cachix setup coq-community
36+
uses: cachix/cachix-action@v16
37+
with:
38+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
39+
extraPullNames: coq, math-comp
40+
name: coq-community
41+
- id: stepGetDerivation
42+
name: Getting derivation for current job (bignums)
43+
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
44+
\"rocq-9.2\" --argstr job \"bignums\" \\\n --dry-run 2> err > out || (touch
45+
fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation
46+
failed\"; exit 1; fi\n"
47+
- id: stepCheck
48+
name: Checking presence of CI target for current job
49+
run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs
50+
actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\
51+
) ; then\n echo \"waiting a bit for derivations that should be in cache\"\
52+
\n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\
53+
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
54+
- if: steps.stepCheck.outputs.status != 'fetched'
55+
name: 'Building/fetching previous CI target: rocq-core'
56+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
57+
"rocq-9.2" --argstr job "rocq-core"
58+
- if: steps.stepCheck.outputs.status != 'fetched'
59+
name: 'Building/fetching previous CI target: stdlib'
60+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
61+
"rocq-9.2" --argstr job "stdlib"
62+
- if: steps.stepCheck.outputs.status != 'fetched'
63+
name: Building/fetching current CI target
64+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
65+
"rocq-9.2" --argstr job "bignums"
266
coq:
367
needs:
468
- rocq-core
@@ -121,11 +185,11 @@ jobs:
121185
name: Building/fetching current CI target
122186
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
123187
"rocq-9.2" --argstr job "hierarchy-builder"
124-
mathcomp-algebra:
188+
iris:
125189
needs:
126190
- rocq-core
127-
- hierarchy-builder
128-
- micromega-plugin
191+
- stdlib
192+
- stdpp
129193
runs-on: ubuntu-latest
130194
steps:
131195
- name: Determine which commit to initially checkout
@@ -162,11 +226,11 @@ jobs:
162226
extraPullNames: coq, math-comp
163227
name: coq-community
164228
- id: stepGetDerivation
165-
name: Getting derivation for current job (mathcomp-algebra)
229+
name: Getting derivation for current job (iris)
166230
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
167-
\"rocq-9.2\" --argstr job \"mathcomp-algebra\" \\\n --dry-run 2> err > out
168-
|| (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting
169-
derivation failed\"; exit 1; fi\n"
231+
\"rocq-9.2\" --argstr job \"iris\" \\\n --dry-run 2> err > out || (touch
232+
fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation
233+
failed\"; exit 1; fi\n"
170234
- id: stepCheck
171235
name: Checking presence of CI target for current job
172236
run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs
@@ -179,21 +243,67 @@ jobs:
179243
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
180244
"rocq-9.2" --argstr job "rocq-core"
181245
- if: steps.stepCheck.outputs.status != 'fetched'
182-
name: 'Building/fetching previous CI target: mathcomp-order'
183-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
184-
"rocq-9.2" --argstr job "mathcomp-order"
185-
- if: steps.stepCheck.outputs.status != 'fetched'
186-
name: 'Building/fetching previous CI target: mathcomp-fingroup'
246+
name: 'Building/fetching previous CI target: stdlib'
187247
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
188-
"rocq-9.2" --argstr job "mathcomp-fingroup"
248+
"rocq-9.2" --argstr job "stdlib"
189249
- if: steps.stepCheck.outputs.status != 'fetched'
190-
name: 'Building/fetching previous CI target: hierarchy-builder'
250+
name: 'Building/fetching previous CI target: stdpp'
191251
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
192-
"rocq-9.2" --argstr job "hierarchy-builder"
252+
"rocq-9.2" --argstr job "stdpp"
193253
- if: steps.stepCheck.outputs.status != 'fetched'
194-
name: 'Building/fetching previous CI target: micromega-plugin'
254+
name: Building/fetching current CI target
195255
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
196-
"rocq-9.2" --argstr job "micromega-plugin"
256+
"rocq-9.2" --argstr job "iris"
257+
mathcomp-algebra:
258+
needs: []
259+
runs-on: ubuntu-latest
260+
steps:
261+
- name: Determine which commit to initially checkout
262+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{
263+
github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha
264+
}}\" >> $GITHUB_ENV\nfi\n"
265+
- name: Git checkout
266+
uses: actions/checkout@v6
267+
with:
268+
fetch-depth: 0
269+
ref: ${{ env.target_commit }}
270+
- name: Determine which commit to test
271+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{
272+
github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url
273+
}} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git
274+
merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
275+
2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\
276+
\ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha
277+
}}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
278+
\ fi\nfi\n"
279+
- name: Git checkout
280+
uses: actions/checkout@v6
281+
with:
282+
fetch-depth: 0
283+
ref: ${{ env.tested_commit }}
284+
- name: Cachix install
285+
uses: cachix/install-nix-action@v31
286+
with:
287+
nix_path: nixpkgs=channel:nixpkgs-unstable
288+
- name: Cachix setup coq-community
289+
uses: cachix/cachix-action@v16
290+
with:
291+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
292+
extraPullNames: coq, math-comp
293+
name: coq-community
294+
- id: stepGetDerivation
295+
name: Getting derivation for current job (mathcomp-algebra)
296+
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
297+
\"rocq-9.2\" --argstr job \"mathcomp-algebra\" \\\n --dry-run 2> err > out
298+
|| (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting
299+
derivation failed\"; exit 1; fi\n"
300+
- id: stepCheck
301+
name: Checking presence of CI target for current job
302+
run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs
303+
actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\
304+
) ; then\n echo \"waiting a bit for derivations that should be in cache\"\
305+
\n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\
306+
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
197307
- if: steps.stepCheck.outputs.status != 'fetched'
198308
name: Building/fetching current CI target
199309
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
@@ -314,6 +424,7 @@ jobs:
314424
stdlib:
315425
needs:
316426
- rocq-core
427+
- micromega-plugin
317428
runs-on: ubuntu-latest
318429
steps:
319430
- name: Determine which commit to initially checkout
@@ -366,10 +477,78 @@ jobs:
366477
name: 'Building/fetching previous CI target: rocq-core'
367478
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
368479
"rocq-9.2" --argstr job "rocq-core"
480+
- if: steps.stepCheck.outputs.status != 'fetched'
481+
name: 'Building/fetching previous CI target: micromega-plugin'
482+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
483+
"rocq-9.2" --argstr job "micromega-plugin"
369484
- if: steps.stepCheck.outputs.status != 'fetched'
370485
name: Building/fetching current CI target
371486
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
372487
"rocq-9.2" --argstr job "stdlib"
488+
stdpp:
489+
needs:
490+
- rocq-core
491+
- stdlib
492+
runs-on: ubuntu-latest
493+
steps:
494+
- name: Determine which commit to initially checkout
495+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{
496+
github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha
497+
}}\" >> $GITHUB_ENV\nfi\n"
498+
- name: Git checkout
499+
uses: actions/checkout@v6
500+
with:
501+
fetch-depth: 0
502+
ref: ${{ env.target_commit }}
503+
- name: Determine which commit to test
504+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{
505+
github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url
506+
}} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git
507+
merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
508+
2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\
509+
\ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha
510+
}}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
511+
\ fi\nfi\n"
512+
- name: Git checkout
513+
uses: actions/checkout@v6
514+
with:
515+
fetch-depth: 0
516+
ref: ${{ env.tested_commit }}
517+
- name: Cachix install
518+
uses: cachix/install-nix-action@v31
519+
with:
520+
nix_path: nixpkgs=channel:nixpkgs-unstable
521+
- name: Cachix setup coq-community
522+
uses: cachix/cachix-action@v16
523+
with:
524+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
525+
extraPullNames: coq, math-comp
526+
name: coq-community
527+
- id: stepGetDerivation
528+
name: Getting derivation for current job (stdpp)
529+
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
530+
\"rocq-9.2\" --argstr job \"stdpp\" \\\n --dry-run 2> err > out || (touch
531+
fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation
532+
failed\"; exit 1; fi\n"
533+
- id: stepCheck
534+
name: Checking presence of CI target for current job
535+
run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs
536+
actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\
537+
) ; then\n echo \"waiting a bit for derivations that should be in cache\"\
538+
\n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\
539+
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
540+
- if: steps.stepCheck.outputs.status != 'fetched'
541+
name: 'Building/fetching previous CI target: rocq-core'
542+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
543+
"rocq-9.2" --argstr job "rocq-core"
544+
- if: steps.stepCheck.outputs.status != 'fetched'
545+
name: 'Building/fetching previous CI target: stdlib'
546+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
547+
"rocq-9.2" --argstr job "stdlib"
548+
- if: steps.stepCheck.outputs.status != 'fetched'
549+
name: Building/fetching current CI target
550+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
551+
"rocq-9.2" --argstr job "stdpp"
373552
name: Nix CI for bundle rocq-9.2
374553
on:
375554
pull_request:

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

Lines changed: 6 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -182,10 +182,7 @@ jobs:
182182
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
183183
"rocq-master" --argstr job "hierarchy-builder"
184184
mathcomp-algebra:
185-
needs:
186-
- rocq-core
187-
- hierarchy-builder
188-
- micromega-plugin
185+
needs: []
189186
runs-on: ubuntu-latest
190187
steps:
191188
- name: Determine which commit to initially checkout
@@ -234,26 +231,6 @@ jobs:
234231
) ; then\n echo \"waiting a bit for derivations that should be in cache\"\
235232
\n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\
236233
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
237-
- if: steps.stepCheck.outputs.status != 'fetched'
238-
name: 'Building/fetching previous CI target: rocq-core'
239-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
240-
"rocq-master" --argstr job "rocq-core"
241-
- if: steps.stepCheck.outputs.status != 'fetched'
242-
name: 'Building/fetching previous CI target: mathcomp-order'
243-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
244-
"rocq-master" --argstr job "mathcomp-order"
245-
- if: steps.stepCheck.outputs.status != 'fetched'
246-
name: 'Building/fetching previous CI target: mathcomp-fingroup'
247-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
248-
"rocq-master" --argstr job "mathcomp-fingroup"
249-
- if: steps.stepCheck.outputs.status != 'fetched'
250-
name: 'Building/fetching previous CI target: hierarchy-builder'
251-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
252-
"rocq-master" --argstr job "hierarchy-builder"
253-
- if: steps.stepCheck.outputs.status != 'fetched'
254-
name: 'Building/fetching previous CI target: micromega-plugin'
255-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
256-
"rocq-master" --argstr job "micromega-plugin"
257234
- if: steps.stepCheck.outputs.status != 'fetched'
258235
name: Building/fetching current CI target
259236
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
@@ -428,6 +405,7 @@ jobs:
428405
stdlib:
429406
needs:
430407
- rocq-core
408+
- micromega-plugin
431409
runs-on: ubuntu-latest
432410
steps:
433411
- name: Determine which commit to initially checkout
@@ -480,6 +458,10 @@ jobs:
480458
name: 'Building/fetching previous CI target: rocq-core'
481459
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
482460
"rocq-master" --argstr job "rocq-core"
461+
- if: steps.stepCheck.outputs.status != 'fetched'
462+
name: 'Building/fetching previous CI target: micromega-plugin'
463+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
464+
"rocq-master" --argstr job "micromega-plugin"
483465
- if: steps.stepCheck.outputs.status != 'fetched'
484466
name: Building/fetching current CI target
485467
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle

‎.nix/config.nix‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -97,6 +97,7 @@ with builtins; with (import <nixpkgs> {}).lib;
9797
# for a complete list of Coq packages available in Nix
9898
# * <github_login>:<branch> is such that this will use the branch <branch>
9999
# from https://github.com/<github_login>/<repository>
100+
stdlib.override.version = "proux01:tify";
100101
};
101102
coq-common-bundles = listToAttrs (forEach coq-master (p:
102103
{ name = p; value.override.version = "master"; }))

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
"175e68be5dcde92457dbb949ef905e771d765a68"
1+
"20731ec68fcf2772869a7d80da55b08723781827"

‎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)