As far as I can tell there is no docker image with Alectryon yet (right?). I'm trying to create one, but something is going wrong. When I build it locally it seems to work fine (
alectryon --version prints the expected version), but when I use it in CI, it complains that the
alectryon command can't be found. I have no clue how to debug this, does anyone with more experience have some suggestions? The
FROM mathcomp/mathcomp:1.13.0-coq-8.15 RUN sudo apt-get update && sudo apt-get install -y python3-pip RUN python3 -m pip install alectryon RUN opam update && opam pin add coq-mathcomp-finmap 1.5.1 --yes
alectryon in the
When I build it locally it seems to work fine (alectryon --version prints the expected version)
Locally, but with or without the image? Running the same commands in the same image is meant to give the same results — OTOH, installing Alectryon outside the image might need different instructions.
In particular, you can run
docker run -it anaagvb/alectryon:coq8.15-mathcomp1.13 locally. Or rather, anybody can, so I'm taking a look
Okay, Unix strikes again: the nested environment gets different
PATH values depending on how exactly it is started, so I guess Gitlab's using a different command:
$ docker run -it anaagvb/alectryon:coq8.15-mathcomp1.13 coq@7e1254587dca:~$ which alectryon /home/coq/.local/bin/alectryon coq@7e1254587dca:~$ echo $PATH /home/coq/.opam/4.07.1+flambda/bin:/home/coq/.local/bin:/home/coq/bin:/usr/local/bin:/usr/bin:/bin:/usr/local/games:/usr/games
$ docker run -it anaagvb/alectryon:coq8.15-mathcomp1.13 /bin/bash WARNING: The requested image's platform (linux/amd64) does not match the detected host platform (linux/arm64/v8) and no specific platform was requested coq@332afb7f5ee9:~$ echo $PATH /home/coq/.opam/4.07.1+flambda/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin coq@332afb7f5ee9:~$ which alectryon coq@332afb7f5ee9:~$
$ docker run -it anaagvb/alectryon:coq8.15-mathcomp1.13 /bin/bash -l coq@699df2139528:~$ which alectryon /home/coq/.local/bin/alectryon
If this is the problem you're hitting, the quickfix is to add
~/.local/bin to the
PATH anyway, either in the CI script, or in the container by appending to the
ENV PATH "/home/coq/.local/bin:$PATH"
(Strictly speaking, this is not perfect but I doubt it's a concrete problem: This might duplicate the PATH entry sometimes).
I haven't summarized why
.local/bin is there only sometimes — to say a bit more, that setting is normally added to the
~/.profile, which is only loaded by
bash when it is started as a login shell (e.g. via
/bin/bash -l), but not as a normal shell (e.g. via
I'll stop this wall of text now :sweat_smile: , please let me know any follow-up
FWIW, the idea was that by including SerAPI in the Docker-Coq images, it would make it easy to use with Alectryon, since Alectryon is quick to install with pip.
Last updated: Aug 19 2022 at 19:03 UTC