opamでmathcompをインストールした - ::Eldesh a b = LEFT a

最近 coqtokyo 第7回Ssreflect勉強会に参加しています。
隔週で火曜日にやっているので是非。

もうすぐ第五回講義資料(ssrcoq5.pdf)に到達しますが、ここでようやく mathcomp の話が出てきます。
さっそく opam で mathcomp をインストールしようとしたところ、以下のようなエラーが出ました。

eldesh@hostname:~/work/garrigue.git$ opam install coq-mathcomp-ssreflect
The following actions will be performed:
  ∗ install coq-mathcomp-ssreflect 1.12.0

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
⬇ retrieved coq-mathcomp-ssreflect.1.12.0  (cached)
[ERROR] The compilation of coq-mathcomp-ssreflect.1.12.0 failed at "make -C mathcomp/ssreflect -j 3".

#=== ERROR while compiling coq-mathcomp-ssreflect.1.12.0 ======================#
# context     2.1.0 | linux/x86_64 | ocaml-base-compiler.4.05.0 | https://coq.inria.fr/opam/released#2021-10-15 21:00
# path        ~/.opam/4.05.0/.opam-switch/build/coq-mathcomp-ssreflect.1.12.0
# command     ~/.opam/opam-init/hooks/sandbox.sh build make -C mathcomp/ssreflect -j 3
# exit-code   2
# env-file    ~/.opam/log/coq-mathcomp-ssreflect-122950-b76a3b.env
# output-file ~/.opam/log/coq-mathcomp-ssreflect-122950-b76a3b.out
### output ###
# make: Entering directory '/home/eldesh/.opam/4.05.0/.opam-switch/build/coq-mathcomp-ssreflect.1.12.0/mathcomp/ssreflect'
# /bin/sh: 1: /home/eldesh/lcl/bincoqtop: not found
# /bin/sh: 1: /home/eldesh/lcl/bincoqtop: not found
# /home/eldesh/lcl/bincoq_makefile  -f Make -o Makefile.coq
# make: /home/eldesh/lcl/bincoq_makefile: Command not found
# ../Makefile.common:55: recipe for target 'Makefile.coq' failed
# make: *** [Makefile.coq] Error 127
# make: *** Waiting for unfinished jobs....
# make: Leaving directory '/home/eldesh/.opam/4.05.0/.opam-switch/build/coq-mathcomp-ssreflect.1.12.0/mathcomp/ssreflect'



<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
┌─ The following actions failed
│ λ build coq-mathcomp-ssreflect 1.12.0
└─
╶─ No changes have been performed

ここがよく解りませんね🤔

# /bin/sh: 1: /home/eldesh/lcl/bincoqtop: not found

PATH も正常に見えます。

eldesh@hostname:~/work/garrigue.git$ which coqc
/home/eldesh/.opam/4.05.0/bin/coqc
eldesh@hostname:~/work/garrigue.git$ echo $PATH
/home/eldesh/.opam/4.05.0/bin:/home/eldesh/.cargo/bin:/home/eldesh/.local/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/usr/local/games

実は COQBIN が犯人で、以下のようになっていました。