coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Vadim Zaliva <vzaliva AT cmu.edu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Latest Coq does not install smoothly using opam on ubuntu 16.04
Date: Mon, 26 Nov 2018 10:38:50 -0800
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=vzaliva AT cmu.edu; spf=Pass smtp.mailfrom=vadim.zaliva AT west.cmu.edu; spf=None smtp.helo=postmaster AT mail-it1-f196.google.com
Ironport-phdr: 9a23:Cy6c8BRWKFjjcT9ZEsHAbuzWptpsv+yvbD5Q0YIujvd0So/mwa69ZxyN2/xhgRfzUJnB7Loc0qyK6/CmATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfbB/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/27ZisNyjKxVrhGvqQFhzYHIe4yaLuZyc7nHcN8GWWZMXMBcXDFBDIOmaIsPCvIMMulCoIbgplsOqAa1Cgq2C+Pryz9ImGX51rA93uQ/EADJxgggH9MQsHvOt9j6KKISUf2vwKbW0DrDcupb1DHg44bGdRAhpOuDXbN2ccfJzUkgDR7FjlOMpozlJzOazPkCv3Kd7+V+SeKijXMspQJpojW32Msglo3EipgWx13E7yl13Yc4KNyiREJmZdOpEZ1dvDyAOYRsWMMtWWRotT46yrIYvZ67ezAHyJE9yB7eb/yLaomI4g7+WOqILzd0mXZodbOlixa99kigzeL8Vs2q31pQsiVFldzMumgM1xzV9MeHVuNw8lm91TuLzQze6eFJLVopmafaKpMt2KM8m54SvEjbGy/5gkT2jKuYdkU+/eio7vzqYqv8qZCBNo90jxvyM6U0lcy7AOQ4LBIBUnOV+Ouiz73j4Vf1T6lPjv0riKXWro3VJdkDqq6jHwBVypoj6wq4Dzq+zNsYmmAHIEtZdxKDkojmIErDIOv4DPe6m1Sjii1nx/HAPr37A5XCNGLPkLn7feU110kJww0qiNtb+ph8C7cbIfu1VFWimsbfC0oHOgC1xq7VAdF8yIpWDXydC6uYLqr6ulqVoO8jPr/fN8cupD/hJq19tLbVhngjlApFJPj77d4scHm9W89eDQCcaHvojM0GFD5W7BUzV/Csg1ifFzNfeiTrBv5u1nQAEIujSLz7aMW1mrXQjiy+A9tban0UUgnRQ0etTJ2NXrI3UAzXIsJllWZaB72oSotk1A338QGjmuQhIe3T9SkV85nk0Yot6g==

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

On Mon, Nov 26, 2018 at 5:10 AM Théo Zimmermann <theo.zimmi AT gmail.com> wrote:

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

On 14/11/2018 00:23, Christian Doczkal wrote:
> 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
>

[Coq-Club] Latest Coq does not install smoothly using opam on ubuntu 16.04, Arthur Charguéraud, 11/13/2018
- Re: [Coq-Club] Latest Coq does not install smoothly using opam on ubuntu 16.04, Christian Doczkal, 11/14/2018
  - Re: [Coq-Club] Latest Coq does not install smoothly using opam on ubuntu 16.04, Théo Zimmermann, 11/26/2018
    - Re: [Coq-Club] Latest Coq does not install smoothly using opam on ubuntu 16.04, Vadim Zaliva, 11/26/2018