Skip to content

Commit 36bcc6f

Browse files
4ever24ever2
committed
Set up Nix CI for 8.20
1 parent 1d9755a commit 36bcc6f

File tree

7 files changed

+1203
-147
lines changed

7 files changed

+1203
-147
lines changed

‎.github/workflows/nix-action-coq-8.20.yml‎

Lines changed: 1113 additions & 0 deletions
Large diffs are not rendered by default.

‎.nix/config.nix‎

Lines changed: 10 additions & 41 deletions
Original file line numberDiff line numberDiff line change
@@ -31,59 +31,28 @@
3131

3232
## select an entry to build in the following `bundles` set
3333
## defaults to "default"
34-
default-bundle = "coq-dev";
34+
default-bundle = "coq-8.20";
3535

3636
# MetaCoq is expected to be compatible with a single coq version
3737
# The name of the bundle should finish with the coq version to use
3838
# cachedMake.sh
39-
bundles."coq-dev" = {
39+
bundles."coq-8.20" = {
40+
coqPackages.coq.override.version = "8.20";
41+
coqPackages.equations.override.version = "1.3.1+8.20";
4042

41-
## You can override Coq and other Coq coqPackages
42-
## through the following attribute
43-
coqPackages.coq.override.version = "master";
44-
coqPackages.equations.override.version = "main";
43+
# coqPackages.metacoq.main-job = true;
44+
coqPackages.metacoq-utils.main-job = true;
4545

46-
## In some cases, light overrides are not available/enough
47-
## in which case you can use either
48-
# coqPackages.<coq-pkg>.overrideAttrs = o: <overrides>;
49-
# coqPackages.equations.overrideAttrs = o: <overrides>;
50-
## or a "long" overlay to put in `.nix/coq-overlays
51-
## you may use `nix-shell --run fetchOverlay <coq-pkg>`
52-
## to automatically retrieve the one from nixpkgs
53-
## if it exists and is correctly named/located
54-
55-
## You can override Coq and other coqPackages
56-
## through the following attribute
57-
## If <ocaml-pkg> does not support light overrides,
58-
## you may use `overrideAttrs` or long overlays
59-
## located in `.nix/ocaml-overlays`
60-
## (there is no automation for this one)
61-
# ocamlPackages.<ocaml-pkg>.override.version = "x.xx";
62-
63-
## You can also override packages from the nixpkgs toplevel
64-
# <nix-pkg>.override.overrideAttrs = o: <overrides>;
65-
## Or put an overlay in `.nix/overlays`
66-
67-
## you may mark a package as a main CI job (one to take deps and
68-
## rev deps from) as follows
69-
# coqPackages.<main-pkg>.main-job = true;
70-
## by default the current package and its shell attributes are main jobs
71-
72-
## you may mark a package as a CI job as follows
73-
# coqPackages.<another-pkg>.job = "test";
74-
## It can then built through
75-
## nix-build --argstr bundle "default" --arg job "test";
76-
## in the absence of such a directive, the job "another-pkg" will
77-
## is still available, but will be automatically included in the CI
78-
## via the command genNixActions only if it is a dependency or a
79-
## reverse dependency of a job flagged as "main-job" (see above).
46+
push-branches = ["coq-8.20"];
8047

48+
# Reverse dependencies
49+
coqPackages.ElmExtraction.override.version = "coq-8.20";
50+
coqPackages.RustExtraction.override.version = "coq-8.20";
8151
};
8252

8353
## Cachix caches to use in CI
8454
## Below we list some standard ones
8555
cachix.coq = {};
86-
# cachix.math-comp = {};
8756
cachix.coq-community = {};
8857

8958
## If you have write access to one of these caches you can

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
"39243d0edb4cb0b872d299c4b128fe232f0d8101"
1+
"a1f630a232a3e2c739df99d0a947bf7465d2f8bb"

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

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

‎.nix/coq-overlays/metacoq/default.nix‎

Lines changed: 78 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,22 @@
1-
{ lib, fetchzip,
2-
mkCoqDerivation, recurseIntoAttrs, single ? false,
3-
coqPackages, coq, equations, version ? null }@args:
4-
with builtins // lib;
1+
{ lib,
2+
mkCoqDerivation, single ? false,
3+
coq, equations, version ? null }@args:
4+
55
let
66
repo = "metacoq";
77
owner = "MetaCoq";
8-
defaultVersion = with versions; switch coq.coq-version [
8+
defaultVersion = lib.switch coq.coq-version [
99
{ case = "8.11"; out = "1.0-beta2-8.11"; }
1010
{ case = "8.12"; out = "1.0-beta2-8.12"; }
1111
# Do not provide 8.13 because it does not compile with equations 1.3 provided by default (only 1.2.3)
1212
# { case = "8.13"; out = "1.0-beta2-8.13"; }
13-
{ case = "8.14"; out = "1.0-8.14"; }
14-
{ case = "8.15"; out = "1.0-8.15"; }
15-
{ case = "8.16"; out = "1.0-8.16"; }
16-
{ case = "dev"; out = "dev"; }
13+
{ case = "8.14"; out = "1.1-8.14"; }
14+
{ case = "8.15"; out = "1.1-8.15"; }
15+
{ case = "8.16"; out = "1.1-8.16"; }
16+
{ case = "8.17"; out = "1.3.1-8.17"; }
17+
{ case = "8.18"; out = "1.3.1-8.18"; }
18+
{ case = "8.19"; out = "1.3.3-8.19"; }
19+
{ case = "8.20"; out = "1.3.4-8.20"; }
1720
] null;
1821
release = {
1922
"1.0-beta2-8.11".sha256 = "sha256-I9YNk5Di6Udvq5/xpLSNflfjRyRH8fMnRzbo3uhpXNs=";
@@ -22,66 +25,109 @@ let
2225
"1.0-8.14".sha256 = "sha256-iRnaNeHt22JqxMNxOGPPycrO9EoCVjusR2s0GfON1y0=";
2326
"1.0-8.15".sha256 = "sha256-8RUC5dHNfLJtJh+IZG4nPTAVC8ZKVh2BHedkzjwLf/k=";
2427
"1.0-8.16".sha256 = "sha256-7rkCAN4PNnMgsgUiiLe2TnAliknN75s2SfjzyKCib/o=";
28+
"1.1-8.14".sha256 = "sha256-6vViCNQl6BnGgOHX3P/OLfFXN4aUfv4RbDokfz2BgQI=";
29+
"1.1-8.15".sha256 = "sha256-qCD3wFW4E+8vSVk4XoZ0EU4PVya0al+JorzS9nzmR/0=";
30+
"1.1-8.16".sha256 = "sha256-cTK4ptxpPPlqxAhasZFX3RpSlsoTZwhTqs2A3BZy9sA=";
31+
"1.2.1-8.17".sha256 = "sha256-FP4upuRsG8B5Q5FIr76t+ecRirrOUX0D1QiLq0/zMyE=";
32+
"1.2.1-8.18".sha256 = "sha256-49g5db2Bv8HpltptJdxA7zrmgNFGC6arx5h2mKHhrko=";
33+
"1.3.1-8.17".sha256 = "sha256-l0/QLC7V3zSk/FsaE2eL6tXy2BzbcI5MAk/c+FESwnc=";
34+
"1.3.1-8.18".sha256 = "sha256-L6Ym4Auwqaxv5tRmJLSVC812dxCqdUU5aN8+t5HVYzY=";
35+
"1.3.1-8.19".sha256 = "sha256-fZED/Uel1jt5XF83dR6HfyhSkfBdLkET8C/ArDgsm64=";
36+
"1.3.2-8.19".sha256 = "sha256-e5Pm1AhaQrO6JoZylSXYWmeXY033QflQuCBZhxGH8MA=";
37+
"1.3.2-8.20".sha256 = "sha256-4J7Ly4Fc2E/I6YqvzTLntVVls5t94OUOjVMKJyyJdw8=";
38+
"1.3.3-8.19".sha256 = "sha256-SBTv49zQXZ+oGvIqWM53hjBKru9prFgZRv8gVgls40k=";
39+
"1.3.4-8.20".sha256 = "sha256-ofRP0Uo48G2LBuIy/5ZLyK+iVZXleKiwfMEBD0rX9fQ=";
2540
};
2641
releaseRev = v: "v${v}";
2742

28-
# list of core metacoq packages sorted by dependency order
29-
packages = [ "utils" "common" "template-coq" "pcuic" "safechecker" "template-pcuic" "erasure" "quotation" "safechecker-plugin" "erasure-plugin" "all" ];
43+
# list of core metacoq packages and their dependencies
44+
packages = {
45+
"utils" = [];
46+
"common" = [ "utils" ];
47+
"template-coq" = [ "common" ];
48+
"pcuic" = if (lib.versionAtLeast coq.coq-version "8.17" || coq.coq-version == "dev")
49+
then [ "common" ]
50+
else [ "template-coq" ];
51+
"safechecker" = [ "pcuic" ];
52+
"template-pcuic" = [ "template-coq" "pcuic" ];
53+
"erasure" = [ "safechecker" "template-pcuic" ];
54+
"quotation" = [ "template-coq" "pcuic" "template-pcuic" ];
55+
"safechecker-plugin" = [ "template-pcuic" "safechecker" ];
56+
"erasure-plugin" = [ "template-pcuic" "erasure" ];
57+
"translations" = [ "template-coq" ];
58+
"all" = [ "safechecker-plugin" "erasure-plugin" "translations" "quotation" ];
59+
};
3060

3161
template-coq = metacoq_ "template-coq";
3262

3363
metacoq_ = package: let
34-
metacoq-deps = if package == "single" then []
35-
else map metacoq_ (head (splitList (pred.equal package) packages));
64+
metacoq-deps = lib.optionals (package != "single") (map metacoq_ packages.${package});
3665
pkgpath = if package == "single" then "./" else "./${package}";
3766
pname = if package == "all" then "metacoq" else "metacoq-${package}";
3867
pkgallMake = ''
3968
mkdir all
4069
echo "all:" > all/Makefile
4170
echo "install:" >> all/Makefile
42-
'' ;
71+
'';
4372
derivation = (mkCoqDerivation ({
4473
inherit version pname defaultVersion release releaseRev repo owner;
4574

4675
mlPlugin = true;
4776
propagatedBuildInputs = [ equations coq.ocamlPackages.zarith ] ++ metacoq-deps;
4877

49-
patchPhase = ''
78+
patchPhase = if lib.versionAtLeast coq.coq-version "8.17" || coq.coq-version == "dev" then ''
5079
patchShebangs ./configure.sh
5180
patchShebangs ./template-coq/update_plugin.sh
5281
patchShebangs ./template-coq/gen-src/to-lower.sh
5382
patchShebangs ./safechecker-plugin/clean_extraction.sh
5483
patchShebangs ./erasure-plugin/clean_extraction.sh
5584
echo "CAMLFLAGS+=-w -60 # Unused module" >> ./safechecker/Makefile.plugin.local
5685
sed -i -e 's/mv $i $newi;/mv $i tmp; mv tmp $newi;/' ./template-coq/gen-src/to-lower.sh ./safechecker-plugin/clean_extraction.sh ./erasure-plugin/clean_extraction.sh
57-
'' ;
86+
'' else ''
87+
patchShebangs ./configure.sh
88+
patchShebangs ./template-coq/update_plugin.sh
89+
patchShebangs ./template-coq/gen-src/to-lower.sh
90+
patchShebangs ./pcuic/clean_extraction.sh
91+
patchShebangs ./safechecker/clean_extraction.sh
92+
patchShebangs ./erasure/clean_extraction.sh
93+
echo "CAMLFLAGS+=-w -60 # Unused module" >> ./safechecker/Makefile.plugin.local
94+
sed -i -e 's/mv $i $newi;/mv $i tmp; mv tmp $newi;/' ./template-coq/gen-src/to-lower.sh ./pcuic/clean_extraction.sh ./safechecker/clean_extraction.sh ./erasure/clean_extraction.sh
95+
'';
5896

59-
configurePhase = optionalString (package == "all") pkgallMake + ''
97+
configurePhase = lib.optionalString (package == "all") pkgallMake + ''
6098
touch ${pkgpath}/metacoq-config
61-
'' + optionalString (elem package ["safechecker" "erasure" "template-pcuic" "quotation" "safechecker-plugin" "erasure-plugin"]) ''
99+
'' + lib.optionalString (lib.elem package ["erasure" "template-pcuic" "quotation" "safechecker-plugin" "erasure-plugin" "translations"]) ''
62100
echo "-I ${template-coq}/lib/coq/${coq.coq-version}/user-contrib/MetaCoq/Template/" > ${pkgpath}/metacoq-config
63-
'' + optionalString (package == "single") ''
101+
'' + lib.optionalString (package == "single") ''
64102
./configure.sh local
65103
'';
66104

67105
preBuild = ''
68106
cd ${pkgpath}
69-
'' ;
107+
'';
70108

71109
meta = {
72110
homepage = "https://metacoq.github.io/";
73-
license = licenses.mit;
74-
maintainers = with maintainers; [ cohencyril ];
111+
license = lib.licenses.mit;
112+
maintainers = with lib.maintainers; [ cohencyril ];
75113
};
76-
} // optionalAttrs (package != "single")
77-
{ passthru = genAttrs packages metacoq_; })
78-
).overrideAttrs (o:
79-
let requiresOcamlStdlibShims = versionAtLeast o.version "1.0-8.16" ||
80-
(o.version == "dev" && (versionAtLeast coq.coq-version "8.16" || coq.coq-version == "dev")) ;
81-
in
82-
{
83-
propagatedBuildInputs = o.propagatedBuildInputs ++ optional requiresOcamlStdlibShims coq.ocamlPackages.stdlib-shims;
84-
});
85-
in derivation;
114+
} // lib.optionalAttrs (package != "single")
115+
{ passthru = lib.mapAttrs (package: deps: metacoq_ package) packages; })
116+
).overrideAttrs (o:
117+
let requiresOcamlStdlibShims = lib.versionAtLeast o.version "1.0-8.16" ||
118+
(o.version == "dev" && (lib.versionAtLeast coq.coq-version "8.16" || coq.coq-version == "dev")) ;
119+
in
120+
{
121+
propagatedBuildInputs = o.propagatedBuildInputs ++ lib.optional requiresOcamlStdlibShims coq.ocamlPackages.stdlib-shims;
122+
});
123+
# utils, common, template-pcuic, quotation, safechecker-plugin, and erasure-plugin
124+
# packages didn't exist before 1.2, so bulding nothing in that case
125+
patched-derivation = derivation.overrideAttrs (o:
126+
lib.optionalAttrs (o.pname != null &&
127+
lib.elem package [ "utils" "common" "template-pcuic" "quotation" "safechecker-plugin" "erasure-plugin" ] &&
128+
o.version != null && o.version != "dev" && lib.versions.isLt "1.2" o.version)
129+
{ patchPhase = ""; configurePhase = ""; preBuild = ""; buildPhase = "echo doing nothing"; installPhase = "echo doing nothing"; }
130+
);
131+
in patched-derivation;
86132
in
87133
metacoq_ (if single then "single" else "all")

‎.nix/nixpkgs.nix‎

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

‎default.nix‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,7 @@
55
}@args:
66
let auto = fetchGit {
77
url = "https://github.com/coq-community/coq-nix-toolbox.git";
8-
allRefs = true ;
9-
# ref = "master";
8+
ref = "master";
109
rev = import .nix/coq-nix-toolbox.nix;
1110
};
1211
in

0 commit comments

Comments
 (0)