The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

Hi Jeremy,

On Linux, it is not traditionally the role of a software development team to prepare the packages for the various Linux distribution. It is instead assumed to be the role of the distribution maintainers.

So while, there have been significant efforts and pain to provide Windows and macOS installers, Linux has received less attention.

Unfortunately, not all Linux distributions are equal in terms of the attention given to the Coq package (ArchLinux is very up-to-date, and Ubuntu is lagging very much), as can be seen here https://repology.org/metapackage/coq/versions.

Furthermore, on standard Linux distributions, upgrading from one version of a software to the next major one generally requires upgrading the entire system. Work computers are often provided on LTS versions of Ubuntu, which means that even if the distribution maintainers were keeping the package up-to-date, there would be a significant delay before the users can benefit from the upgrade.

That's why it is generally recommended to use opam to install an up-to-date Coq (and packages).

Unfortunately, opam itself isn't without issues and not trivial to use for the casual user. One issue in particular is that it installs everything from source. In the case of CoqIDE, there will be system dependencies (on gtk libraries) that need to be installed by the user, which might not be trivial to do either. Then there is also the problem of the long time it takes to build a package from sources. (It is however surprising that it takes a long time to download the sources.)

It is quite sad that, as of today, it has become much more complex to install an up-to-date Coq + CoqIDE on Linux than on Windows. This is to fix this that Enrico has recently started to look into providing a snap package (https://github.com/coq/coq/issues/9289).

We can definitely not substitute ourselves to the distribution maintainers and provide packages for a variety of distributions. However, the Snap platform seems to be targeting portability over all Linux distributions, so this seems indeed like a way to workaround this problem. Eventually, it should also be doable to provide a set of external packages on Linux via the Snap package as we do on Windows when using the installer...

Regarding the learning of Coq and CoqIDE, I don't think that it is two things that you should regard as separate. Any student learning Coq today learns to use Coq through an environment like CoqIDE or Proof-General (both provide very similar features). Learning Coq using coqtop only means making one's life harder, not easier, even if it can feel like you are learning less stuff at the same time. Indeed, user interfaces will make standard operations like stepping back earlier in a proof, or replaying it, significantly easier.

It's like programming: the invention of editors, then IDEs, did not make it harder but easier...

Cheers,

Théo

Le mar. 15 janv. 2019 à 03:23, Jeremy Dawson <Jeremy.Dawson AT anu.edu.au> a écrit :

Hi Laurent/Theo,

Thanks for the hint about dnf search - something I should have tried.

that was at home, here at work it's ubuntu, and the latest package (with
the IDE one called coqide) is version 8.4.

So I tried to install coqide using the instructions at
https://coq.inria.fr/opam/www/using.html, but got errors

[ERROR] curl: code 404 while downloading
         https://opam.ocaml.org/archives/coqide.8.7.2+opam.tar.gz
[ERROR] curl: code 404 while downloading
         https://opam.ocaml.org/archives/lablgtk.2.18.5+opam.tar.gz
[ERROR] The sources of the following couldn't be obtained, aborting:
           - coqide.8.7.2
           - lablgtk.2.18.5
         (This may be fixed by running 'opam update')

So I tried that but it seemed to hang.
(Maybe it didn't, see below).

So I tried to install the latest version (which an email a few months
ago suggested, but I had put this off, since installing coq was so
difficult the first time I did it).

Right now it seems that the opam init step is populating a the directory
~/opam-coq.8.8.2 at the glorious speed of about 1MB per minute.  So
maybe opam update wasn't hanging earlier.

Meanwhile - since I've been wondering what it is that is being
downloadad - I see that (based on the original installation) there is
292MB of stuff in ~/opam-coq.8.7 of which a lot seems to be not
software, but information about software available in the repository,
and 423MB of stuff in ~/.opam of which a lot seems to be empty directories.

Is this stuff all to do with coq, or simply to do with ocaml more generally?

Would it be possible to make the coq software (only) available
somewhere, like on github?  (or - and I've no idea how much effort is
involved in doing this - Fedora and Ubuntu packages for recent versions?)

I should say that there are times I've considered other software
packages, and abandoned thoughts of using them because of the difficulty
of installation, when they haven't been nearly as difficult as this.

And back to the subject of coqide: Coq is not easy to learn.  I don't
think it is helpful for developers to approach the system on the basis
that users ought to learn to use something else, as well, at the same
time.  I acknowledge that, so far as I can see, coqide doesn't or may
not share the horrible features of a similar IDE for another theorem
prover I've used, but nonetheless you don't want to be telling users
that they should learn about something else while they're trying to
learn to use Coq.

Cheers,

Jeremy



On 15/1/19 8:16 am, Laurent Thery wrote:
>
>
> On 1/14/19 10:14 PM, Jeremy Dawson wrote:
>> I'm using the Fedora package coq.  Is there a different package for coqide?
>
> Yep, on my machine
>
> % dnf search coqide
> ======================= Name & Summary Matched: coqide
> ========================
> coq-coqide.x86_64 : Coqide IDE for Coq proof management system
>
> --
> Laurent
>