Stream: coq-community devs & users

Topic: ✔ docker image _with_ Coq

view this post on Zulip Beta Ziliani (Sep 14 2021 at 01:23):

Unless I'm missing something, the docker images at coqorg allows you to build or install Coq, but they don't come with it bundled already. Are there any images with Coq included already? I feel like a waste of resources to run the installation of Coq at each run.

view this post on Zulip Beta Ziliani (Sep 14 2021 at 01:29):

Ah, the infamous eval $(opam env). Sorry for the noise!

view this post on Zulip Notification Bot (Sep 14 2021 at 01:29):

Beta Ziliani has marked this topic as resolved.

view this post on Zulip Erik Martin-Dorel (Sep 14 2021 at 12:20):

Hi Beta Ziliani, you said:

Ah, the infamous eval $(opam env). Sorry for the noise!

but normally the eval $(opam env) command should be unnecessary to type, because it is implied by this line:
https://github.com/coq-community/docker-base/blob/16a5f953785f2231dfc023c09fb41e6d658d7a9f/base/single/Dockerfile#L100

ENTRYPOINT ["opam", "exec", "--"]

in the base image.

Socoqtop should already be in the path, e.g.:

$ sudo docker run --rm -it coqorg/coq:8.13-ocaml-4.12-flambda

Unable to find image 'coqorg/coq:8.13-ocaml-4.12-flambda' locally
8.13-ocaml-4.12-flambda: Pulling from coqorg/coq
a330b6cecb98: Already exists
d12090a988d8: Pull complete
5d30c95e5dfe: Pull complete
853c22c7abab: Pull complete
c59b7422b397: Pull complete
25b8a59765bd: Pull complete
Digest: sha256:69570012431de10162b7b951679d46bea36203ac638dd8b0dd7aa4c82c224a30
Status: Downloaded newer image for coqorg/coq:8.13-ocaml-4.12-flambda

coq@6f074ce676cf:~$ coqtop
Welcome to Coq 8.13.2 (September 2021)

Coq <

Anyway feel free to react if you think you spotted an issue or you'd just want to have more documentation pointers.

view this post on Zulip Paolo Giarrusso (Sep 14 2021 at 13:22):

I remember the semantics of ENTRYPOINT are complex and non-transparent, so might be part of the problem.

view this post on Zulip Paolo Giarrusso (Sep 14 2021 at 13:28):

At a slightly closer look, things seem better than I remember, but ENTRYPOINT will not affect RUN in derived Dockerfiles, or run commands that specify ENTRYPOINT; there might be more.

Last updated: Jun 03 2023 at 17:29 UTC