Skip to content

Commit 42a5f56

Browse files
mattam82mattam82
committed
Fix overlays
1 parent ac88008 commit 42a5f56

File tree

5 files changed

+98
-50
lines changed

5 files changed

+98
-50
lines changed

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

Lines changed: 83 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -124,8 +124,13 @@ jobs:
124124
"rocq-dev" --argstr job "equations"
125125
metarocq:
126126
needs:
127-
- rocq-core
127+
- coq
128+
- equations
128129
- stdlib
130+
- metarocq-safechecker-plugin
131+
- metarocq-erasure-plugin
132+
- metarocq-translations
133+
- metarocq-quotation
129134
runs-on: ubuntu-latest
130135
steps:
131136
- name: Determine which commit to initially checkout
@@ -175,13 +180,33 @@ jobs:
175180
\n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\
176181
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
177182
- if: steps.stepCheck.outputs.status != 'fetched'
178-
name: 'Building/fetching previous CI target: rocq-core'
183+
name: 'Building/fetching previous CI target: coq'
179184
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
180-
"rocq-dev" --argstr job "rocq-core"
185+
"rocq-dev" --argstr job "coq"
186+
- if: steps.stepCheck.outputs.status != 'fetched'
187+
name: 'Building/fetching previous CI target: equations'
188+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
189+
"rocq-dev" --argstr job "equations"
181190
- if: steps.stepCheck.outputs.status != 'fetched'
182191
name: 'Building/fetching previous CI target: stdlib'
183192
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
184193
"rocq-dev" --argstr job "stdlib"
194+
- if: steps.stepCheck.outputs.status != 'fetched'
195+
name: 'Building/fetching previous CI target: metarocq-safechecker-plugin'
196+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
197+
"rocq-dev" --argstr job "metarocq-safechecker-plugin"
198+
- if: steps.stepCheck.outputs.status != 'fetched'
199+
name: 'Building/fetching previous CI target: metarocq-erasure-plugin'
200+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
201+
"rocq-dev" --argstr job "metarocq-erasure-plugin"
202+
- if: steps.stepCheck.outputs.status != 'fetched'
203+
name: 'Building/fetching previous CI target: metarocq-translations'
204+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
205+
"rocq-dev" --argstr job "metarocq-translations"
206+
- if: steps.stepCheck.outputs.status != 'fetched'
207+
name: 'Building/fetching previous CI target: metarocq-quotation'
208+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
209+
"rocq-dev" --argstr job "metarocq-quotation"
185210
- if: steps.stepCheck.outputs.status != 'fetched'
186211
name: Building/fetching current CI target
187212
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
@@ -190,6 +215,7 @@ jobs:
190215
needs:
191216
- coq
192217
- equations
218+
- stdlib
193219
- metarocq-utils
194220
runs-on: ubuntu-latest
195221
steps:
@@ -247,6 +273,10 @@ jobs:
247273
name: 'Building/fetching previous CI target: equations'
248274
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
249275
"rocq-dev" --argstr job "equations"
276+
- if: steps.stepCheck.outputs.status != 'fetched'
277+
name: 'Building/fetching previous CI target: stdlib'
278+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
279+
"rocq-dev" --argstr job "stdlib"
250280
- if: steps.stepCheck.outputs.status != 'fetched'
251281
name: 'Building/fetching previous CI target: metarocq-utils'
252282
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
@@ -259,6 +289,7 @@ jobs:
259289
needs:
260290
- coq
261291
- equations
292+
- stdlib
262293
- metarocq-safechecker
263294
- metarocq-template-pcuic
264295
runs-on: ubuntu-latest
@@ -317,6 +348,10 @@ jobs:
317348
name: 'Building/fetching previous CI target: equations'
318349
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
319350
"rocq-dev" --argstr job "equations"
351+
- if: steps.stepCheck.outputs.status != 'fetched'
352+
name: 'Building/fetching previous CI target: stdlib'
353+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
354+
"rocq-dev" --argstr job "stdlib"
320355
- if: steps.stepCheck.outputs.status != 'fetched'
321356
name: 'Building/fetching previous CI target: metarocq-safechecker'
322357
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
@@ -333,6 +368,7 @@ jobs:
333368
needs:
334369
- coq
335370
- equations
371+
- stdlib
336372
- metarocq-template-pcuic
337373
- metarocq-erasure
338374
runs-on: ubuntu-latest
@@ -391,6 +427,10 @@ jobs:
391427
name: 'Building/fetching previous CI target: equations'
392428
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
393429
"rocq-dev" --argstr job "equations"
430+
- if: steps.stepCheck.outputs.status != 'fetched'
431+
name: 'Building/fetching previous CI target: stdlib'
432+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
433+
"rocq-dev" --argstr job "stdlib"
394434
- if: steps.stepCheck.outputs.status != 'fetched'
395435
name: 'Building/fetching previous CI target: metarocq-template-pcuic'
396436
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
@@ -407,6 +447,7 @@ jobs:
407447
needs:
408448
- coq
409449
- equations
450+
- stdlib
410451
- metarocq-common
411452
runs-on: ubuntu-latest
412453
steps:
@@ -464,6 +505,10 @@ jobs:
464505
name: 'Building/fetching previous CI target: equations'
465506
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
466507
"rocq-dev" --argstr job "equations"
508+
- if: steps.stepCheck.outputs.status != 'fetched'
509+
name: 'Building/fetching previous CI target: stdlib'
510+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
511+
"rocq-dev" --argstr job "stdlib"
467512
- if: steps.stepCheck.outputs.status != 'fetched'
468513
name: 'Building/fetching previous CI target: metarocq-common'
469514
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
@@ -476,6 +521,7 @@ jobs:
476521
needs:
477522
- coq
478523
- equations
524+
- stdlib
479525
- metarocq-template-rocq
480526
- metarocq-pcuic
481527
- metarocq-template-pcuic
@@ -535,6 +581,10 @@ jobs:
535581
name: 'Building/fetching previous CI target: equations'
536582
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
537583
"rocq-dev" --argstr job "equations"
584+
- if: steps.stepCheck.outputs.status != 'fetched'
585+
name: 'Building/fetching previous CI target: stdlib'
586+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
587+
"rocq-dev" --argstr job "stdlib"
538588
- if: steps.stepCheck.outputs.status != 'fetched'
539589
name: 'Building/fetching previous CI target: metarocq-template-rocq'
540590
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
@@ -555,6 +605,7 @@ jobs:
555605
needs:
556606
- coq
557607
- equations
608+
- stdlib
558609
- metarocq-pcuic
559610
runs-on: ubuntu-latest
560611
steps:
@@ -612,6 +663,10 @@ jobs:
612663
name: 'Building/fetching previous CI target: equations'
613664
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
614665
"rocq-dev" --argstr job "equations"
666+
- if: steps.stepCheck.outputs.status != 'fetched'
667+
name: 'Building/fetching previous CI target: stdlib'
668+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
669+
"rocq-dev" --argstr job "stdlib"
615670
- if: steps.stepCheck.outputs.status != 'fetched'
616671
name: 'Building/fetching previous CI target: metarocq-pcuic'
617672
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
@@ -624,6 +679,7 @@ jobs:
624679
needs:
625680
- coq
626681
- equations
682+
- stdlib
627683
- metarocq-template-pcuic
628684
- metarocq-safechecker
629685
runs-on: ubuntu-latest
@@ -682,6 +738,10 @@ jobs:
682738
name: 'Building/fetching previous CI target: equations'
683739
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
684740
"rocq-dev" --argstr job "equations"
741+
- if: steps.stepCheck.outputs.status != 'fetched'
742+
name: 'Building/fetching previous CI target: stdlib'
743+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
744+
"rocq-dev" --argstr job "stdlib"
685745
- if: steps.stepCheck.outputs.status != 'fetched'
686746
name: 'Building/fetching previous CI target: metarocq-template-pcuic'
687747
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
@@ -698,6 +758,7 @@ jobs:
698758
needs:
699759
- coq
700760
- equations
761+
- stdlib
701762
- metarocq-template-rocq
702763
- metarocq-pcuic
703764
runs-on: ubuntu-latest
@@ -756,6 +817,10 @@ jobs:
756817
name: 'Building/fetching previous CI target: equations'
757818
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
758819
"rocq-dev" --argstr job "equations"
820+
- if: steps.stepCheck.outputs.status != 'fetched'
821+
name: 'Building/fetching previous CI target: stdlib'
822+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
823+
"rocq-dev" --argstr job "stdlib"
759824
- if: steps.stepCheck.outputs.status != 'fetched'
760825
name: 'Building/fetching previous CI target: metarocq-template-rocq'
761826
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
@@ -772,6 +837,7 @@ jobs:
772837
needs:
773838
- coq
774839
- equations
840+
- stdlib
775841
- metarocq-common
776842
runs-on: ubuntu-latest
777843
steps:
@@ -829,6 +895,10 @@ jobs:
829895
name: 'Building/fetching previous CI target: equations'
830896
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
831897
"rocq-dev" --argstr job "equations"
898+
- if: steps.stepCheck.outputs.status != 'fetched'
899+
name: 'Building/fetching previous CI target: stdlib'
900+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
901+
"rocq-dev" --argstr job "stdlib"
832902
- if: steps.stepCheck.outputs.status != 'fetched'
833903
name: 'Building/fetching previous CI target: metarocq-common'
834904
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
@@ -841,6 +911,7 @@ jobs:
841911
needs:
842912
- coq
843913
- equations
914+
- stdlib
844915
- metarocq-template-rocq
845916
runs-on: ubuntu-latest
846917
steps:
@@ -898,6 +969,10 @@ jobs:
898969
name: 'Building/fetching previous CI target: equations'
899970
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
900971
"rocq-dev" --argstr job "equations"
972+
- if: steps.stepCheck.outputs.status != 'fetched'
973+
name: 'Building/fetching previous CI target: stdlib'
974+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
975+
"rocq-dev" --argstr job "stdlib"
901976
- if: steps.stepCheck.outputs.status != 'fetched'
902977
name: 'Building/fetching previous CI target: metarocq-template-rocq'
903978
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
@@ -910,6 +985,7 @@ jobs:
910985
needs:
911986
- coq
912987
- equations
988+
- stdlib
913989
runs-on: ubuntu-latest
914990
steps:
915991
- name: Determine which commit to initially checkout
@@ -966,6 +1042,10 @@ jobs:
9661042
name: 'Building/fetching previous CI target: equations'
9671043
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
9681044
"rocq-dev" --argstr job "equations"
1045+
- if: steps.stepCheck.outputs.status != 'fetched'
1046+
name: 'Building/fetching previous CI target: stdlib'
1047+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
1048+
"rocq-dev" --argstr job "stdlib"
9691049
- if: steps.stepCheck.outputs.status != 'fetched'
9701050
name: Building/fetching current CI target
9711051
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle

‎.nix/config.nix‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,8 @@
1313
## when calling `nix-shell` and `nix-build` without the `--argstr job` argument
1414
shell-attribute = "equations";
1515

16+
no-rocq-yet = true;
17+
1618
## Maybe the shortname of the library is different from
1719
## the name of the nixpkgs attribute, if so, set it here:
1820
# pname = "{{shortname}}";

.nix/rocq-overlays/metacoq/default.nix renamed to .nix/coq-overlays/metacoq/default.nix

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
{
22
lib,
3-
mkRocqDerivation,
3+
mkCoqDerivation,
44
single ? false,
5-
rocq-core,
5+
coq,
66
equations,
77
stdlib,
88
version ? null,
@@ -11,7 +11,7 @@
1111
let
1212
repo = "metarocq";
1313
owner = "MetaRocq";
14-
defaultVersion = lib.switch rocq-core.rocq-version [
14+
defaultVersion = lib.switch coq.coq-version [
1515
{ case = "9.0"; out = "1.4-9.0"; }
1616
] null;
1717
release = {
@@ -70,7 +70,7 @@ let
7070
echo "install:" >> all/Makefile
7171
'';
7272
derivation =
73-
(mkRocqDerivation (
73+
(mkCoqDerivation (
7474
{
7575
inherit
7676
version
@@ -86,8 +86,8 @@ let
8686
propagatedBuildInputs = [
8787
equations
8888
stdlib
89-
rocq-core.ocamlPackages.zarith
90-
rocq-core.ocamlPackages.stdlib-shims
89+
coq.ocamlPackages.zarith
90+
coq.ocamlPackages.stdlib-shims
9191
] ++ metacoq-deps;
9292

9393
patchPhase =
@@ -117,7 +117,7 @@ let
117117
"translations"
118118
])
119119
''
120-
echo "-I ${template-coq}/lib/coq/${rocq-core.rocq-version}/user-contrib/MetaCoq/Template/" > ${pkgpath}/metacoq-config
120+
echo "-I ${template-coq}/lib/coq/${coq.coq-version}/user-contrib/MetaCoq/Template/" > ${pkgpath}/metacoq-config
121121
''
122122
+ lib.optionalString (package == "single") ''
123123
./configure.sh local

.nix/rocq-overlays/metarocq/default.nix renamed to .nix/coq-overlays/metarocq/default.nix

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
{
22
lib,
3-
mkRocqDerivation,
3+
mkCoqDerivation,
4+
coq,
45
single ? false,
5-
rocq-core,
66
equations,
77
stdlib,
88
version ? null,
@@ -65,7 +65,7 @@ let
6565
echo "install:" >> all/Makefile
6666
'';
6767
derivation =
68-
(mkRocqDerivation (
68+
(mkCoqDerivation (
6969
{
7070
inherit
7171
version
@@ -80,8 +80,8 @@ let
8080
propagatedBuildInputs = [
8181
equations
8282
stdlib
83-
rocq-core.ocamlPackages.zarith
84-
rocq-core.ocamlPackages.stdlib-shims
83+
# rocq-core.ocamlPackages.zarith
84+
# rocq-core.ocamlPackages.stdlib-shims
8585
] ++ metarocq-deps;
8686

8787
patchPhase =
@@ -111,7 +111,7 @@ let
111111
"translations"
112112
])
113113
''
114-
echo "-I ${template-rocq}/lib/coq/${rocq-core.rocq-version}/user-contrib/MetaRocq/Template/" > ${pkgpath}/metarocq-config
114+
echo "-I ${template-rocq}/lib/coq/${coq.coq-version}/user-contrib/MetaRocq/Template/" > ${pkgpath}/metarocq-config
115115
''
116116
+ lib.optionalString (package == "single") ''
117117
./configure.sh local

‎.nix/rocq-overlays/equations/default.nix‎

Lines changed: 0 additions & 34 deletions
This file was deleted.

0 commit comments

Comments
 (0)