Skip to content

Commit e8d7787

Browse files
author
Michael Raitza
committed
Add Nix flakes-based build scripts
1 parent 1d5976a commit e8d7787

File tree

6 files changed

+298
-0
lines changed

6 files changed

+298
-0
lines changed

‎.github/nix-makes.yml‎

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
name: Nix Makes CI
2+
permissions: read-all
3+
concurrency:
4+
cancel-in-progress: true
5+
group: ${{ github.actor }}
6+
7+
on:
8+
push:
9+
branches:
10+
- main
11+
- coq-8.17
12+
pull_request:
13+
paths:
14+
- .github/workflows/**
15+
pull_request_target:
16+
types:
17+
- opened
18+
- synchronize
19+
- reopened
20+
21+
jobs:
22+
build:
23+
runs-on: ubuntu-latest
24+
25+
steps:
26+
- uses: actions/checkout@v4
27+
- uses: docker://ghcr.io/fluidattacks/makes/amd64:24.02
28+
with:
29+
args: sh -c "chown -R root:root /github/workspace && m . /build"

‎.nix/default.nix‎

Lines changed: 95 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,95 @@
1+
{ lib, fetchzip,
2+
mkCoqDerivation, recurseIntoAttrs, single ? false,
3+
coqPackages, coq, equations, version ? null }@args:
4+
with builtins // lib;
5+
let
6+
repo = "metacoq";
7+
owner = "MetaCoq";
8+
defaultVersion = with versions; switch coq.coq-version [
9+
{ case = "8.11"; out = "1.0-beta2-8.11"; }
10+
{ case = "8.12"; out = "1.0-beta2-8.12"; }
11+
# Do not provide 8.13 because it does not compile with equations 1.3 provided by default (only 1.2.3)
12+
# { 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 = "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.2-8.19"; }
19+
] null;
20+
release = {
21+
# Release tarballs from GitHub or local sources for Version "dev".
22+
"1.0-beta2-8.11".sha256 = "sha256-I9YNk5Di6Udvq5/xpLSNflfjRyRH8fMnRzbo3uhpXNs=";
23+
"1.0-beta2-8.12".sha256 = "sha256-I8gpmU9rUQJh0qfp5KOgDNscVvCybm5zX4TINxO1TVA=";
24+
"1.0-beta2-8.13".sha256 = "sha256-IC56/lEDaAylUbMCfG/3cqOBZniEQk8jmI053DBO5l8=";
25+
"1.0-8.14".sha256 = "sha256-iRnaNeHt22JqxMNxOGPPycrO9EoCVjusR2s0GfON1y0=";
26+
"1.0-8.15".sha256 = "sha256-8RUC5dHNfLJtJh+IZG4nPTAVC8ZKVh2BHedkzjwLf/k=";
27+
"1.0-8.16".sha256 = "sha256-7rkCAN4PNnMgsgUiiLe2TnAliknN75s2SfjzyKCib/o=";
28+
"1.3.1-8.17".sha256 = "sha256-l0/QLC7V3zSk/FsaE2eL6tXy2BzbcI5MAk/c+FESwnc=";
29+
"1.3.1-8.18".sha256 = "sha256-L6Ym4Auwqaxv5tRmJLSVC812dxCqdUU5aN8+t5HVYzY=";
30+
"1.3.1-8.19".sha256 = "sha256-fZED/Uel1jt5XF83dR6HfyhSkfBdLkET8C/ArDgsm64=";
31+
"1.3.2-8.19".sha256 = "sha256-e5Pm1AhaQrO6JoZylSXYWmeXY033QflQuCBZhxGH8MA=";
32+
"dev".src = lib.const (lib.cleanSource ../.);
33+
};
34+
releaseRev = v: "v${v}";
35+
36+
# list of core metacoq packages sorted by dependency order
37+
packages = [ "utils" "common" "template-coq" "pcuic" "safechecker" "template-pcuic" "erasure" "quotation" "safechecker-plugin" "erasure-plugin" "all" ];
38+
39+
template-coq = metacoq_ "template-coq";
40+
41+
metacoq_ = package: let
42+
metacoq-deps = if package == "single" then []
43+
else map metacoq_ (head (splitList (pred.equal package) packages));
44+
pkgpath = if package == "single" then "./" else "./${package}";
45+
pname = if package == "all" then "metacoq" else "metacoq-${package}";
46+
pkgallMake = ''
47+
mkdir all
48+
echo "all:" > all/Makefile
49+
echo "install:" >> all/Makefile
50+
'' ;
51+
derivation = (mkCoqDerivation ({
52+
inherit version pname defaultVersion release releaseRev repo owner;
53+
54+
mlPlugin = true;
55+
propagatedBuildInputs = [ equations coq.ocamlPackages.zarith ] ++ metacoq-deps;
56+
57+
patchPhase = ''
58+
patchShebangs ./configure.sh
59+
patchShebangs ./template-coq/update_plugin.sh
60+
patchShebangs ./template-coq/gen-src/to-lower.sh
61+
patchShebangs ./safechecker-plugin/clean_extraction.sh
62+
patchShebangs ./erasure-plugin/clean_extraction.sh
63+
echo "CAMLFLAGS+=-w -60 # Unused module" >> ./safechecker/Makefile.plugin.local
64+
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
65+
'' ;
66+
67+
configurePhase = optionalString (package == "all") pkgallMake + ''
68+
touch ${pkgpath}/metacoq-config
69+
'' + optionalString (elem package ["safechecker" "erasure" "template-pcuic" "quotation" "safechecker-plugin" "erasure-plugin"]) ''
70+
echo "-I ${template-coq}/lib/coq/${coq.coq-version}/user-contrib/MetaCoq/Template/" > ${pkgpath}/metacoq-config
71+
'' + optionalString (package == "single") ''
72+
./configure.sh local
73+
'';
74+
75+
preBuild = ''
76+
cd ${pkgpath}
77+
'' ;
78+
79+
meta = {
80+
homepage = "https://metacoq.github.io/";
81+
license = licenses.mit;
82+
maintainers = with maintainers; [ cohencyril ];
83+
};
84+
} // optionalAttrs (package != "single")
85+
{ passthru = genAttrs packages metacoq_; })
86+
).overrideAttrs (o:
87+
let requiresOcamlStdlibShims = versionAtLeast o.version "1.0-8.16" ||
88+
(o.version == "dev" && (versionAtLeast coq.coq-version "8.16" || coq.coq-version == "dev")) ;
89+
in
90+
{
91+
propagatedBuildInputs = o.propagatedBuildInputs ++ optional requiresOcamlStdlibShims coq.ocamlPackages.stdlib-shims;
92+
});
93+
in derivation;
94+
in
95+
metacoq_ (if single then "single" else "all")

‎.nix/overlay.nix‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
final: prev: let
2+
pkg = ./default.nix;
3+
name = "metacoq";
4+
injectPkg = name: set:
5+
prev.${name}.overrideScope (self: _: {
6+
metacoq = self.callPackage pkg {};
7+
metacoq-dev = self.callPackage pkg { version = "dev"; };
8+
});
9+
in (prev.lib.mapAttrs injectPkg {
10+
inherit (final) coqPackages_8_17 coqPackages_8_18 coqPackages_8_19;
11+
})

‎flake.lock‎

Lines changed: 96 additions & 0 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎flake.nix‎

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
{
2+
description = "MetaCoq is a project formalizing Coq in Coq";
3+
4+
inputs = {
5+
flake-utils.url = "github:numtide/flake-utils";
6+
makes.url = "github:fluidattacks/makes/24.02";
7+
nixpkgs.url = "github:nixos/nixpkgs/release-24.05";
8+
};
9+
10+
outputs = { self, flake-utils, makes, nixpkgs, ... }:
11+
with flake-utils.lib;
12+
eachDefaultSystem (system: let
13+
pkgs = import nixpkgs {
14+
inherit system;
15+
overlays = [self.overlays.default];
16+
};
17+
in {
18+
devShells.default = self.packages.${system}.default;
19+
20+
packages = {
21+
default = self.packages.${system}.coqPackages_8_17-metacoq-dev;
22+
} // (with pkgs.lib; foldl' mergeAttrs { }
23+
(concatMap (coq: [{
24+
# Released packages using upstream tarballs (see .nix/default.nix)
25+
"${coq}-metacoq" = pkgs.${coq}.metacoq;
26+
# Local source tree
27+
"${coq}-metacoq-dev" = pkgs.${coq}."metacoq-dev";
28+
}])
29+
[ "coqPackages_8_17" "coqPackages_8_18" "coqPackages_8_19" ]));
30+
31+
# CI runner
32+
apps.makes = makes.apps.${system}.default;
33+
})
34+
// {
35+
overlays.default = import .nix/overlay.nix;
36+
};
37+
}

‎makes.nix‎

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
{
2+
fetchNixpkgs,
3+
inputs,
4+
makeSearchPaths,
5+
...
6+
}: {
7+
cache.readNixos = true;
8+
formatNix = {
9+
enable = true;
10+
targets = ["/"];
11+
};
12+
inputs = {
13+
# Use nixpkgs from recorded flake.lock
14+
nixpkgs = let
15+
nixpkgsAttrs = (builtins.fromJSON (builtins.readFile ./flake.lock)).nodes.nixpkgs_2.locked;
16+
in
17+
fetchNixpkgs {
18+
rev = nixpkgsAttrs.rev;
19+
sha256 = nixpkgsAttrs.narHash;
20+
acceptAndroidSdkLicense = false;
21+
allowUnfree = false;
22+
overlays = [(import .nix/overlay.nix)];
23+
};
24+
};
25+
outputs."/build" = makeSearchPaths {
26+
bin = [
27+
inputs.nixpkgs.coqPackages_8_17.metacoq-dev
28+
];
29+
};
30+
}

0 commit comments

Comments
 (0)