Zulip Chat Archive

Stream: general

Topic: Missing leanpkg

Jason Rute (Apr 29 2020 at 01:16):

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 (Apr 29 2020 at 01:18):

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

Jason Rute (Apr 29 2020 at 01:19):

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 (Apr 29 2020 at 01:19):

Or am I just doing something dumb?

Jason Rute (Apr 29 2020 at 02:49):

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 (Apr 29 2020 at 03:10):

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 (Apr 29 2020 at 03:15):

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

Kevin Buzzard (Apr 29 2020 at 06:50):

Good to know

Sebastian Ullrich (Apr 29 2020 at 08:19):

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

Sebastian Ullrich (Apr 29 2020 at 08:23):

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

Patrick Massot (Apr 29 2020 at 08:41):

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

Sebastian Ullrich (Apr 29 2020 at 08:50):

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

Last updated: Dec 20 2023 at 11:08 UTC