Stream: Coq users

Topic: From Docker with love


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

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

Most of the time we connect to Docker running on our local machine, but you can also connect to Docker on a different machine too.

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

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

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

Get the latest version of Coq Interactive Prover for Linux - Coq

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

Fix #192

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

view this post on Zulip Karl Palmskog (Jan 14 2021 at 10:02):

"Coq Interactive Prover" sounds awkward

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

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

view this post on Zulip Enrico Tassi (Jan 14 2021 at 10:10):

OK, thanks for the suggestion

view this post on Zulip Enrico Tassi (Jan 14 2021 at 10:11):

updated

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

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

Get the latest version of Visual Studio Code for Linux - Code editing. Redefined.

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

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

view this post on Zulip Karl Palmskog (Jan 14 2021 at 18:11):

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

view this post on Zulip Karl Palmskog (Jan 14 2021 at 18:11):

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

view this post on Zulip Enrico Tassi (Jan 14 2021 at 18:12):

OK, done

view this post on Zulip Enrico Tassi (Jan 14 2021 at 18:12):

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

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

view this post on Zulip Enrico Tassi (Jan 14 2021 at 18:13):

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

view this post on Zulip Enrico Tassi (Jan 14 2021 at 18:14):

I think it is a rendering issue/choice

view this post on Zulip Karl Palmskog (Jan 14 2021 at 18:14):

sigh, probably some frontend processing they do then.

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

Snaps are containerised software packages that are simple to create and install. They auto-update and are safe to run. And because they bundle their dependencies, they work on all major Linux systems without modification.
Snaps are containerised software packages that are simple to create and install. They auto-update and are safe to run. And because they bundle their dependencies, they work on all major Linux systems without modification.

view this post on Zulip Paolo Giarrusso (Jan 15 2021 at 01:24):

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

view this post on Zulip Paolo Giarrusso (Jan 15 2021 at 01:27):

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

Get the latest version of Coq Interactive Prover for Linux - Coq

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

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

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

view this post on Zulip Enrico Tassi (Jan 15 2021 at 07:15):

The sources are here

view this post on Zulip Enrico Tassi (Jan 15 2021 at 07:16):

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

Multi platform setup for Coq, Coq libraries and tools - coq/platform

view this post on Zulip Enrico Tassi (Jan 15 2021 at 07:16):

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

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

Multi platform setup for Coq, Coq libraries and tools - coq/platform

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

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

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

I pull a docker image (will use python 3 as an example) docker pull python:3.6 Then I launch a docker container docker run -it -p 127.0.0.1:8000:8000 python:3.6 bash (note that here 127.0.0.1 i...

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

view this post on Zulip Paolo Giarrusso (Jan 18 2021 at 11:51):

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

view this post on Zulip Anton Trunov (Jan 18 2021 at 12:20):

It's vscoq mostly and a bit of coqide

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

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

I have a development server, which is only accessible from 127.0.0.1:8000, not 192.168.1.x:8000. As a quick hack, is there a way to set up something to listen on another port (say, 8001) so that fr...

view this post on Zulip Paolo Giarrusso (Feb 19 2021 at 20:06):

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

view this post on Zulip Paolo Giarrusso (Feb 19 2021 at 20:07):

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

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

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

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

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

view this post on Zulip Paolo Giarrusso (Feb 24 2021 at 08:53):

(And I did some experiments above).

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

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

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

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

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

view this post on Zulip Enrico Tassi (Feb 25 2021 at 21:25):

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

view this post on Zulip Enrico Tassi (Feb 25 2021 at 21:28):

it's related to lablgtk

view this post on Zulip Enrico Tassi (Feb 25 2021 at 21:28):

if I run a native gtk app, then it works

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

view this post on Zulip Enrico Tassi (Feb 25 2021 at 21:30):

ah ah, no, my bad

view this post on Zulip Enrico Tassi (Feb 25 2021 at 21:30):

it works

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

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

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