## 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.

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

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

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: May 10 2021 at 19:16 UTC