Zulip Chat Archive

Stream: general

Topic: Get olean files without elan on Win10

Abhimanyu Pallavi Sudhir (Oct 27 2018 at 11:15):

I'd like to download updates to mathlib manually from github, then produce the olean files. How can I do this? I saw these instructions, but apparently they aren't compatible with VS2018.

Kevin Buzzard (Oct 27 2018 at 12:06):

I think that elan is supposed to do all of this for you. But if you choose not to use it for some reason, then you can use leanpkg to build the .olean files. Maybe this old page https://xenaproject.wordpress.com/2017/12/02/how-to-install-mathlib-and-keep-it-up-to-date/ helps you? But I think that users are now encouraged to use elan

Chris Hughes (Oct 27 2018 at 12:22):

elan still doesn't work with spaces in user names.

Abhimanyu Pallavi Sudhir (Oct 27 2018 at 12:26):

elan still doesn't work with spaces in user names.

Wait, which usernames?

Kenny Lau (Oct 27 2018 at 12:28):

your username

Abhimanyu Pallavi Sudhir (Oct 27 2018 at 12:29):

your username

Yeah, I mean -- the Windows username? For file paths and stuff?

Kenny Lau (Oct 27 2018 at 12:29):

yes

Abhimanyu Pallavi Sudhir (Oct 27 2018 at 12:29):

Ok, that's not a problem, then.

Kevin Buzzard (Oct 27 2018 at 12:40):

Yes, I think the issue is exactly with file paths. What's even more frustrating is that apparently the problem has been fixed, but the PR has not yet been accepted (and might never be, I guess, until Lean 4 comes out next year)

Last updated: Dec 20 2023 at 11:08 UTC