Discussion:
[Coq-Club] Latest Coq does not install smoothly using opam on ubuntu 16.04
Arthur Charguéraud
2018-11-13 13:06:42 UTC
Permalink
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
2018-11-13 23:23:31 UTC
Permalink
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
2018-11-26 13:09:49 UTC
Permalink
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
2018-11-26 18:38:50 UTC
Permalink
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: +1(510)220-1060
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
Loading...