From 03acc5ea1f860b5a32539dc05f0d04df200c3c8d Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sun, 29 Nov 2020 11:30:45 +0100 Subject: [PATCH] feat: Nix: sanitized build --- flake.nix | 95 +++------------------------------------- nix/bootstrap.nix | 6 ++- nix/buildLeanPackage.nix | 3 +- nix/packages.nix | 89 +++++++++++++++++++++++++++++++++++++ 4 files changed, 101 insertions(+), 92 deletions(-) create mode 100644 nix/packages.nix diff --git a/flake.nix b/flake.nix index 3408ffde17..3bcf89ae40 100644 --- a/flake.nix +++ b/flake.nix @@ -14,101 +14,18 @@ }; outputs = { self, nixpkgs, flake-utils, temci, nix, mdBook }: flake-utils.lib.eachDefaultSystem (system: - with nixpkgs.legacyPackages.${system}; let - nix-pinned = writeShellScriptBin "nix" '' - ${nix.defaultPackage.${system}}/bin/nix --experimental-features 'nix-command flakes' --extra-substituters https://lean4.cachix.org/ --option warn-dirty false $@ - ''; - llvmPackages = llvmPackages_10; - cc = ccacheWrapper.override rec { - # macOS doesn't like the lld override, but I guess it already uses that anyway - cc = if system == "x86_64-darwin" then llvmPackages.clang else llvmPackages.clang.override { - # linker go brrr - bintools = llvmPackages.lldClang.bintools; - }; - extraConfig = '' - export CCACHE_DIR=/nix/var/cache/ccache - export CCACHE_UMASK=007 - export CCACHE_BASE_DIR=$NIX_BUILD_TOP - [ -d $CCACHE_DIR ] || exec ${cc}/bin/$(basename "$0") "$@" - ''; + packages = nixpkgs.legacyPackages.${system}.callPackage (./nix/packages.nix) { inherit nix temci mdBook; }; + in { + packages = packages // rec { + debug = packages.override { debug = true; }; + sanitized = packages.override { extraCMakeFlags = [ "-DLEAN_EXTRA_CXX_FLAGS=-fsanitize=address,undefined" "-DLEANC_EXTRA_FLAGS=-fsanitize=address,undefined" "-DSMALL_ALLOCATOR=OFF" ]; }; + sandebug = sanitized.override { debug = true; }; }; - lean = callPackage (import ./nix/bootstrap.nix) { - stdenv = overrideCC stdenv cc; - inherit buildLeanPackage; - }; - buildLeanPackage = callPackage (import ./nix/buildLeanPackage.nix) { - inherit (lean) stdenv leanc; - lean = lean.stage1; - inherit lean-emacs; - nix = nix-pinned; - }; - lean4-mode = emacsPackages.melpaBuild { - pname = "lean4-mode"; - version = "1"; - src = ./lean4-mode; - packageRequires = with pkgs.emacsPackages.melpaPackages; [ dash dash-functional f flycheck s ]; - recipe = pkgs.writeText "recipe" '' - (lean4-mode :repo "leanprover/lean4" :fetcher github :files ("*.el")) - ''; - fileSpecs = [ "*.el" ]; - }; - lean-emacs = emacsWithPackages (epkgs: - with epkgs; [ dash dash-functional f flycheck s ] ++ [ lean4-mode ]); - lean-mdbook = mdbook.overrideAttrs (drv: rec { - name = "lean-${mdbook.name}"; - src = mdBook; - cargoDeps = drv.cargoDeps.overrideAttrs (_: { - inherit src; - outputHash = "sha256-BTm76YxY/tI4Pg53UbR+7KiQydb9L0FGYNZ0UKGyacw="; - }); - doCheck = false; - }); - doc = stdenv.mkDerivation { - name ="lean-doc"; - src = ./doc; - buildInputs = [ lean-mdbook ]; - buildCommand = '' - mdbook build -d $out $src - ''; - }; - # We use a separate derivation instead of `checkPhase` so we can push it but not `doc` to the binary cache - doc-test = stdenv.mkDerivation { - name ="lean-doc-test"; - src = ./doc; - buildInputs = [ lean-mdbook lean.stage1 strace ]; - patchPhase = '' - patchShebangs test - ''; - buildPhase = '' - ./test - mdbook test - touch $out - ''; - dontInstall = true; - }; - in rec { - packages = { - inherit cc lean4-mode buildLeanPackage llvmPackages; - lean = lean.stage1; - debug = lean.override { debug = true; }; - temci = (import temci {}).override { doCheck = false; }; - nix = nix-pinned; - nixpkgs = nixpkgs.legacyPackages.${system}; - ciShell = writeShellScriptBin "ciShell" '' - set -o pipefail - export PATH=${nix-pinned}/bin:${moreutils}/bin:$PATH - # prefix lines with cumulative and individual execution time - "$@" |& ts -i "(%.S)]" | ts -s "[%M:%S" - ''; - mdbook = lean-mdbook; - inherit doc doc-test; - } // lean.stage1.Lean // lean.stage1 // lean; defaultPackage = packages.lean; checks.lean = packages.test; - }) // rec { templates.pkg = { path = ./nix/templates/pkg; diff --git a/nix/bootstrap.nix b/nix/bootstrap.nix index d3f9918c16..45a7785e88 100644 --- a/nix/bootstrap.nix +++ b/nix/bootstrap.nix @@ -1,4 +1,6 @@ -{ debug ? false, stdenv, lib, cmake, gmp, buildLeanPackage, writeShellScriptBin }: +{ debug ? false, extraCMakeFlags ? [], + stdenv, lib, cmake, gmp, buildLeanPackage, writeShellScriptBin, + ... }: rec { inherit stdenv; buildCMake = args: stdenv.mkDerivation ({ @@ -6,7 +8,7 @@ rec { buildInputs = [ gmp ]; # https://github.com/NixOS/nixpkgs/issues/60919 hardeningDisable = [ "all" ]; - cmakeFlags = [ "-DSTAGE=1" "-DPREV_STAGE=./faux-prev-stage" ] ++ lib.optional (args.debug or debug) [ "-DCMAKE_BUILD_TYPE=Debug" ]; + cmakeFlags = [ "-DSTAGE=1" "-DPREV_STAGE=./faux-prev-stage" ] ++ extraCMakeFlags ++ lib.optional (args.debug or debug) [ "-DCMAKE_BUILD_TYPE=Debug" ]; dontStrip = (args.debug or debug); postConfigure = '' diff --git a/nix/buildLeanPackage.nix b/nix/buildLeanPackage.nix index bee228fdbf..5f87912cf3 100644 --- a/nix/buildLeanPackage.nix +++ b/nix/buildLeanPackage.nix @@ -1,6 +1,7 @@ { debug ? false, leanFlags ? [], leancFlags ? [], lean, lean-leanDeps ? lean, lean-final ? lean, leanc, - stdenv, lib, coreutils, gnused, writeShellScriptBin, bash, lean-emacs, nix, substituteAll, symlinkJoin, linkFarmFromDrvs }: + stdenv, lib, coreutils, gnused, writeShellScriptBin, bash, lean-emacs, nix, substituteAll, symlinkJoin, linkFarmFromDrvs, + ... }: with builtins; let # "Init.Core" ~> "Init/Core" modToPath = mod: replaceStrings ["."] ["/"] mod; diff --git a/nix/packages.nix b/nix/packages.nix new file mode 100644 index 0000000000..2acd3b9449 --- /dev/null +++ b/nix/packages.nix @@ -0,0 +1,89 @@ +{ pkgs, nix, temci, mdBook, ... } @ args: +with pkgs; +let + nix-pinned = writeShellScriptBin "nix" '' + ${nix.defaultPackage.${system}}/bin/nix --experimental-features 'nix-command flakes' --extra-substituters https://lean4.cachix.org/ --option warn-dirty false $@ + ''; + llvmPackages = llvmPackages_10; + cc = ccacheWrapper.override rec { + # macOS doesn't like the lld override, but I guess it already uses that anyway + cc = if system == "x86_64-darwin" then llvmPackages.clang else llvmPackages.clang.override { + # linker go brrr + bintools = llvmPackages.lldClang.bintools; + }; + extraConfig = '' + export CCACHE_DIR=/nix/var/cache/ccache + export CCACHE_UMASK=007 + export CCACHE_BASE_DIR=$NIX_BUILD_TOP + [ -d $CCACHE_DIR ] || exec ${cc}/bin/$(basename "$0") "$@" + ''; + }; + lean = callPackage (import ./bootstrap.nix) (args // { + stdenv = overrideCC llvmPackages.stdenv cc; + inherit buildLeanPackage; + }); + buildLeanPackage = callPackage (import ./buildLeanPackage.nix) (args // { + inherit (lean) stdenv leanc; + lean = lean.stage1; + inherit lean-emacs; + nix = nix-pinned; + }); + lean4-mode = emacsPackages.melpaBuild { + pname = "lean4-mode"; + version = "1"; + src = ../lean4-mode; + packageRequires = with pkgs.emacsPackages.melpaPackages; [ dash dash-functional f flycheck s ]; + recipe = pkgs.writeText "recipe" '' + (lean4-mode :repo "leanprover/lean4" :fetcher github :files ("*.el")) + ''; + fileSpecs = [ "*.el" ]; + }; + lean-emacs = emacsWithPackages (epkgs: + with epkgs; [ dash dash-functional f flycheck s ] ++ [ lean4-mode ]); + lean-mdbook = mdbook.overrideAttrs (drv: rec { + name = "lean-${mdbook.name}"; + src = mdBook; + cargoDeps = drv.cargoDeps.overrideAttrs (_: { + inherit src; + outputHash = "sha256-BTm76YxY/tI4Pg53UbR+7KiQydb9L0FGYNZ0UKGyacw="; + }); + doCheck = false; + }); + doc = stdenv.mkDerivation { + name ="lean-doc"; + src = ../doc; + buildInputs = [ lean-mdbook ]; + buildCommand = '' + mdbook build -d $out $src + ''; + }; + # We use a separate derivation instead of `checkPhase` so we can push it but not `doc` to the binary cache + doc-test = stdenv.mkDerivation { + name ="lean-doc-test"; + src = ../doc; + buildInputs = [ lean-mdbook lean.stage1 strace ]; + patchPhase = '' + patchShebangs test + ''; + buildPhase = '' + ./test + mdbook test + touch $out + ''; + dontInstall = true; + }; +in { + inherit cc lean4-mode buildLeanPackage llvmPackages; + lean = lean.stage1; + temci = (import temci {}).override { doCheck = false; }; + nix = nix-pinned; + nixpkgs = pkgs; + ciShell = writeShellScriptBin "ciShell" '' + set -o pipefail + export PATH=${nix-pinned}/bin:${moreutils}/bin:$PATH + # prefix lines with cumulative and individual execution time + "$@" |& ts -i "(%.S)]" | ts -s "[%M:%S" + ''; + mdbook = lean-mdbook; + inherit doc doc-test; +} // lean.stage1.Lean // lean.stage1 // lean