tjh.dev
nixpkgs mirror (for testing)
github.com/NixOS/nixpkgs
nix
1{
2 lib,
3 mkCoqDerivation,
4 single ? false,
5 coq,
6 equations,
7 version ? null,
8}@args:
9
10let
11 repo = "metarocq";
12 owner = "MetaRocq";
13 defaultVersion =
14 let
15 case = case: out: { inherit case out; };
16 in
17 lib.switch coq.coq-version [
18 (case "9.1" "1.4.1-9.1")
19 (case "9.0" "1.4-9.0.1")
20 ] null;
21 release = {
22 "1.4-9.0".sha256 = "sha256-5QecDAMkvgfDPZ7/jDfnOgcE+Eb1LTAozP7nz6nkuxg=";
23 "1.4-9.0.1".sha256 = "sha256-zMUd2A6EG0LYK3L9ABQvS/Et4MDpSmf3Pxd9+IPNYkI=";
24 "1.4-9.1".sha256 = "sha256-v6jFvUavIzyb/e6ytAaZjxQLFM9uW9TDUB77yRO74eE=";
25 "1.4.1-9.1".sha256 = "sha256-tzoAWX74lg7pArGVP11QBvDRKMvmGxXvrf3+1E3Y4DI=";
26 };
27 releaseRev = v: "v${v}";
28
29 # list of core metarocq packages and their dependencies
30 packages = {
31 "utils" = [ ];
32 "common" = [ "utils" ];
33 "template-rocq" = [ "common" ];
34 "pcuic" = [ "common" ];
35 "safechecker" = [ "pcuic" ];
36 "template-pcuic" = [
37 "template-rocq"
38 "pcuic"
39 ];
40 "erasure" = [
41 "safechecker"
42 "template-pcuic"
43 ];
44 "quotation" = [
45 "template-rocq"
46 "pcuic"
47 "template-pcuic"
48 ];
49 "safechecker-plugin" = [
50 "template-pcuic"
51 "safechecker"
52 ];
53 "erasure-plugin" = [
54 "template-pcuic"
55 "erasure"
56 ];
57 "translations" = [ "template-rocq" ];
58 "all" = [
59 "safechecker-plugin"
60 "erasure-plugin"
61 "translations"
62 "quotation"
63 ];
64 };
65
66 template-rocq = metarocq_ "template-rocq";
67
68 metarocq_ =
69 package:
70 let
71 metarocq-deps = lib.optionals (package != "single") (map metarocq_ packages.${package});
72 pkgpath = if package == "single" then "./" else "./${package}";
73 pname = if package == "all" then "metarocq" else "metarocq-${package}";
74 pkgallMake = ''
75 mkdir all
76 echo "all:" > all/Makefile
77 echo "install:" >> all/Makefile
78 '';
79 derivation = mkCoqDerivation (
80 {
81 inherit
82 version
83 pname
84 defaultVersion
85 release
86 releaseRev
87 repo
88 owner
89 ;
90
91 mlPlugin = true;
92 propagatedBuildInputs = [
93 equations
94 coq.ocamlPackages.zarith
95 coq.ocamlPackages.stdlib-shims
96 ]
97 ++ metarocq-deps;
98
99 patchPhase = ''
100 patchShebangs ./configure.sh
101 patchShebangs ./template-rocq/update_plugin.sh
102 patchShebangs ./template-rocq/gen-src/to-lower.sh
103 patchShebangs ./safechecker-plugin/clean_extraction.sh
104 patchShebangs ./erasure-plugin/clean_extraction.sh
105 echo "CAMLFLAGS+=-w -60 # Unused module" >> ./safechecker/Makefile.plugin.local
106 sed -i -e 's/mv $i $newi;/mv $i tmp; mv tmp $newi;/' ./template-rocq/gen-src/to-lower.sh ./safechecker-plugin/clean_extraction.sh ./erasure-plugin/clean_extraction.sh
107 '';
108
109 configurePhase =
110 lib.optionalString (package == "all") pkgallMake
111 + ''
112 touch ${pkgpath}/metarocq-config
113 ''
114 +
115 lib.optionalString
116 (lib.elem package [
117 "erasure"
118 "template-pcuic"
119 "quotation"
120 "safechecker-plugin"
121 "erasure-plugin"
122 "translations"
123 ])
124 ''
125 echo "-I ${template-rocq}/lib/coq/${coq.coq-version}/user-contrib/MetaRocq/Template/" > ${pkgpath}/metarocq-config
126 ''
127 + lib.optionalString (package == "single") ''
128 ./configure.sh local
129 '';
130
131 preBuild = ''
132 cd ${pkgpath}
133 '';
134
135 meta = {
136 homepage = "https://metarocq.github.io/";
137 license = lib.licenses.mit;
138 maintainers = with lib.maintainers; [ cohencyril ];
139 };
140 }
141 // lib.optionalAttrs (package != "single") {
142 passthru = lib.mapAttrs (package: deps: metarocq_ package) packages;
143 }
144 );
145 in
146 derivation;
147in
148metarocq_ (if single then "single" else "all")