You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
lake build is failing to build in Windows, in a project using mathlib. As the Zulip Topic details, this might be an issue with ERROR_INVALID_PARAMETER, as lake is calling CreateProcess with a 56856-character string as the lpCommandLine argument, and that's invalid because the maximum length for that parameter is 32767 characters. @bustercopley was able to produce an exe by writing the arguments to a file args.txt and invoking leanc as leanc.exe @args.txt, what lake should be doing automatically.
Prerequisites
Please put an X between the brackets as you perform the following steps:
https://github.com/leanprover/lean4/issues
Avoid dependencies to Mathlib or Batteries.
https://live.lean-lang.org/#project=lean-nightly
(You can also use the settings there to switch to “Lean nightly”)
Description
lake build
is failing to build in Windows, in a project using mathlib. As the Zulip Topic details, this might be an issue withERROR_INVALID_PARAMETER
, aslake
is callingCreateProcess
with a 56856-character string as thelpCommandLine
argument, and that's invalid because the maximum length for that parameter is 32767 characters. @bustercopley was able to produce an exe by writing the arguments to a fileargs.txt
and invoking leanc asleanc.exe @args.txt
, what lake should be doing automatically.Context
The error was discussed about on this topic: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/could.20not.20rename.20packages.20directory
Steps to Reproduce
Expected behavior: The build completes successfully, albeit with sorry warnings
Actual behavior: Build fails with error
Versions
Lean.versionString: "4.8.0-rc1"
OS version: Windows 10 Home Single Language 22H2
Impact
General compilation in Windows with Mathlib
The text was updated successfully, but these errors were encountered: