Stream: Coq users

Topic: From Docker with love

Paolo Giarrusso (Jan 13 2021 at 22:05):

Did anybody look into running Coq in Docker but using IDEs with it? I could put docker run ... -v <map local folder> -- coq in a wrapper, but I wanted to ask before reinventing the wheel

Paolo Giarrusso (Jan 13 2021 at 22:06):

as a bonus, it seems one can connect to a remote Docker daemon and run Coq on a more powerful computer
(TODO: read https://nickjanetakis.com/blog/docker-tip-73-connecting-to-a-remote-docker-daemon)

Anton Trunov (Jan 14 2021 at 07:49):

Paolo, please post your findings somewhere if you find a solution. I'm also interested in this setup (more from the prospect of managing student setups than my own, probably).

Guillaume Melquiond (Jan 14 2021 at 09:11):

for what is worth, we are running Why3's graphical interface from inside a Docker, so I presume the exact same setup would work for Coq (note that the IDE is shipped as part of the Docker image; we are not trying to make an external editor interact with binaries inside an image, so I do not know if that is what Paolo intended): https://why3.gitlabpages.inria.fr/why3/install.html#installation-via-docker

Enrico Tassi (Jan 14 2021 at 09:49):

It's not docker, but a similar container based package. It's still in beta phase (not listed in the search engine). Feedback is welcome especially for students. It's based on the Coq platform, so it contains all that is in there (if you want to add something, ask there): https://snapcraft.io/coq-prover

Enrico Tassi (Jan 14 2021 at 09:49):

It comes with CoqIDE and modulo https://github.com/coq-community/vscoq/pull/194 (or a manual config) works with vscode as well

Enrico Tassi (Jan 14 2021 at 09:50):

(CoqIDE runs from the container, vscode is not bundled, but can be found in the same store)

Karl Palmskog (Jan 14 2021 at 10:02):

"Coq Interactive Prover" sounds awkward

Enrico Tassi (Jan 14 2021 at 10:06):

I can change the title, but the store admins suggested to make it clear what it is. What do you find weird? Would "Coq - Interactive Prover" work better?

Karl Palmskog (Jan 14 2021 at 10:07):

the only ones that make sense to me are "Coq Interactive Theorem Prover" and "Coq Proof Assistant"

Enrico Tassi (Jan 14 2021 at 10:10):

OK, thanks for the suggestion

Enrico Tassi (Jan 14 2021 at 10:11):

updated

Karl Palmskog (Jan 14 2021 at 17:59):

@Enrico Tassi almost all the licenses for the platform are nicely SPDX, but IMO the license for Coq should be fully SPDX as well: LGPL-2.1-only (right now it's LGPL-2.1 on the snapcraft page)

Karl Palmskog (Jan 14 2021 at 18:02):

I also think you should add the Development category in addition to Science and Education (e.g., CoqIDE is essentially a tool like VsCode, which uses Development category, https://snapcraft.io/code)

Enrico Tassi (Jan 14 2021 at 18:07):

Unfortunately I can only have 2 categories, maybe education is a bit of a stretch... but development is as well a bit of a stretch imo

Enrico Tassi (Jan 14 2021 at 18:08):

For the license, I did select 2.1-only from a list of SPDX, and it is printed like that. In the package description I take the ones from OPAM. I also tried to write a custom SPDX expression, but I get a parse error at -only

Karl Palmskog (Jan 14 2021 at 18:11):

why is Development a stretch? I disagree, given all the verified software projects using Coq.

Karl Palmskog (Jan 14 2021 at 18:11):

given only two categories, I would go with Science and Development

Enrico Tassi (Jan 14 2021 at 18:12):

OK, done

Enrico Tassi (Jan 14 2021 at 18:12):

For the license, I really don't know how to improve

Karl Palmskog (Jan 14 2021 at 18:13):

I guess it's fine. We can only blame the FSF for the annoying or later stuff

Enrico Tassi (Jan 14 2021 at 18:13):

Screenshot-from-2021-01-14-19-13-22.png

Enrico Tassi (Jan 14 2021 at 18:14):

I think it is a rendering issue/choice

Karl Palmskog (Jan 14 2021 at 18:14):

sigh, probably some frontend processing they do then.

Paolo Giarrusso (Jan 15 2021 at 01:24):

https://snapcraft.io/search?q=coq and https://snapcraft.io/search?q=coq-prover find nothing? Just because it's beta?

Paolo Giarrusso (Jan 15 2021 at 01:24):

@Enrico Tassi where's the source of the snap package?

Paolo Giarrusso (Jan 15 2021 at 01:27):

I can't find a link from https://snapcraft.io/coq-prover...

Paolo Giarrusso (Jan 15 2021 at 01:30):

in any case, my use case seems closer to Why3, plus it might include some internal software: my company has an opam repository, Coq binary, coqdep patch, and our choice of Coq plugins.

Paolo Giarrusso (Jan 15 2021 at 01:35):

OTOH, part of the motivation was harder-to-install dependencies like coinor-csdp (psatz's backend), and for that I opened a thread.

Paolo Giarrusso (Jan 15 2021 at 01:48):

okay, found the answer: browsing the sources is not supported, I have to download the snap (https://merlijn.sebrechts.be/blog/2020-08-17-verify-snap/). I'll infer snap might not be what I specifically need. Still cool.

Enrico Tassi (Jan 15 2021 at 07:15):

The sources are here

Enrico Tassi (Jan 15 2021 at 07:16):

https://github.com/coq/platform/tree/v8.13/linux

Enrico Tassi (Jan 15 2021 at 07:16):

It is not listed cause I didn't make the snap fully public yet

Enrico Tassi (Jan 15 2021 at 07:18):

Adding software is trivial, you can edit https://github.com/coq/platform/blob/v8.13/coq_platform_packages.sh for opam stuff, or edit the snapcraft file for Debian stuff

Enrico Tassi (Jan 15 2021 at 07:23):

Btw, being able to customize the platform is an objective of the platform scripts (eg for teachers) so feel free to ask around if doc or features are missing

Paolo Giarrusso (Jan 18 2021 at 11:42):

Initial analysis suggests supporting Emacs might be easy — cmdline coqtop works out of the box with
docker run --rm -i some_coq_image coqtop
but I'm only assuming that's all that Emacs needs.
That works even under rlwarap:
rlwrap docker run --rm -i some_coq_image coqtop
notably, that doesn't work well with the common run -it, because the latter allocates a pseudo-tty (like e.g. ssh would), which is not what rlwrap (or most clients) expect.

Paolo Giarrusso (Jan 18 2021 at 11:48):

or rather, supporting vscoq & c. _outside_ might be harder — vscoq listens on some localhost ports and expects coqidetop to connect to them. But vscoq actually listens on _localhost_, preventing access from other machines (which, likely, is for the better) or even containers (except maybe on Linux with https://stackoverflow.com/a/57422557/53974).

Paolo Giarrusso (Jan 18 2021 at 11:50):

I'll look into Why3's approach next (_at some point_), but I'd expect some trouble running VsCode in a container (at least, it using the wrong keybindings for a Mac)

Paolo Giarrusso (Jan 18 2021 at 11:51):

@Anton Trunov do you have students use Emacs, coqide, or vscoq?

Anton Trunov (Jan 18 2021 at 12:20):

It's vscoq mostly and a bit of coqide

Guillaume Melquiond (Jan 18 2021 at 12:50):

Paolo Giarrusso said:

except maybe on Linux.

Yes, if you choose --network host, then the container uses the same network stack, so connections to localhost work fine.

Paolo Giarrusso (Jan 22 2021 at 05:10):

More portable idea (for non-Linux): have the wrapper parse the relevant options to find the chosen ports, and interpose an ssh tunnel between the two machines. (or apparently socat if you don't need the security, e.g. when using Docker https://unix.stackexchange.com/a/187038/28519)

Paolo Giarrusso (Feb 19 2021 at 20:06):

@Aleksey Arens here’s a fun candidate for “running Coq inside a VM-y thing”

Paolo Giarrusso (Feb 19 2021 at 20:07):

(hm, I should find the time to do it)

Aleksey Arens (Feb 19 2021 at 20:09):

Paolo Giarrusso said:

Aleksey Arens here’s a fun candidate for “running Coq inside a VM-y thing”

I wonder if Coq could run inside a mirageOS instance? I doubt it should, since it's not SMP AFAIK.

Aleksey Arens (Feb 20 2021 at 00:06):

Paolo Giarrusso said:

Did anybody look into running Coq in Docker but using IDEs with it? I could put docker run ... -v <map local folder> -- coq in a wrapper, but I wanted to ask before reinventing the wheel

I presume, a text-based connection is all that is needed. In that case, emacs's proof-general would be more than adequate. I also don't see any great difficulties with adjusting any existing IDEs to work over a network connection; worst case scenario would involve interacting with socat, possibly through a wrapper binary.

Clément Pit-Claudel (Feb 24 2021 at 04:08):

I've run Coq in VMs before and connected to it using a local Emacs + TRAMP; not sure how well that would work with Docker

Paolo Giarrusso (Feb 24 2021 at 08:51):

If Emacs is good enough for you (it’s not for me), wrapping coq with the right “docker run” incantation should just work. That’s a common Docker use-case.

Paolo Giarrusso (Feb 24 2021 at 08:53):

(And I did some experiments above).

Guillaume Melquiond (Feb 24 2021 at 09:03):

Something I recently tried with Why3 is to run it using Broadway. And surprisingly enough, it works out of the box. (Despite all its flaws, GTK never ceases to amaze.) You just need to set the environment variable GDK_BACKEND=broadway before running coqide and to export port 8080 of your Docker container, and that is it. (Possibly, you might have to first execute broadwayd & in your Docker container. I have never quite understood when explicitly running the multiplexer is needed.)

Guillaume Melquiond (Feb 24 2021 at 09:04):

And I missed the most important part: You have to point your web browser to localhost:8080, since the whole point of changing the backend is to use your browser as the graphical interface of coqide.

Paolo Giarrusso (Feb 25 2021 at 21:18):

Oooooh https://developer.gnome.org/gtk3/stable/gtk-broadway.html (for all the others who'll be googling)

Enrico Tassi (Feb 25 2021 at 21:21):

gares@ollypat:~/MATHCOMP/hierarchy-builder$ broadwayd :5
Listening on /run/user/1000/broadway6.socket
^Z
[1]+  Stopped                 broadwayd :5
gares@ollypat:~/MATHCOMP/hierarchy-builder$ bg
[1]+ broadwayd :5 &
gares@ollypat:~/MATHCOMP/hierarchy-builder$ GDK_BACKEND=broadway BROADWAY_DISPLAY=:5 coqide
Unable to init server: Could not connect: Connection refused
Fatal error: exception Gtk.Error("GtkMain.init: initialization failed\nml_gtk_init: initialization failed")

Paolo Giarrusso (Feb 25 2021 at 21:24):

Generic troubleshooting Qs: Do all GTK versions support Broadway? My link is for gtk3, and I'd bet there's a compile-time flag? You'd hope if you have the daemon it was enabled.

Enrico Tassi (Feb 25 2021 at 21:25):

ii libgtk-3-0:amd64 3.24.20-0ubuntu1 amd64 GTK graphical user interface library

Enrico Tassi (Feb 25 2021 at 21:28):

it's related to lablgtk

Enrico Tassi (Feb 25 2021 at 21:28):

if I run a native gtk app, then it works

Enrico Tassi (Feb 25 2021 at 21:29):

I've 3.1.1, maybe @Guillaume Melquiond used an older version and this is a regression

Enrico Tassi (Feb 25 2021 at 21:30):

ah ah, no, my bad

Enrico Tassi (Feb 25 2021 at 21:30):

it works

Enrico Tassi (Feb 25 2021 at 21:31):

I was runing coqide from the snap package, which is "app armored" (I think I did not give it the network capability)

Guillaume Melquiond (Feb 25 2021 at 21:32):

Yes, broadwayd needs to run inside the container. And then you just export the port it opens.

Paolo Giarrusso (Jul 12 2021 at 20:57):

Never got around to this but VsCode's previewing a general solution:
https://code.visualstudio.com/docs/remote/containers#_quick-start-open-an-existing-folder-in-a-container

Last updated: Oct 05 2023 at 02:01 UTC