From e8d7787bb8476d4b5b80183bf9ef4700c3128394 Mon Sep 17 00:00:00 2001 From: Michael Raitza Date: Wed, 31 Jul 2024 17:57:05 +0200 Subject: [PATCH] Add Nix flakes-based build scripts --- .github/nix-makes.yml | 29 +++++++++++++ .nix/default.nix | 95 ++++++++++++++++++++++++++++++++++++++++++ .nix/overlay.nix | 11 +++++ flake.lock | 96 +++++++++++++++++++++++++++++++++++++++++++ flake.nix | 37 +++++++++++++++++ makes.nix | 30 ++++++++++++++ 6 files changed, 298 insertions(+) create mode 100644 .github/nix-makes.yml create mode 100644 .nix/default.nix create mode 100644 .nix/overlay.nix create mode 100644 flake.lock create mode 100644 flake.nix create mode 100644 makes.nix diff --git a/.github/nix-makes.yml b/.github/nix-makes.yml new file mode 100644 index 000000000..32ed56ac3 --- /dev/null +++ b/.github/nix-makes.yml @@ -0,0 +1,29 @@ +name: Nix Makes CI +permissions: read-all +concurrency: + cancel-in-progress: true + group: ${{ github.actor }} + +on: + push: + branches: + - main + - coq-8.17 + pull_request: + paths: + - .github/workflows/** + pull_request_target: + types: + - opened + - synchronize + - reopened + +jobs: + build: + runs-on: ubuntu-latest + + steps: + - uses: actions/checkout@v4 + - uses: docker://ghcr.io/fluidattacks/makes/amd64:24.02 + with: + args: sh -c "chown -R root:root /github/workspace && m . /build" diff --git a/.nix/default.nix b/.nix/default.nix new file mode 100644 index 000000000..f54f51530 --- /dev/null +++ b/.nix/default.nix @@ -0,0 +1,95 @@ +{ lib, fetchzip, + mkCoqDerivation, recurseIntoAttrs, single ? false, + coqPackages, coq, equations, version ? null }@args: +with builtins // lib; +let + repo = "metacoq"; + owner = "MetaCoq"; + defaultVersion = with versions; switch coq.coq-version [ + { case = "8.11"; out = "1.0-beta2-8.11"; } + { case = "8.12"; out = "1.0-beta2-8.12"; } + # Do not provide 8.13 because it does not compile with equations 1.3 provided by default (only 1.2.3) + # { case = "8.13"; out = "1.0-beta2-8.13"; } + { case = "8.14"; out = "1.0-8.14"; } + { case = "8.15"; out = "1.0-8.15"; } + { case = "8.16"; out = "1.0-8.16"; } + { case = "8.17"; out = "1.3.1-8.17"; } + { case = "8.18"; out = "1.3.1-8.18"; } + { case = "8.19"; out = "1.3.2-8.19"; } + ] null; + release = { + # Release tarballs from GitHub or local sources for Version "dev". + "1.0-beta2-8.11".sha256 = "sha256-I9YNk5Di6Udvq5/xpLSNflfjRyRH8fMnRzbo3uhpXNs="; + "1.0-beta2-8.12".sha256 = "sha256-I8gpmU9rUQJh0qfp5KOgDNscVvCybm5zX4TINxO1TVA="; + "1.0-beta2-8.13".sha256 = "sha256-IC56/lEDaAylUbMCfG/3cqOBZniEQk8jmI053DBO5l8="; + "1.0-8.14".sha256 = "sha256-iRnaNeHt22JqxMNxOGPPycrO9EoCVjusR2s0GfON1y0="; + "1.0-8.15".sha256 = "sha256-8RUC5dHNfLJtJh+IZG4nPTAVC8ZKVh2BHedkzjwLf/k="; + "1.0-8.16".sha256 = "sha256-7rkCAN4PNnMgsgUiiLe2TnAliknN75s2SfjzyKCib/o="; + "1.3.1-8.17".sha256 = "sha256-l0/QLC7V3zSk/FsaE2eL6tXy2BzbcI5MAk/c+FESwnc="; + "1.3.1-8.18".sha256 = "sha256-L6Ym4Auwqaxv5tRmJLSVC812dxCqdUU5aN8+t5HVYzY="; + "1.3.1-8.19".sha256 = "sha256-fZED/Uel1jt5XF83dR6HfyhSkfBdLkET8C/ArDgsm64="; + "1.3.2-8.19".sha256 = "sha256-e5Pm1AhaQrO6JoZylSXYWmeXY033QflQuCBZhxGH8MA="; + "dev".src = lib.const (lib.cleanSource ../.); + }; + releaseRev = v: "v${v}"; + + # list of core metacoq packages sorted by dependency order + packages = [ "utils" "common" "template-coq" "pcuic" "safechecker" "template-pcuic" "erasure" "quotation" "safechecker-plugin" "erasure-plugin" "all" ]; + + template-coq = metacoq_ "template-coq"; + + metacoq_ = package: let + metacoq-deps = if package == "single" then [] + else map metacoq_ (head (splitList (pred.equal package) packages)); + pkgpath = if package == "single" then "./" else "./${package}"; + pname = if package == "all" then "metacoq" else "metacoq-${package}"; + pkgallMake = '' + mkdir all + echo "all:" > all/Makefile + echo "install:" >> all/Makefile + '' ; + derivation = (mkCoqDerivation ({ + inherit version pname defaultVersion release releaseRev repo owner; + + mlPlugin = true; + propagatedBuildInputs = [ equations coq.ocamlPackages.zarith ] ++ metacoq-deps; + + patchPhase = '' + patchShebangs ./configure.sh + patchShebangs ./template-coq/update_plugin.sh + patchShebangs ./template-coq/gen-src/to-lower.sh + patchShebangs ./safechecker-plugin/clean_extraction.sh + patchShebangs ./erasure-plugin/clean_extraction.sh + echo "CAMLFLAGS+=-w -60 # Unused module" >> ./safechecker/Makefile.plugin.local + 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 + '' ; + + configurePhase = optionalString (package == "all") pkgallMake + '' + touch ${pkgpath}/metacoq-config + '' + optionalString (elem package ["safechecker" "erasure" "template-pcuic" "quotation" "safechecker-plugin" "erasure-plugin"]) '' + echo "-I ${template-coq}/lib/coq/${coq.coq-version}/user-contrib/MetaCoq/Template/" > ${pkgpath}/metacoq-config + '' + optionalString (package == "single") '' + ./configure.sh local + ''; + + preBuild = '' + cd ${pkgpath} + '' ; + + meta = { + homepage = "https://metacoq.github.io/"; + license = licenses.mit; + maintainers = with maintainers; [ cohencyril ]; + }; + } // optionalAttrs (package != "single") + { passthru = genAttrs packages metacoq_; }) + ).overrideAttrs (o: + let requiresOcamlStdlibShims = versionAtLeast o.version "1.0-8.16" || + (o.version == "dev" && (versionAtLeast coq.coq-version "8.16" || coq.coq-version == "dev")) ; + in + { + propagatedBuildInputs = o.propagatedBuildInputs ++ optional requiresOcamlStdlibShims coq.ocamlPackages.stdlib-shims; + }); + in derivation; +in +metacoq_ (if single then "single" else "all") diff --git a/.nix/overlay.nix b/.nix/overlay.nix new file mode 100644 index 000000000..50aaf4041 --- /dev/null +++ b/.nix/overlay.nix @@ -0,0 +1,11 @@ +final: prev: let + pkg = ./default.nix; + name = "metacoq"; + injectPkg = name: set: + prev.${name}.overrideScope (self: _: { + metacoq = self.callPackage pkg {}; + metacoq-dev = self.callPackage pkg { version = "dev"; }; + }); +in (prev.lib.mapAttrs injectPkg { + inherit (final) coqPackages_8_17 coqPackages_8_18 coqPackages_8_19; +}) diff --git a/flake.lock b/flake.lock new file mode 100644 index 000000000..7e3f68b68 --- /dev/null +++ b/flake.lock @@ -0,0 +1,96 @@ +{ + "nodes": { + "flake-utils": { + "inputs": { + "systems": "systems" + }, + "locked": { + "lastModified": 1710146030, + "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=", + "owner": "numtide", + "repo": "flake-utils", + "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a", + "type": "github" + }, + "original": { + "owner": "numtide", + "repo": "flake-utils", + "type": "github" + } + }, + "makes": { + "inputs": { + "nixpkgs": "nixpkgs" + }, + "locked": { + "lastModified": 1722040633, + "narHash": "sha256-d7/emJX5BmM6dpGBRR66gSwywHQT8K2aoweG2R2/74U=", + "owner": "fluidattacks", + "repo": "makes", + "rev": "9b48d0e155d7fb08fc4e8318380e7a0cf359a202", + "type": "github" + }, + "original": { + "owner": "fluidattacks", + "ref": "24.02", + "repo": "makes", + "type": "github" + } + }, + "nixpkgs": { + "locked": { + "lastModified": 1667092106, + "narHash": "sha256-ZQwHNd/RemupaV52ePNNv4Kp+LHzPjssEAumLijum4E=", + "owner": "nix-community", + "repo": "nixpkgs.lib", + "rev": "2c15a4c90737d33309daf869bae0daaa35eeb264", + "type": "github" + }, + "original": { + "owner": "nix-community", + "repo": "nixpkgs.lib", + "type": "github" + } + }, + "nixpkgs_2": { + "locked": { + "lastModified": 1722435350, + "narHash": "sha256-Ga464yboezJHH8XIPVIelDn9ZsLMCN3TqnuFNXvHO2w=", + "owner": "nixos", + "repo": "nixpkgs", + "rev": "e17b82b20adb7f20511da210429eac1bd2fa7bf7", + "type": "github" + }, + "original": { + "owner": "nixos", + "ref": "release-24.05", + "repo": "nixpkgs", + "type": "github" + } + }, + "root": { + "inputs": { + "flake-utils": "flake-utils", + "makes": "makes", + "nixpkgs": "nixpkgs_2" + } + }, + "systems": { + "locked": { + "lastModified": 1681028828, + "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", + "owner": "nix-systems", + "repo": "default", + "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", + "type": "github" + }, + "original": { + "owner": "nix-systems", + "repo": "default", + "type": "github" + } + } + }, + "root": "root", + "version": 7 +} diff --git a/flake.nix b/flake.nix new file mode 100644 index 000000000..f3fa4963c --- /dev/null +++ b/flake.nix @@ -0,0 +1,37 @@ +{ + description = "MetaCoq is a project formalizing Coq in Coq"; + + inputs = { + flake-utils.url = "github:numtide/flake-utils"; + makes.url = "github:fluidattacks/makes/24.02"; + nixpkgs.url = "github:nixos/nixpkgs/release-24.05"; + }; + + outputs = { self, flake-utils, makes, nixpkgs, ... }: + with flake-utils.lib; + eachDefaultSystem (system: let + pkgs = import nixpkgs { + inherit system; + overlays = [self.overlays.default]; + }; + in { + devShells.default = self.packages.${system}.default; + + packages = { + default = self.packages.${system}.coqPackages_8_17-metacoq-dev; + } // (with pkgs.lib; foldl' mergeAttrs { } + (concatMap (coq: [{ + # Released packages using upstream tarballs (see .nix/default.nix) + "${coq}-metacoq" = pkgs.${coq}.metacoq; + # Local source tree + "${coq}-metacoq-dev" = pkgs.${coq}."metacoq-dev"; + }]) + [ "coqPackages_8_17" "coqPackages_8_18" "coqPackages_8_19" ])); + + # CI runner + apps.makes = makes.apps.${system}.default; + }) + // { + overlays.default = import .nix/overlay.nix; + }; +} diff --git a/makes.nix b/makes.nix new file mode 100644 index 000000000..d7e6d5bec --- /dev/null +++ b/makes.nix @@ -0,0 +1,30 @@ +{ + fetchNixpkgs, + inputs, + makeSearchPaths, + ... +}: { + cache.readNixos = true; + formatNix = { + enable = true; + targets = ["/"]; + }; + inputs = { + # Use nixpkgs from recorded flake.lock + nixpkgs = let + nixpkgsAttrs = (builtins.fromJSON (builtins.readFile ./flake.lock)).nodes.nixpkgs_2.locked; + in + fetchNixpkgs { + rev = nixpkgsAttrs.rev; + sha256 = nixpkgsAttrs.narHash; + acceptAndroidSdkLicense = false; + allowUnfree = false; + overlays = [(import .nix/overlay.nix)]; + }; + }; + outputs."/build" = makeSearchPaths { + bin = [ + inputs.nixpkgs.coqPackages_8_17.metacoq-dev + ]; + }; +}