Skip to content

Commit

Permalink
fix: avoid "Argument list is too large" on building via nix.
Browse files Browse the repository at this point in the history
The buildLeanPackage uses environment variable to store a list of libraries,
then passes that variable to the lean as CLI arguments.
According to this (https://stackoverflow.com/a/28865503),
CLI arguments and environment variables share same space,
therefore there is an error "Argument list is too large" when building a package with too many
components.
(for example - mathlib4)

This change makes buildLeanPackage to use a file instead of environment variable to store a list of
libraries.
  • Loading branch information
zerox committed Oct 22, 2023
1 parent a832f39 commit 5bacd9f
Showing 1 changed file with 9 additions and 1 deletion.
10 changes: 9 additions & 1 deletion nix/buildLeanPackage.nix
Original file line number Diff line number Diff line change
Expand Up @@ -155,11 +155,19 @@ with builtins; let
cPath = relpath + ".c";
inherit leanFlags leanPluginFlags;
leanLoadDynlibFlags = map (p: "--load-dynlib=${pathOfSharedLib p}") (loadDynlibsOfDeps deps);
passAsFile = [
# When building a package with too many dependencies,
# this variable become huge, which cause "Argument list is too large" error,
# so it should be passed as a file to avoid such errors.
"leanLoadDynlibFlags"
];
buildCommand = ''
# Increase stack limit to avoid "Argument list is too large" error.
ulimit -s unlimited
dir=$(dirname $relpath)
mkdir -p $dir $out/$dir $ilean/$dir $c/$dir
if [ -d $src ]; then cp -r $src/. .; else cp $src $leanPath; fi
lean -o $out/$oleanPath -i $ilean/$ileanPath -c $c/$cPath $leanPath $leanFlags $leanPluginFlags $leanLoadDynlibFlags
lean -o $out/$oleanPath -i $ilean/$ileanPath -c $c/$cPath $leanPath $leanFlags $leanPluginFlags $(cat $leanLoadDynlibFlagsPath)
'';
}) // {
inherit deps;
Expand Down

0 comments on commit 5bacd9f

Please sign in to comment.