feat: Nix: add nativeSharedLibs option
* feat: Add nativeSharedLibs option Use LD_PRELOAD with staticLibDeps Add a verbose flag when debug is true Use shared libs instead feat: Add recursive nativeSharedLibs Repair printPaths Remove -v flag from lean call feat: Use new load-dynlib option Remove LD_PRELOAD fix: Add allNativeSharedLibs to allLinkFlags Trying to fix native linking feat: Automatic link flags of nativeSharedLibs fix: Add gmp to sharedLib buildInputs * fix: Wrap executable files in a linker group This is a bit slower but ensures that cycles or bad ordering of the static lib dependencies is resolved. * Convert allExternalDeps to a list Breaking change if you depend on allExternalDeps being a attrset
This commit is contained in:
Anders Christiansen Sørby
GitHub
parent
a9317760e7
commit
cfe924e53e
1 changed files with 41 additions and 21 deletions
|
|
@ -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, ... }:
|
||||
runCommand, gmp, ... }:
|
||||
let lean-final' = lean-final; in
|
||||
lib.makeOverridable (
|
||||
{ name, src, fullSrc ? src,
|
||||
|
|
@ -8,6 +8,12 @@ lib.makeOverridable (
|
|||
deps ? [ lean.Lean lean.Leanpkg ],
|
||||
# Static library dependencies. Each derivation `static` should contain a static library in the directory `${static}`.
|
||||
staticLibDeps ? [],
|
||||
# Whether to wrap static library inputs in a -Wl,--start-group [...] -Wl,--end-group to ensure dependencies are resolved.
|
||||
groupStaticLibs ? false,
|
||||
# Shared library dependencies included at interpretation with --load-dynlib and linked to. Each derivation `shared` should contain a
|
||||
# shared library at the path `${shared}/${shared.libName or shared.name}` and a name to link to like `-l${shared.linkName or shared.name}`.
|
||||
# These libs are also linked to in packages that depend on this one.
|
||||
nativeSharedLibs ? [],
|
||||
# Lean plugin dependencies. Each derivation `plugin` should contain a plugin library at path `${plugin}/${plugin.name}`.
|
||||
pluginDeps ? [],
|
||||
debug ? false, leanFlags ? [], leancFlags ? [], linkFlags ? [], executableName ? lib.toLower name,
|
||||
|
|
@ -53,17 +59,24 @@ with builtins; let
|
|||
srcRoot = src;
|
||||
|
||||
# A flattened list of Lean-module dependencies (`deps`)
|
||||
allExternalDeps = lib.foldr (dep: allExternalDeps: allExternalDeps // { ${dep.name} = dep; } // dep.allExternalDeps) {} deps;
|
||||
allExternalDeps = lib.unique (lib.foldr (dep: allExternalDeps: allExternalDeps ++ [ dep ] ++ dep.allExternalDeps) [] deps);
|
||||
allNativeSharedLibs =
|
||||
lib.unique (lib.flatten (nativeSharedLibs ++ (map (dep: dep.allNativeSharedLibs or []) allExternalDeps)));
|
||||
|
||||
# A flattened list of all static library dependencies: this and every dep module's explicitly provided `staticLibDeps`,
|
||||
# plus every dep module itself: `dep.staticLib`
|
||||
allStaticLibDeps =
|
||||
lib.unique (lib.flatten (staticLibDeps ++ (map (dep: [dep.staticLib] ++ dep.staticLibDeps or []) (attrValues allExternalDeps))));
|
||||
leanPluginFlags = lib.concatStringsSep " " (map (dep: "--plugin=${dep}/${dep.name}") pluginDeps);
|
||||
lib.unique (lib.flatten (staticLibDeps ++ (map (dep: [dep.staticLib] ++ dep.staticLibDeps or []) allExternalDeps)));
|
||||
|
||||
pathOfSharedLib = dep: dep.libPath or "${dep}/${dep.libName or dep.name}";
|
||||
|
||||
leanPluginFlags = lib.concatStringsSep " " (map (dep: "--plugin=${pathOfSharedLib dep}") pluginDeps);
|
||||
leanLoadDynlibFlags = lib.concatStringsSep " " (map (dep: "--load-dynlib=${pathOfSharedLib dep}") allNativeSharedLibs);
|
||||
|
||||
fakeDepRoot = runBareCommandLocal "${name}-dep-root" {} ''
|
||||
mkdir $out
|
||||
cd $out
|
||||
mkdir ${lib.concatStringsSep " " ([name] ++ attrNames allExternalDeps)}
|
||||
mkdir ${lib.concatStringsSep " " ([name] ++ (map (d: d.name) allExternalDeps))}
|
||||
'';
|
||||
print-lean-deps = writeShellScriptBin "print-lean-deps" ''
|
||||
export LEAN_PATH=${fakeDepRoot}
|
||||
|
|
@ -91,12 +104,11 @@ with builtins; let
|
|||
outputs = [ "out" "c" ];
|
||||
oleanPath = relpath + ".olean";
|
||||
cPath = relpath + ".c";
|
||||
inherit leanFlags;
|
||||
inherit leanPluginFlags;
|
||||
inherit leanFlags leanPluginFlags leanLoadDynlibFlags;
|
||||
buildCommand = ''
|
||||
mkdir -p $(dirname $relpath) $out/$(dirname $relpath) $c/$(dirname $relpath)
|
||||
cp $src $leanPath
|
||||
lean -o $out/$oleanPath -c $c/$cPath $leanPath $leanFlags $leanPluginFlags
|
||||
lean -o $out/$oleanPath -c $c/$cPath $leanPath $leanFlags $leanPluginFlags $leanLoadDynlibFlags
|
||||
'';
|
||||
} // {
|
||||
inherit deps;
|
||||
|
|
@ -112,11 +124,11 @@ with builtins; let
|
|||
# make local "copy" so `drv`'s Nix store path doesn't end up in ccache's hash
|
||||
ln -s ${drv.c}/${drv.cPath} src.c
|
||||
# on the other hand, a debug build is pretty fast anyway, so preserve the path for gdb
|
||||
leanc -c -o $out/$oPath $leancFlags -fPIC ${if debug then "${drv.c}/${drv.cPath} -g " else "src.c -O3 -DNDEBUG"}
|
||||
leanc -c -o $out/$oPath $leancFlags -fPIC ${if debug then "${drv.c}/${drv.cPath} -g -v" else "src.c -O3 -DNDEBUG"}
|
||||
'';
|
||||
};
|
||||
singleton = name: value: listToAttrs [ { inherit name value; } ];
|
||||
externalModMap = lib.foldr (dep: depMap: depMap // dep.mods) {} (attrValues allExternalDeps);
|
||||
externalModMap = lib.foldr (dep: depMap: depMap // dep.mods) {} allExternalDeps;
|
||||
# Recursively build `mod` and its dependencies. `modMap` maps module names to
|
||||
# `{ deps, drv }` pairs of a derivation and its transitive dependencies (as a nested
|
||||
# mapping from module names to derivations). It is passed linearly through the
|
||||
|
|
@ -133,38 +145,46 @@ with builtins; let
|
|||
PATH=${lean}/bin:$PATH ${lean-vscode}/bin/code "$@"
|
||||
'';
|
||||
printPaths = deps: writeShellScriptBin "print-paths" ''
|
||||
echo '${toJSON { oleanPath = [(depRoot "print-paths" deps)]; srcPath = ["."] ++ map (dep: dep.src) (attrValues allExternalDeps); }}'
|
||||
echo '${toJSON { oleanPath = [(depRoot "print-paths" deps)]; srcPath = ["."] ++ map (dep: dep.src) allExternalDeps; }}'
|
||||
'';
|
||||
makePrintPathsFor = deps: mods: printPaths deps // mapAttrs (_: mod: makePrintPathsFor (deps ++ [mod]) mods) mods;
|
||||
mods = buildModAndDeps name {};
|
||||
in rec {
|
||||
inherit name lean deps staticLibDeps allExternalDeps print-lean-deps src mods;
|
||||
modRoot = depRoot name [ mods.${name} ];
|
||||
cTree = symlinkJoin { name = "${name}-cTree"; paths = map (mod: mod.c) (attrValues mods); };
|
||||
allLinkFlags = lib.foldr (shared: acc: acc ++ [ "-L${shared}" "-l${shared.linkName or shared.name}" ]) linkFlags allNativeSharedLibs;
|
||||
|
||||
objects = mapAttrs compileMod mods;
|
||||
oTree = symlinkJoin { name = "${name}-oTree"; paths = (attrValues objects); };
|
||||
staticLib = runCommand "${name}-lib" { buildInputs = [ stdenv.cc.bintools.bintools ]; } ''
|
||||
mkdir -p $out
|
||||
ar Trcs $out/lib${name}.a ${lib.concatStringsSep " " (map (drv: "${drv}/${drv.oPath}") (attrValues objects))};
|
||||
'';
|
||||
sharedLib = runCommand "${name}.so" { buildInputs = [ stdenv.cc ]; } ''
|
||||
|
||||
# Static lib inputs
|
||||
staticLibLinkWrapper = libs: if groupStaticLibs
|
||||
then "-Wl,--start-group ${libs} -Wl,--end-group"
|
||||
else "${libs}";
|
||||
staticLibArguments = staticLibLinkWrapper ("${staticLib}/* ${lib.concatStringsSep " " (map (d: "${d}/*.a") allStaticLibDeps)}");
|
||||
in rec {
|
||||
inherit name lean deps staticLibDeps allNativeSharedLibs allLinkFlags allExternalDeps print-lean-deps src mods objects staticLib;
|
||||
modRoot = depRoot name [ mods.${name} ];
|
||||
cTree = symlinkJoin { name = "${name}-cTree"; paths = map (mod: mod.c) (attrValues mods); };
|
||||
oTree = symlinkJoin { name = "${name}-oTree"; paths = (attrValues objects); };
|
||||
sharedLib = runCommand "${name}.so" { buildInputs = [ stdenv.cc gmp ]; } ''
|
||||
mkdir -p $out/lib
|
||||
${leanc}/bin/leanc -fPIC -shared \
|
||||
-Wl,--whole-archive ${staticLib}/* -Wl,--no-whole-archive\
|
||||
${lib.concatStringsSep " " (map (d: "${d}/*.a") allStaticLibDeps)} \
|
||||
${staticLibArguments} \
|
||||
-o $out/${name}.so
|
||||
'';
|
||||
executable = runCommand executableName { buildInputs = [ stdenv.cc leanc ]; } ''
|
||||
mkdir -p $out/bin
|
||||
leanc ${staticLib}/* ${lib.concatStringsSep " " (map (d: "${d}/*.a") allStaticLibDeps)} \
|
||||
leanc ${staticLibArguments} \
|
||||
-o $out/bin/${executableName} \
|
||||
${lib.concatStringsSep " " linkFlags}
|
||||
${lib.concatStringsSep " " allLinkFlags}
|
||||
'' // {
|
||||
withSharedStdlib = runCommand executableName { buildInputs = [ stdenv.cc leanc ]; } ''
|
||||
mkdir -p $out/bin
|
||||
leanc ${staticLib}/* -lleanshared \
|
||||
-o $out/bin/${executableName} \
|
||||
${lib.concatStringsSep " " linkFlags}
|
||||
${lib.concatStringsSep " " allLinkFlags}
|
||||
'';
|
||||
};
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue