Zulip Chat Archive

Stream: general

Topic: slashes in leanpkg.path

Kevin Buzzard (Jul 06 2018 at 16:54):

What does leanpkg.path look like on windows? I have about 20 minutes to get mathlib up and running on a win7 machine with no admin access and hence no git (apparently!). Are they / or \, and one or two?

Kevin Buzzard (Jul 06 2018 at 16:54):

I have lean and mathlib and VS code

Kevin Buzzard (Jul 06 2018 at 16:55):

I have no msys2 and no command line

Kevin Buzzard (Jul 06 2018 at 16:55):

I have notepad :-)

Andrew Ashworth (Jul 06 2018 at 16:56):

builtin_path
path _target/deps/mathlib/.
path ./src

Kevin Buzzard (Jul 06 2018 at 16:56):

thanks

Kevin Buzzard (Jul 06 2018 at 16:57):

works!

Kevin Buzzard (Jul 06 2018 at 16:57):

hmm

Kevin Buzzard (Jul 06 2018 at 16:57):

now need to make .olean files

Kevin Buzzard (Jul 06 2018 at 16:58):

with no command line :-/

Kenny Lau (Jul 06 2018 at 16:58):

how about just use the online version

Chris Hughes (Jul 06 2018 at 17:03):

download someone elses oleans?

Kenny Lau (Jul 06 2018 at 17:03):

where from?

Chris Hughes (Jul 06 2018 at 17:03):

I could upload mine.

Chris Hughes (Jul 06 2018 at 17:05):

Or Kevin could upload his.

Kevin Buzzard (Jul 06 2018 at 17:05):

I have some here for unix :-)

Chris Hughes (Jul 06 2018 at 17:05):

I don't know if Windows oleans are any different

Last updated: Dec 20 2023 at 11:08 UTC