Installation on fresh Ubuntu

Stream: general

[Riccardo Brasca]

I am trying to install everything on a fresh machine with Ubuntu 23.10, following the official instructions.

It seems something doesn't work and VsCode is not installed

wget -q https://raw.githubusercontent.com/leanprover-community/mathlib4/master/scripts/install_debian.sh && bash install_debian.sh ; rm -f install_debian.sh && source ~/.profile
+ sudo apt install -y git curl
[sudo] password for riccardo:
Reading package lists... Done
Building dependency tree... Done
Reading state information... Done
The following additional packages will be installed:
  git-man liberror-perl
Suggested packages:
  git-daemon-run | git-daemon-sysvinit git-doc git-email git-gui gitk gitweb git-cvs git-mediawiki git-svn
The following NEW packages will be installed:
  curl git git-man liberror-perl
0 upgraded, 4 newly installed, 0 to remove and 8 not upgraded.
Need to get 4,910 kB of archives.
After this operation, 24.5 MB of additional disk space will be used.
Get:1 http://fr.archive.ubuntu.com/ubuntu mantic-updates/main amd64 curl amd64 8.2.1-1ubuntu3.2 [216 kB]
Get:2 http://fr.archive.ubuntu.com/ubuntu mantic/main amd64 liberror-perl all 0.17029-2 [25.6 kB]
Get:3 http://fr.archive.ubuntu.com/ubuntu mantic/main amd64 git-man all 1:2.40.1-1ubuntu1 [1,085 kB]
Get:4 http://fr.archive.ubuntu.com/ubuntu mantic/main amd64 git amd64 1:2.40.1-1ubuntu1 [3,583 kB]
Fetched 4,910 kB in 0s (25.6 MB/s)
Selecting previously unselected package curl.
(Reading database ... 142561 files and directories currently installed.)
Preparing to unpack .../curl_8.2.1-1ubuntu3.2_amd64.deb ...
Unpacking curl (8.2.1-1ubuntu3.2) ...
Selecting previously unselected package liberror-perl.
Preparing to unpack .../liberror-perl_0.17029-2_all.deb ...
Unpacking liberror-perl (0.17029-2) ...
Selecting previously unselected package git-man.
Preparing to unpack .../git-man_1%3a2.40.1-1ubuntu1_all.deb ...
Unpacking git-man (1:2.40.1-1ubuntu1) ...
Selecting previously unselected package git.
Preparing to unpack .../git_1%3a2.40.1-1ubuntu1_amd64.deb ...
Unpacking git (1:2.40.1-1ubuntu1) ...
Setting up liberror-perl (0.17029-2) ...
Setting up git-man (1:2.40.1-1ubuntu1) ...
Setting up curl (8.2.1-1ubuntu3.2) ...
Setting up git (1:2.40.1-1ubuntu1) ...
Processing triggers for man-db (2.11.2-3) ...
+ wget https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh
--2024-01-16 16:05:53--  https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh
Resolving raw.githubusercontent.com (raw.githubusercontent.com)... 185.199.110.133, 185.199.109.133, 185.199.111.133, ...
Connecting to raw.githubusercontent.com (raw.githubusercontent.com)|185.199.110.133|:443... connected.
HTTP request sent, awaiting response... 200 OK
Length: 10006 (9.8K) [text/plain]
Saving to: ‘elan-init.sh’

elan-init.sh                                  100%[================================================================================================>]   9.77K  --.-KB/s    in 0.001s

2024-01-16 16:05:53 (16.8 MB/s) - ‘elan-init.sh’ saved [10006/10006]

+ bash elan-init.sh -y
info: downloading installer
info: syncing channel updates for 'stable'
info: latest update on stable, lean version v4.4.0
info: downloading component 'lean'
182.6 MiB / 182.6 MiB (100 %)  89.0 MiB/s ETA:   0 s
info: installing component 'lean'
info: default toolchain set to 'stable'

  stable installed - Lean (version 4.4.0, commit ca7d6dadb9e1, Release)

+ rm elan-init.sh
++ which code
++ which codium
+ vsc=

Am I a missing something or there is actually a problem with the script?

Note that I am not asking how to finish the installation, just to check if the script is correct.

[Julian Berman]

I think the script is wrong.

[Julian Berman]

Specifically I think which at least in some shells will spit out its message to stdout and not stderr, so 2>/dev/null doesn't do anything, and vsc will be non-empty but the script is trying to check whether it exists.

[Julian Berman]

I personally avoid which at all costs (not to mention avoiding shell at all costs) but at worst it lies, and at best it can be confusing. But yeah that's I think the problem there.

[Julian Berman]

(On macOS by the way which behaves this way as well it seems, it outputs foo not found to stdout.)

[Julian Berman]

Maybe using /usr/bin/which (i.e. not the shell command) was intended or is a better idea, but probably some CI is also not a bad idea.

[Mario Carneiro]

have you tried which which? :laughing:

[Riccardo Brasca]

which whichwhich code does not return anything, as expected

[Riccardo Brasca]

it seems it doesn't enter the if

[Riccardo Brasca]

It does the same thing on a fresh debian installation

[Riccardo Brasca]

I don't know anything about shell scripts, but if I run by hand the line (erasing from the script)

vsc="$(which code1 2>/dev/null || which codium 2>/dev/null)"

and then I do bash install_debian.sh it works.

[Julian Berman]

Oh right, it's other shell nonsense.

[Julian Berman]

It's because vsc="$(which code 2>/dev/null || which codium 2>/dev/null)" has nonzero exit code, and set -e will stop the script there

[Julian Berman]

Presumably you tried it at an interactive shell where you didn't run set -e.

[Julian Berman]

You can put || true at the end there to fix it -- vsc="$(which code 2>/dev/null || which codium 2>/dev/null || true)"

[Riccardo Brasca]

Yep, this works

[Riccardo Brasca]

So what is the best solution? It seems pretty bad that literally the first thing a new user is supposed to run doesn't work as expected.

[Riccardo Brasca]

#9784

[Julian Berman]

Riccardo Brasca said:

So what is the best solution? It seems pretty bad that literally the first thing a new user is supposed to run doesn't work as expected.

the || true would be my recommendation for being a small change. Removing the set -e is "worse" as it makes it a lot easier to not exit when something fails and you'd expect things to "blow up" in some reasonable language -- shell is a disaster.