Zulip Chat Archive

Stream: maths

Topic: cache-olean instructions

Chris Hughes (Jul 10 2019 at 12:33):

#1205 @Simon Hudon The instructions are out of date.

Simon Hudon (Jul 10 2019 at 15:14):

You mean this bit: 

$ scripts/setup-dev-scripts.sh
$ source ~/.profile
$ setup-lean-git-hooks

Simon Hudon (Jul 10 2019 at 15:14):

?

Chris Hughes (Jul 10 2019 at 15:15):

Yes.

Simon Hudon (Jul 10 2019 at 15:18):

Didn't there use to be documentation for installing it with curl?

Simon Hudon (Jul 10 2019 at 15:19):

Ok, we can replace the first line with: 

curl https://raw.githubusercontent.com/leanprover-community/mathlib-tools/master/scripts/remote-install-update-mathlib.sh -sSf | bash

Simon Hudon (Jul 10 2019 at 18:04):

@Chris Hughes I just made the change. Can you check that you're happy with it?

Chris Hughes (Jul 10 2019 at 18:40):

I don't get any errors, but it doesn't download binaries when I checkout.

Chris Hughes (Jul 10 2019 at 18:42):

Sorry, I get this error
hint: The '.git/hooks/post-checkout' hook was ignored because it's not set as executable.

Chris Hughes (Jul 10 2019 at 19:36):

I did chmod +x .git/hooks/post-checkout and now it works.

Keeley Hoek (Jul 11 2019 at 07:08):

By the way, curl isn't installed on a modern default ubuntu installation. wget is though

Keeley Hoek (Jul 11 2019 at 10:52):

I guess it's because curl isn't GPL

Keeley Hoek (Jul 11 2019 at 11:00):

wget -qnv -O- https://raw.githubusercontent.com/leanprover-community/mathlib-tools/master/scripts/remote-install-update-mathlib.sh | bash

Floris van Doorn (Jul 11 2019 at 12:29):

Note: On Windows, it's the other way around for git bash: it does have curl, but not wget.

Last updated: Dec 20 2023 at 11:08 UTC