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 Dockerfile
:
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
Is alectryon
in the PATH
?
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 Dockerfile
this:
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 PATH
by ~/.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 /bin/bash
).
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.
@Paolo Giarrusso that was exactly the issue, thanks very much!
Théo Zimmermann said:
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.
You're right, but I didn't immediately realize SerAPI was part of the image I was using, and then I already had everything set up, so I thought I might as well go ahead with only alectryon and finmap. It feels wasteful to install dependencies in CI, even if it takes negligible resources :sweat_smile:
Ana de Almeida Borges has marked this topic as resolved.
Last updated: Dec 07 2023 at 17:01 UTC