From a29f059442eb7817281ce2ae2863ccc9e0a79542 Mon Sep 17 00:00:00 2001 From: Michael Raitza Date: Tue, 21 May 2024 18:04:18 +0200 Subject: [PATCH] Restructure nix tool chain and use makes for CI MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Makes provides several interesting tools for our context: - attestation of the build products (i.e. for the verified Kôika compiler) - linters and formatters - container image generators and other deployment / packaging tools --- .github/workflows/flake-build.yml | 5 +- default.nix | 72 ++++++++++++++++ flake.nix | 132 ++++++------------------------ ignored_paths.nix | 9 ++ makes.lock.nix | 6 ++ makes.nix | 32 ++++++++ overlay.nix | 16 ++++ 7 files changed, 164 insertions(+), 108 deletions(-) create mode 100644 default.nix create mode 100644 ignored_paths.nix create mode 100644 makes.lock.nix create mode 100644 makes.nix create mode 100644 overlay.nix diff --git a/.github/workflows/flake-build.yml b/.github/workflows/flake-build.yml index e6730c1..86634fd 100644 --- a/.github/workflows/flake-build.yml +++ b/.github/workflows/flake-build.yml @@ -20,8 +20,7 @@ jobs: # Steps represent a sequence of tasks that will be executed as part of the job steps: - uses: actions/checkout@v4 - - uses: cachix/install-nix-action@v25 + - uses: docker://ghcr.io/fluidattacks/makes/amd64:24.02 with: github_access_token: ${{ secrets.GITHUB_TOKEN }} - - run: nix build - - run: nix flake check + - run: m . /build diff --git a/default.nix b/default.nix new file mode 100644 index 0000000..1731628 --- /dev/null +++ b/default.nix @@ -0,0 +1,72 @@ +{ + lib, + mkCoqDerivation, + coq, + boost, + python3, + sphinx, + doCheck ? false, +}: +mkCoqDerivation rec { + pname = "koika"; + defaultVersion = "0.0.1"; + + opam-name = "koika"; + useDune = true; + + release."0.0.1" = { + src = lib.const (lib.cleanSourceWith { + src = lib.cleanSource ./.; + filter = let + inherit (lib) all hasSuffix; + ignorePaths = xs: path: all (x: ! hasSuffix x path) xs; + in + path: _: ignorePaths (import ./ignored_paths.nix) path; + }); + }; + + enableParallelBuilding = true; + + nativeBuildInputs = [ + python3 + sphinx + ]; + + buildInputs = [ + boost + ]; + + propagatedBuildInputs = with coq.ocamlPackages; [ + findlib + base + core + core_unix + stdio + parsexp + hashcons + zarith + ]; + + preInstall = '' + dune build README.html + mkdir -p $out/share/doc/koika + cp README.html $out/share/doc/koika/ + ''; + + postInstall = '' + mkdir -p "$OCAMLFIND_DESTDIR" + mv "$out/lib/koika" "$OCAMLFIND_DESTDIR" + ''; + + inherit doCheck; + checkPhase = '' + runHook preCheck + ./coq.kernel.hack.sh + dune build @runtest + runHook postCheck + ''; + + shellHook = '' + [ -x coq.kernel.hack.sh ] && ./coq.kernel.hack.sh + ''; +} diff --git a/flake.nix b/flake.nix index 0754bf4..f8a78e1 100644 --- a/flake.nix +++ b/flake.nix @@ -6,114 +6,36 @@ flake-utils.url = "github:numtide/flake-utils"; }; - outputs = { self, flake-utils, nixpkgs, ... }: + outputs = { + self, + flake-utils, + nixpkgs, + ... + }: with flake-utils.lib; - let - koikaPkg = { lib, mkCoqDerivation, coq, boost, python3, sphinx }: mkCoqDerivation rec { - pname = "koika"; - defaultVersion = "0.0.1"; - - opam-name = "koika"; - useDune = true; - - release."0.0.1" = { - src = lib.const (lib.cleanSourceWith { - src = lib.cleanSource ./.; - filter = let inherit (lib) hasSuffix; in path: type: - (! hasSuffix ".gitignore" path) - && (! hasSuffix "flake.nix" path) - && (! hasSuffix "flake.lock" path) - && (! hasSuffix "_build" path); - }); + eachDefaultSystem (system: let + pkgs = import nixpkgs { + inherit system; + overlays = [self.overlays.default]; + }; + in { + checks = { + koika = self.packages.${system}.default.override { + doCheck = true; + }; }; - enableParallelBuilding = true; - - nativeBuildInputs = [ - python3 - sphinx - ]; - - buildInputs = [ - boost - ]; - - propagatedBuildInputs = with coq.ocamlPackages; [ - findlib - base - core - core_unix - stdio - parsexp - hashcons - zarith - ]; - - preInstall = '' - dune build README.html - mkdir -p $out/share/doc/koika - cp README.html $out/share/doc/koika/ - ''; - - postInstall = '' - mkdir -p "$OCAMLFIND_DESTDIR" - mv "$out/lib/koika" "$OCAMLFIND_DESTDIR" - ''; - - # NOTE: Also build the examples, because they use additional parts of - # the Dune toolchain. - checkPhase = '' - runHook preCheck - ./coq.kernel.hack.sh - dune build @runtest - runHook postCheck - ''; - - shellHook = '' - [ -x coq.kernel.hack.sh ] && ./coq.kernel.hack.sh - ''; - }; - - in eachDefaultSystem (system: let - - pkgs = import nixpkgs { - inherit system; - overlays = [ self.overlays.default ]; - }; - - - in { - - checks = { - koika = self.packages.${system}.default.overrideAttrs (_: { - doCheck = true; - }); - }; - - devShells.default = self.checks.${system}.koika; - - packages = { - default = self.packages.${system}.coq8_14-koika; - coq8_14-koika = pkgs.coqPackages_8_14.koika; - coqDev-koika = pkgs.coqPackages_koika.koika; - }; - - }) // { + devShells.default = self.checks.${system}.koika; - # NOTE: To use this flake, apply the following overlay to nixpkgs and use - # koika from its respective coqPackages_VER attribute set! - overlays.default = final: prev: let - injectKoika = name: set: - prev.${name}.overrideScope (self: _: { - koika = self.callPackage koikaPkg {}; - }); - in (nixpkgs.lib.mapAttrs injectKoika { - inherit (final) coqPackages_8_14; - }) // { - coqPackages_koika = prev.coqPackages_8_14.overrideScope (self: super: { - coq = super.coq.override { customOCamlPackages = prev.ocaml-ng.ocamlPackages_4_09; }; - koika = self.callPackage koikaPkg {}; - }); + packages = { + default = self.packages.${system}.coq8_14-koika; + coq8_14-koika = pkgs.coqPackages_8_14.koika; + coqDev-koika = pkgs.coqPackages_koika.koika; + }; + }) + // { + # NOTE: To use this flake, apply the following overlay to nixpkgs and use + # koika from its respective coqPackages_VER attribute set! + overlays.default = import ./overlay.nix; }; - }; } diff --git a/ignored_paths.nix b/ignored_paths.nix new file mode 100644 index 0000000..840b4a4 --- /dev/null +++ b/ignored_paths.nix @@ -0,0 +1,9 @@ +[ + "default.nix" + "flake.nix" + "makes.lock.nix" + "makes.nix" + "overlay.nix" + "makes" + ".gitignore" +] diff --git a/makes.lock.nix b/makes.lock.nix new file mode 100644 index 0000000..579f46c --- /dev/null +++ b/makes.lock.nix @@ -0,0 +1,6 @@ +{ + makesSrc = builtins.fetchGit { + url = "https://github.com/fluidattacks/makes"; + ref = "refs/tags/24.02"; + }; +} diff --git a/makes.nix b/makes.nix new file mode 100644 index 0000000..df28534 --- /dev/null +++ b/makes.nix @@ -0,0 +1,32 @@ +{ + 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.locked; + in + fetchNixpkgs { + rev = nixpkgsAttrs.rev; + sha256 = nixpkgsAttrs.narHash; + acceptAndroidSdkLicense = false; + allowUnfree = false; + overlays = [(import ./overlay.nix)]; + }; + }; + outputs."/build" = makeSearchPaths { + bin = [ + (inputs.nixpkgs.coqPackages_8_14.koika.override { + doCheck = true; + }) + ]; + }; +} diff --git a/overlay.nix b/overlay.nix new file mode 100644 index 0000000..a254c8d --- /dev/null +++ b/overlay.nix @@ -0,0 +1,16 @@ +final: prev: let + koikaPkg = ./default.nix; + injectKoika = name: set: + prev.${name}.overrideScope (self: _: { + koika = self.callPackage koikaPkg {}; + }); +in + (prev.lib.mapAttrs injectKoika { + inherit (final) coqPackages_8_14; + }) + // { + coqPackages_koika = prev.coqPackages_8_14.overrideScope (self: super: { + coq = super.coq.override {customOCamlPackages = prev.ocaml-ng.ocamlPackages_4_09;}; + koika = self.callPackage koikaPkg {}; + }); + }