Stream: Coq users

Topic: Connect PG / VsCoq to docker?


view this post on Zulip 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?

view this post on Zulip Yannick Forster (Nov 17 2022 at 13:31):

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

view this post on Zulip Huỳnh Trần Khanh (Nov 17 2022 at 14:08):

VS Code has this and it's quite easy to configure as long as you have a Docker image ready

view this post on Zulip Huỳnh Trần Khanh (Nov 17 2022 at 14:08):

https://code.visualstudio.com/docs/devcontainers/containers

view this post on Zulip Huỳnh Trần Khanh (Nov 17 2022 at 14:10):

Disclaimer: not a researcher, I'm not sure if this satisfies your research use case

view this post on Zulip 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:

  1. 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

view this post on Zulip 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.

view this post on Zulip Erik Martin-Dorel (Nov 17 2022 at 15:12):

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

view this post on Zulip Huỳnh Trần Khanh (Nov 17 2022 at 15:43):

(deleted)

view this post on Zulip Théo Zimmermann (Nov 17 2022 at 17:26):

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

view this post on Zulip 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?

view this post on Zulip 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/...

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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: Jan 31 2023 at 14:03 UTC