Connect PG / VsCoq to docker? · Coq users

Stream: Coq users

Topic: Connect PG / VsCoq to docker?

Yannick Forster (Nov 17 2022 at 13:30):

We're trying to run an old Coq development based on 8.9.1 on a new Mac M1, which doesn't work because the necessary OCaml versions are not available. A viable path is to use the coqorg docker images to get Coq running. Does anybody have experience with connecting Coq run in a docker image to any IDE?

Yannick Forster (Nov 17 2022 at 13:31):

@Erik Martin-Dorel might be a good candidate to know :)

Huỳnh Trần Khanh (Nov 17 2022 at 14:08):

(deleted)

Huỳnh Trần Khanh (Nov 17 2022 at 14:08):

(deleted)

Huỳnh Trần Khanh (Nov 17 2022 at 14:10):

(deleted)

Erik Martin-Dorel (Nov 17 2022 at 15:06):

Yannick Forster said:

Erik Martin-Dorel might be a good candidate to know :)

@Yannick Forster thanks for the ping, actually with emacs, we have two feasible strategies:

either you install Emacs+PG directly in the docker image, and albeit there is typically no graphical interface within docker CLI, you can always use emacs -nw

→ you can find one such "extended" image example here:

https://gitlab.com/erikmd/docker-coq-primitive-floats/container_registry/3622214

https://gitlab.com/erikmd/docker-coq-primitive-floats/-/blob/master/Dockerfile

and a ready-to-use auto-setup .emacs here:

https://github.com/erikmd/tapfa-init.el/raw/master/.emacs

Erik Martin-Dorel (Nov 17 2022 at 15:07):

To be more precise, a comprehensive CLI workflow would be:

docker pull registry.gitlab.com/erikmd/docker-coq-primitive-floats/master_coq-8.15-flambda-validsdp-1.0.1:latest
# or docker build etc.

mkdir -p data && docker run --name=COQ -it -v "$PWD/data:/data" registry.gitlab.com/erikmd/docker-coq-primitive-floats/master_coq-8.15-flambda-validsdp-1.0.1:latest emacs -nw /data

C-x C-c

ls -hal data

docker start -ai COQ

etc.

Erik Martin-Dorel (Nov 17 2022 at 15:12):

or, to benefit from a graphical interface and avoid extending the images, one could directly open an emacs session and connect to a coqtop taken from a coqorg/coq image.

I've seen some dedicated emacs modes allowing this, and even if this is not a use case for my everyday coq developments (I prefer to use opam-switch-mode), I am also interested to document this for interested users.

So if you want, we could discuss this together in PM Zulip (or Zoom) these days to exchange pointers? and ideally add the outcome somewhere if you want… (at least, here :)

Huỳnh Trần Khanh (Nov 17 2022 at 15:43):

(deleted)

Théo Zimmermann (Nov 17 2022 at 17:26):

Just FTR, another solution (besides Docker) for this use case is Nix.

Paolo Giarrusso (Nov 17 2022 at 18:44):

But if Coq 8.9.1 doesn't work on OCaml 4.10.2, I don't think NixPkgs for Mac can fix that?

Paolo Giarrusso (Nov 17 2022 at 18:46):

OTOH, a Linux VM for ARM will support older OCaml versions (it's only Mac + ARM that's recent) — whether with or without Nix/Docker/...

Paolo Giarrusso (Nov 17 2022 at 18:48):

OTOH, beware that a Linux VMs for x86 do not enjoy Rosetta speed AFAIK; certainly not for Docker x86 images. The slowdown I remember was about 6x, which might be okay for you but made me reach my Intel Mac ~~reactor~~ computer

Yannick Forster (Nov 21 2022 at 11:09):

Using the link provided by @Huỳnh Trần Khanh (https://code.visualstudio.com/docs/devcontainers/containers) with the coqorg/coq-8.09.1 image worked great :) But indeed as noted by @Paolo Giarrusso, compilation is slow and compiling MetaCoq requires -j 1 because otherwise the container runs out of memory - but it works

Yannick Forster (Nov 21 2022 at 11:11):

As of today, that seems the easiest way to go for me. But I'd be happy to see a way to connect a PG instance to a docker-based coqtop (not least because in the future, reproducibility of old builds will be an issue, and we would like users to be able to run a ~10 year old Coq project easily)

Last updated: Oct 13 2024 at 01:02 UTC