Zulip Chat Archive

Stream: maths

Topic: cache-olean instructions


view this post on Zulip Chris Hughes (Jul 10 2019 at 12:33):

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

view this post on Zulip Simon Hudon (Jul 10 2019 at 15:14):

You mean this bit:

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

view this post on Zulip Simon Hudon (Jul 10 2019 at 15:14):

?

view this post on Zulip Chris Hughes (Jul 10 2019 at 15:15):

Yes.

view this post on Zulip Simon Hudon (Jul 10 2019 at 15:18):

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

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

view this post on Zulip Simon Hudon (Jul 10 2019 at 18:04):

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

view this post on Zulip Chris Hughes (Jul 10 2019 at 18:40):

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

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

view this post on Zulip Chris Hughes (Jul 10 2019 at 19:36):

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

view this post on Zulip Keeley Hoek (Jul 11 2019 at 07:08):

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

view this post on Zulip Keeley Hoek (Jul 11 2019 at 10:52):

I guess it's because curl isn't GPL

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

view this post on Zulip 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: May 06 2021 at 17:38 UTC