Missing leanpkg

Stream: general

[Jason Rute]

I'm trying to run lean on a clean cloud machine (AWS EC2 c4.large, amazon linux). I did:

sudo yum install python36 -y

wget -q https://raw.githubusercontent.com/leanprover-community/mathlib-tools/master/scripts/install_debian.sh && bash install_debian.sh ; rm -f install_debian.sh && source ~/.profile

leanproject new test_project

I get the error:

No such file or directory: 'leanpkg'

[Jason Rute]

I just did pip3 install mathlibtools to see if it helps. It doesn't.

[Jason Rute]

I think @Patrick Massot told me that leanproject still depends on leanpkg. I wonder if we stopped shipping leanpkg in that script by mistake.

[Jason Rute]

Or am I just doing something dumb?

[Jason Rute]

Ok, I think that leanpkg stuff was just a red herring. When I went to install elan directly, I got this error.

[ec2-user@ip-172-31-31-7 ~]$ curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh
info: downloading installer
/tmp/tmp.ALQTnW5hvr/elan-init: /lib64/libc.so.6: version `GLIBC_2.18' not found (required by /tmp/tmp.ALQTnW5hvr/elan-init)

[Jason Rute]

Ok, short story. I was using an old instance AWS snapshot with Amazon Linux 2017.09. I need to upgrade to 2018.03. (I can't figure out how to do this, but I think I can just start over from scratch with my snapshot. It's good to do some house cleaning.)

[Jason Rute]

I was able however to get this all working in a new EC2 instance with Amazon Linux.

[Kevin Buzzard]

Good to know

[Sebastian Ullrich]

There should really be a set -e in install_debian.sh

[Sebastian Ullrich]

By the way, what's up with this wget; bash; rm idiom instead of curl | bash?

[Patrick Massot]

I think it was because wget is here by default and curl needs installing

[Sebastian Ullrich]

I see. I think you can use wget -O - to pipe it as well.