The Coq mailing list

[Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>]

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
>