max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: Nix: link with gold instead of lld

Browse source 
https://twitter.com/derKha/status/1419645259894640645
This commit is contained in:
Sebastian Ullrich 2021-07-29 15:20:12 +02:00
parent 45b599ef69
commit 0db80c6ea8
2 changed files with 12 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
nix/buildLeanPackage.nix
View file

@ -1,6 +1,6 @@
{ lean, lean-leanDeps ? lean, lean-final ? lean, leanc,
stdenv, lib, coreutils, gnused, writeShellScriptBin, bash, lean-emacs, lean-vscode, nix, substituteAll, symlinkJoin, linkFarmFromDrvs,
... }:
runCommand, ... }:
let lean-final' = lean-final; in
{ name, src, fullSrc ? src,
# Lean dependencies. Each entry should be an output of buildLeanPackage.
@ -15,7 +15,7 @@ with builtins; let
# "Init.Core" ~> "Init/Core"
modToPath = mod: replaceStrings ["."] ["/"] mod;
modToLean = mod: modToPath mod + ".lean";
mkDerivation = args@{ buildCommand, ... }: derivation (args // {
mkBareDerivation = args@{ buildCommand, ... }: derivation (args // {
inherit stdenv;
inherit (stdenv) system;
buildInputs = (args.buildInputs or []) ++ [ coreutils ];
@ -28,12 +28,12 @@ with builtins; let
${buildCommand}
'' ];
});
runCommand = name: args: buildCommand: mkDerivation (args // { inherit name buildCommand; });
runCommandLocal = name: args: buildCommand: runCommand name (args // {
runBareCommand = name: args: buildCommand: mkBareDerivation (args // { inherit name buildCommand; });
runBareCommandLocal = name: args: buildCommand: runBareCommand name (args // {
preferLocalBuild = true;
allowSubstitutes = false;
}) buildCommand;
depRoot = name: deps: mkDerivation {
depRoot = name: deps: mkBareDerivation {
name = "${name}-depRoot";
inherit deps;
depRoots = map (drv: drv.LEAN_PATH) deps;
@ -59,7 +59,7 @@ with builtins; let
lib.unique (lib.flatten (staticLibDeps ++ (map (dep: [dep.staticLib] ++ dep.staticLibDeps or []) (attrValues allExternalDeps))));
leanPluginFlags = lib.concatStringsSep " " (map (dep: "--plugin=${dep}/${dep.name}") pluginDeps);
fakeDepRoot = runCommandLocal "${name}-dep-root" {} ''
fakeDepRoot = runBareCommandLocal "${name}-dep-root" {} ''
mkdir $out
cd $out
mkdir ${lib.concatStringsSep " " ([name] ++ attrNames allExternalDeps)}
@ -69,7 +69,7 @@ with builtins; let
${lean-leanDeps}/bin/lean --deps --stdin | ${gnused}/bin/sed "s!$LEAN_PATH/!!;s!/!.!g;s!.olean!!"
'';
# build a file containing the module names of all immediate dependencies of `mod`
leanDeps = mod: mkDerivation {
leanDeps = mod: mkBareDerivation {
name ="${mod}-deps";
src = src + ("/" + modToLean mod);
buildInputs = [ print-lean-deps ];
@ -80,7 +80,7 @@ with builtins; let
allowSubstitutes = false;
};
# build module (.olean and .c) given derivations of all (transitive) dependencies
buildMod = mod: deps: mkDerivation rec {
buildMod = mod: deps: mkBareDerivation rec {
name = "${mod}";
LEAN_PATH = depRoot mod deps;
relpath = modToPath mod;
@ -100,7 +100,7 @@ with builtins; let
} // {
inherit deps;
};
compileMod = mod: drv: mkDerivation {
compileMod = mod: drv: mkBareDerivation {
name = "${mod}-cc";
buildInputs = [ leanc stdenv.cc ];
hardeningDisable = [ "all" ];

9
nix/packages.nix
View file

@ -6,11 +6,7 @@ let
'';
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;
};
cc = llvmPackages.clang;
extraConfig = ''
export CCACHE_DIR=/nix/var/cache/ccache
export CCACHE_UMASK=007
@ -29,8 +25,9 @@ let
# https://github.com/NixOS/nixpkgs/issues/119779
installPhase = builtins.replaceStrings ["use_response_file_by_default=1"] ["use_response_file_by_default=0"] old.installPhase;
});
stdenv = overrideCC llvmPackages.stdenv cc;
lean = callPackage (import ./bootstrap.nix) (args // {
stdenv = overrideCC llvmPackages.stdenv cc;
stdenv = if stdenv.isLinux then useGoldLinker stdenv else stdenv;
inherit buildLeanPackage;
});
makeOverridableLeanPackage = f: