✔ Docker image with Alectryon · Miscellaneous

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

Paolo Giarrusso (May 31 2022 at 01:05):

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

Paolo Giarrusso (May 31 2022 at 01:16):

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):

Ana de Almeida Borges (May 31 2022 at 09:35):

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:

Stream: Miscellaneous

Topic: ✔ Docker image with Alectryon

Ana de Almeida Borges (May 31 2022 at 00:31):