Zulip Chat Archive

Stream: new members

Topic: elan install


view this post on Zulip Ethan (Jan 21 2020 at 01:26):

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

view this post on Zulip Bryan Gin-ge Chen (Jan 21 2020 at 01:35):

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?

view this post on Zulip Reid Barton (Jan 21 2020 at 01:49):

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

view this post on Zulip Ethan (Jan 21 2020 at 02:24):

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.

view this post on Zulip Kevin Buzzard (Jan 21 2020 at 02:35):

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

view this post on Zulip Ethan (Jan 21 2020 at 02:47):

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!

view this post on Zulip Bryan Gin-ge Chen (Jan 21 2020 at 02:52):

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?

view this post on Zulip Ethan (Jan 21 2020 at 03:09):

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

view this post on Zulip Bryan Gin-ge Chen (Jan 21 2020 at 03:19):

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.


Last updated: May 11 2021 at 23:11 UTC