Package Details: coq 8.6-4

Git Clone URL: (read-only)
Package Base: coq
Description: Formal proof management system
Upstream URL:
Licenses: GPL
Groups: coq
Conflicts: coq-nox
Replaces: coq-nox
Submitter: td123
Maintainer: zorun
Last Packager: zorun
Votes: 62
Popularity: 2.465776
First Submitted: 2012-04-09 20:45
Last Updated: 2017-02-06 19:38

Required by (6)

Sources (3)

Latest Comments

kellino commented on 2017-02-07 08:06

Thanks, everything is working perfectly now.

zorun commented on 2017-02-06 19:39

kellino: your issue should be fixed, coqidetop.cmxs is now installed in the main "coq" package.

zorun commented on 2017-02-05 14:19

I've just updated the package again, because the lablgtk2 issue was solved.

So, you need lablgtk2 2.18.5-4, maybe your mirror still doesn't have it. You can wait for your mirror to update, or fetch it directly from

kellino commented on 2017-02-05 14:14

Thanks for the quick response. Let's see what upstream says.

I've just tried to install the coqide package, despite all the extra dependencies, but this fails to build.

The error is Incomplete lablgtk2 (in OCaml library) : no /usr/lib/ocaml/lablgtk2/gSourceView.cmi

but isn't this pulled in as a dependency of coq? I tried removing every coq related thing I could find in my system and reinstalling (both as coq and then coqide seperately, and just with coqide pulling in coq as a dependency) but the error is the same. So, coqtop works, but I can't install coqide or use coquille - and what's more, mathcomp no longer compiles :(

zorun commented on 2017-02-04 20:03

Yes, I think it's related to the new split: coq-nox was calling "make install", which apparently installed some bits related to coqide even if coqide itself was not built. The new coq package runs "make install-coq", which omits everything related to coqide.

There are two possibilities:

1) keep coq and coqide as it is, and ensure coquille depends on coqide. Unfortunately, it means that coquille would pull a lot of graphical dependencies, even on headless systems where it is useless and unwanted.
2) move the files needed by coquille to the main "coq" package (which means deviating from upstream or submitting the change upstream)

The second solution is better if the change can be made upstream, I'll poke the maintainers to know if it's possible.

kellino commented on 2017-02-04 19:20

Hi, I was previously using coq-nox with the vim plugin coquille. everything worked beautifully (thanks). Using this new package though I get the error

Error during initialization:
Error: File not found on loadpath : coqidetop.cmxs

Coquille tries to launch coqtop with the following flags "-ideslave -main-channel stdfds -async-proofs on".

Any suggestions as to why the coqidetop.cmxs file is missing? Is it now part of the coqide package or has it been removed entirely?



zorun commented on 2017-02-03 16:36

andres: Thanks for the suggestion! My intention was to build a split package for [community] with coq, coq-doc, and coqide. But if coqide is difficult to build because of dependencies, it is indeed possible to only move coq and coq-doc to [community] and keep coqide in the AUR.

As for the delay, it's mostly because my PGP key is still not in the Arch keyring. Since it's taking much longer than expected, I just pushed coq 8.6 to the AUR. Also, coqide is now a separate package, in preparation for coq entering [community].

andres commented on 2017-02-03 14:38

Does coq itself depend on lablgtk2-full, or just the IDE? I think it would make a lot of sense to move Coq to community and keep the (less awesomely maintained) IDE in AUR for the time being. I would be completely unsurprized if CoqIDE kept breaking faster than we can keep fixing it, while proofgeneral has been flawlessly stable... longer than I have used coq (a couple of years). At the very least, I find it unfortunate that coq-8.6 is getting delayed (in a roundabout way) on arch due to CoqIDE sadness. I would be willing to lend a hand with some of the work here -- especially if that meant I can stop maintaining my own fork of this package.

zorun commented on 2017-02-03 11:22

IooNag: As a workaround, I pushed a package lablgtk2-full with the missing binding. This needs to be fixed properly before moving coq to [community]...

IooNag commented on 2017-01-31 23:25

Package coq 8.5pl3-1 no longer builds on an up-to-date system because Gtksourceview bindings have been removed from lablgtk2 2.18.5-3. This removal is on-purpose, for the reason stated in .

All comments