failed to start child process

Stream: general

[Scott Morrison]

I have a student who can't run leanpkg on Windows: leanpkg.bat new test says: "failed to start child process", and doesn't create a new directory.

[Scott Morrison]

Has anyone experienced this, and knows the fix?

[Scott Morrison]

I know nothing about Windows anymore.

[Johan Commelin]

Has anyone experienced this, and knows the fix?

The fix would obviously be to wipe Windows and install a proper OS.

[Minchao Wu]

@Scott Morrison one of my colleagues has experienced this. The simplest solution would be using Git Bash if Git is installed.

[Kevin Buzzard]

I've had several problems with git on Windows. There appears to be more than one canonical installation of git.

[Chris Hughes]

I always get that error if I use the windows command line instead of Msys.

[Kevin Buzzard]

The mantra I tell Windows users is msys2, git, lean binary, set msys2 path variable so it can see git and leanpkg, then follow instructions in reference manual

[Kevin Buzzard]

Oh -- and don't put lean in a directory whose full name has a space in

[Scott Morrison]

We found yet another solution: activate the "Linux Subsystem for Windows", install the "Ubuntu" app, and use elan there. It was incredibly painless and fast (15 minutes?)

[Mario Carneiro]

really? I've never had much success with WSL

[Olli]

Any ideas what the "failed to start child process" might be due to? I am on Windows 10 and I get it when trying to use leanpkg for basically anything. I see that it originates in the C++ code base of Lean itself.

I saw some mentions of this issue in the mailing list, where it was mentioned that it occasionally happens, but for me I'm unable to do almost anything with leanpkg, which means I can't use mathlib as far as I can tell.

I might give using WSL a try, although I'm afraid that configuring VSCode might become a pain in that case.

[Olli]

I suppose another thing I could try is compiling Lean from source and hoping that that fixes the issue.