feat: Nix: sanitized build
This commit is contained in:
Sebastian Ullrich
parent
2ffd929227
commit
03acc5ea1f
4 changed files with 101 additions and 92 deletions
95
flake.nix
95
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;
|
||||
|
|
|
|||
|
|
@ -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 = ''
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
89
nix/packages.nix
Normal file
89
nix/packages.nix
Normal file
|
|
@ -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
|
||||
Loading…
Add table
Reference in a new issue