Ana de Almeida Borges (May 31 2022 at 00:31): Ana de Almeida Borges (May 31 2022 at 00:31):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.
Paolo Giarrusso (May 31 2022 at 01:06):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
Paolo Giarrusso (May 31 2022 at 01:12):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).
Paolo Giarrusso (May 31 2022 at 01:18):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).
Paolo Giarrusso (May 31 2022 at 01:19):I'll stop this wall of text now :sweat_smile: , please let me know any follow-up
Théo Zimmermann (May 31 2022 at 07:05):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.
Ana de Almeida Borges (May 31 2022 at 09:32):@Paolo Giarrusso that was exactly the issue, thanks very much!
Ana de Almeida Borges (May 31 2022 at 09:35):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:
Notification Bot (May 31 2022 at 09:37):Ana de Almeida Borges has marked this topic as resolved.
Last updated: Jun 01 2023 at 12:01 UTC