Zulip Chat Archive

Stream: general

Topic: Get olean files without elan on Win10


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Chris Hughes (Oct 27 2018 at 12:22):

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

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 27 2018 at 12:26):

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

Wait, which usernames?

view this post on Zulip Kenny Lau (Oct 27 2018 at 12:28):

your username

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 27 2018 at 12:29):

your username

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

view this post on Zulip Kenny Lau (Oct 27 2018 at 12:29):

yes

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 27 2018 at 12:29):

Ok, that's not a problem, then.

view this post on Zulip 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: May 10 2021 at 19:16 UTC