elan install

Stream: new members

[Ethan]

Hi, thought I'd follow a talk by Scott Morrison in vscode [1] on windows. I get an error in the initial few minutes with import data.nat.prime giving an error file 'data\nat\prime' not found in the LEAN_PATH. Googling leads me to think maybe I need to install mathlib [2]. I get stuck though installing elan. Running curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh gives me an error

curl: (22) The requested URL returned error: 404 Not Found
elan: command failed: curl -sSfL https://github.com/Kha/elan/releases/download/v0.7.5/elan-i686-pc-windows-msvc.zip -o /tmp/tmp.wzaAdEylcT/elan-init.zip

Am I on the right track? Is there another way to install mathlib (or elan)?

1. https://www.youtube.com/watch?v=2FQOakOfP00&list=PL7i7VGTKzi-QFrAEojtwxnX5xTccOPXbM
2. https://github.com/leanprover-community/mathlib/blob/master/docs/install/windows.md

[Bryan Gin-ge Chen]

Yes, you need to install mathlib (following these instructions) for import data.nat.prime to work. I'm not sure why the elan install script is requesting a non-existent file though, it should be something from this list: https://github.com/Kha/elan/releases/ What shell are you using? If you're not using the Git for Windows shell, maybe try that?

[Reid Barton]

it looks like there is no binary release there for 32-bit windows (i686-pc-windows), only 64-bit windows (x86_64-pc-windows)

[Ethan]

Hi Bryan and Reid, After installing the elan release and instructions, I'm following https://github.com/leanprover-community/mathlib/blob/master/docs/install/project.md to create a project with a mathlib dependency. Running leanpkg.exe new testproj fails with failed to start child process. At various points in trying to get this to work I've used cmd, cygwin, wsl bash, powershell, and git for windows bash.

[Kevin Buzzard]

Did you try searching for that error on this site? Not sure if it will help. Does dropping the .exe change anything?

[Ethan]

I think I have it (though I'm unsure if I could do it again), I'm able to run leanpkg.exe in a cygwin shell to create a project and add the mathlib dependency. I had to run updath-mathlib from a wsl bash shell (the shell I used to run remote-install-update-mathlib.sh). vscode works with the test example (#check topological_space). Thank you for all the help!

[Bryan Gin-ge Chen]

Glad you got things working, but you shouldn't have needed to use cygwin or WSL. Out of curiosity, where did you see that suggested? Now I guess you're running the Linux version of Lean in Windows. Are you indeed on a 32-bit Windows system?

I think the "failed to start child process" error tends to occur when you don't use Git for Windows bash. If you're on a 64-bit system, could you try and reconstruct the steps you took before you got that error?

[Ethan]

Going over it again, the problem was running the 32-bit shells (the prompt shows MINGW32 instead of MINGW64). In 64 bit git for windows bash I can run elan-init.sh and leanpkg. wsl was just the the easiest way to install python. It's not clear to me if that was a requirement for mathlib but it was listed under the "Installing mathlib supporting tools" section

[Bryan Gin-ge Chen]

Ah, OK. That makes more sense. I think there was some talk at the Lean Together 2020 meeting about figuring out a better installation path for Windows users, but I'm not sure what came out of it.