[Coq-Club] Latest Coq does not install smoothly using opam on ubuntu 16.04

[Arthur Charguéraud]

Dear Coq user,

If you are using opam or if you are recommending your students to use
opam to install Coq, you may be interested to know that it does not work
out of the box anymore.

- The opam package for coqIDE associated with coq=8.8.2 is only
distributed in opam2 format
- opam2 activates sandboxing by default, using bubblewrap >= 2.0
(program name bwrap)
- ubuntu 16.04 distributes only an older version of bubblewrap
- opam2 installation scripts fails with an obscur error when using the
old bubblewrap.

Workaround is to manually install a recent bubblewrap, or disable
sandboxing (not easy, and not recommended).

(For details: https://github.com/ocaml/opam/issues/3424)

+
Arthur

[Christian Doczkal]

Hello Arthur,

- The opam package for coqIDE associated with coq=8.8.2 is only distributed in opam2 format

Good point, I only pushed for the coq package to be in the coq-released repository (which is still in 1.x format). I suppose there is no reason not to add the coqide package as well.

- opam2 activates sandboxing by default, using bubblewrap >= 2.0 (program name bwrap)
- ubuntu 16.04 distributes only an older version of bubblewrap

As far as I know, not even Ubuntu 18.10 ships opam-2. I would already consider manually installing opam as "not smooth" (as in, it leads to programs being installed that no package manager knows about).

- opam2 installation scripts fails with an obscur error when using the old bubblewrap.

I'm not surprised...

Best,
Christian

[Théo Zimmermann]

Hello,

I recently discovered the existence of the following ppa which includes
an opam 2 package for both bionic and cosmic:
https://launchpad.net/~avsm/+archive/ubuntu/ppa

Might be of interest to some.

Disclaimer: I haven't tested it (as I don't use Ubuntu, nor opam for the
matter).

Théo

Post by Christian Doczkal
Hello Arthur,

- The opam package for coqIDE associated with coq=8.8.2 is only distributed in opam2 format

Good point, I only pushed for the coq package to be in the coq-released repository (which is still in 1.x format). I suppose there is no reason not to add the coqide package as well.

- opam2 activates sandboxing by default, using bubblewrap >= 2.0 (program name bwrap)
- ubuntu 16.04 distributes only an older version of bubblewrap

As far as I know, not even Ubuntu 18.10 ships opam-2. I would already consider manually installing opam as "not smooth" (as in, it leads to programs being installed that no package manager knows about).

- opam2 installation scripts fails with an obscur error when using the old bubblewrap.

I'm not surprised...
Best,
Christian

[Vadim Zaliva]

I am using opam v2 from this PPA for about a week now and happy to report
it works well with coq packages.

Vadim

--
CMU ECE Ph.D. candidate
Mobile/Signal/WhatsApp: [phone]

Post by Théo Zimmermann
Hello,
I recently discovered the existence of the following ppa which includes
https://launchpad.net/~avsm/+archive/ubuntu/ppa
Might be of interest to some.
Disclaimer: I haven't tested it (as I don't use Ubuntu, nor opam for the
matter).
Théo

Post by Christian Doczkal
Hello Arthur,

Post by Arthur Charguéraud
- The opam package for coqIDE associated with coq=8.8.2 is only

distributed in opam2 format

Post by Christian Doczkal
Good point, I only pushed for the coq package to be in the coq-released

repository (which is still in 1.x format). I suppose there is no reason not
to add the coqide package as well.

Post by Christian Doczkal

Post by Arthur Charguéraud
- opam2 activates sandboxing by default, using bubblewrap >= 2.0

(program name bwrap)

Post by Christian Doczkal

Post by Arthur Charguéraud
- ubuntu 16.04 distributes only an older version of bubblewrap

As far as I know, not even Ubuntu 18.10 ships opam-2. I would already

consider manually installing opam as "not smooth" (as in, it leads to
programs being installed that no package manager knows about).

Post by Christian Doczkal

Post by Arthur Charguéraud
- opam2 installation scripts fails with an obscur error when using the

old bubblewrap.

Post by Christian Doczkal
I'm not surprised...
Best,
Christian