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.469930
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 .

zorun commented on 2017-01-07 16:26

I am aware that coq 8.6 has been released, but I will soon push the new version directly to [community]. The structure of the new packages will be different:

- coq: will contain the base installation (without the IDE)
- coqide: will contain the IDE
- coq-doc: documentation built from source

So, if you were using `coq-nox`, you will want to install `coq`. If you were using `coq` (which included the IDE up to now), you will want to install both `coq` and `coqide`.

LligngG commented on 2016-09-26 19:29

Oops… nevermind, sorry… :-s
Problem solved… 4Go of RAM, no swap… with -j1 it work just fine. With -j2, OOM killer make it "work"…

Sorry :-s

LligngG commented on 2016-09-26 18:59

Hi, I have performed some more tests (making sure I wasn't changing anything but the -j option), and I have this error with -j n>1 (the file triggering the error seem to be random).

I have a very fresh arch install with an intel i3 6100.
the error look like that:
COQC theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
<W> Grammar extension: in [tactic:simple_tactic] some rule has been masked
<W> Grammar extension: in [tactic:simple_tactic] some rule has been masked
Error: Could not compile the library to native code.
make[1]: *** [ theories/QArith/QArith_base.vo] Error 1
make[1]: *** Waiting for unfinished jobs....
make[1]: Leaving directory '/tmp/yaourt-tmp-simon/aur-coq/src/coq-8.5pl2'
make: *** [Makefile:159: submake] Error 2

But, I should have done that before post it here, I tried with the source from the coq website, I have the same bug…

zorun commented on 2016-09-24 14:23

What error do you have? It builds fine here with -j6.

LligngG commented on 2016-09-24 14:08

Maybe its an upstream bug, but it doesn't build with -j make option in /etc/makepkg.conf



zorun commented on 2016-07-11 21:09

Updated to 8.5pl2, which seems to have fixed the mysterious compilation issue!

zorun commented on 2016-05-11 19:37

I have bumped the package to 8.5pl1.

Let me know if the issue with lablgtk2 is still there. If you don't need coqide, just use the `coq-nox` package.

gsnedders commented on 2016-02-24 21:22

@zorun I'm having the same problem, where it's finding it via ocamlfind and failing in the same way. This is with it installed from the normal package.

gsnedders@vanveen:~$ ocamlfind query lablgtk2
gsnedders@vanveen:~$ pacman -Qo /usr/lib/ocaml/lablgtk2
/usr/lib/ocaml/lablgtk2/ is owned by lablgtk2 2.18.3-2

zorun commented on 2016-02-16 20:56

The problem seems to be that you have another installation of lablgtk2:

"LablGtk2 found (via ocamlfind), with native threads"

On my system, lablgtk2 is provided via the normal Archlinux package:

"LablGtk2 found (in OCaml library), with native threads"

How did you install lablgtk2? Do you use opam?

tomoki commented on 2016-02-12 11:28


Thank you for your help.
Here is full log of "yaourt -S coq --noconfirm".

My system is up to date currently (2016/02/12), and ocaml version is 4.02.3 which is taken from official arch repository.

And, "pacman -Qs ocaml" outputs .

My system is 64bit, which runs on i7-5600U.

zorun commented on 2016-02-11 12:48

Hi tomoki,

I cannot reproduce this error. A quick search dig out these seemingly related bug reports:

Which version of ocaml are you using? Is your system up-to-date?

Could you provide the output of the start of compilation? It should look like this:
Can you also provide the output of "pacman -Qs ocaml"?

tomoki commented on 2016-02-06 07:53

Thank you for mentaining this package!

I got following error when I build this package:

OCAMLDEP checker/
OCAMLBEST -o bin/ocamllibdep
/usr/bin/ld: /usr/lib/ocaml/libasmrun.a(startup.o): relocation R_X86_64_32 against `.rodata.str1.1' can not be used when making a shared object; recompile with -fPIC
/usr/lib/ocaml/libasmrun.a: error adding symbols: Bad value
collect2: error: ld returned 1 exit status
File "caml_startup", line 1:
Error: Error during linking
make[1]: *** No rule to make target 'bin/ocamllibdep', needed by 'grammar/grammar.mllib.d'. Stop.

Any ideas?

srl commented on 2016-01-26 17:08

A nice touch would be a .desktop file for coqide. There's one at [1], for instance.


zorun commented on 2016-01-23 19:00

Indeed, when updating to 8.5, I thought camlp4 was bundled with ocaml. I have now added the missing dependency, thanks!

jdarch commented on 2016-01-23 18:46

Shouldn't camlp5 or camlp4 be a dependency?

atondwal commented on 2016-01-23 16:58

Here's the PKGBUILD updated for the newest stable version (8.5):

zorun commented on 2016-01-21 22:12

Thanks for the heads-up about coq 8.5. However, it does not compile:

make[1]: *** No rule to make target 'parsing/', needed by 'parsing/compat.cmo'. Stop.
make[1]: *** Waiting for unfinished jobs....

Forcing camlp4 instead of camlp5 seems to work fine, I'll probably update the package this way.

CIB commented on 2015-08-10 16:02

I also get an error with camlp5-transitional. Changing it to camlp4 fixed it for me.

CAMLP4O lib/compat.ml4
Error while loading "tools/compat5.cmo": interface mismatch on Pervasives.

zorun commented on 2015-06-25 09:11

It looks like the compiler was killed during your package build... Maybe you don't have enough RAM?

It builds fine for me with camlp5-transitional 6.12 for the AUR.

anastas commented on 2015-06-11 15:39

Editing PKGBUILD to build with camlp4 instead of camlp5-transitional solved the problem.

anastas commented on 2015-06-10 16:52

I'm getting the following error when attempting to install:

COQC theories/FSets/FMapAVL.v recipe for target 'theories/FSets/FMapAVL.vo' failed
make[1]: *** [theories/FSets/FMapAVL.vo] Killed
make[1]: *** Deleting file 'theories/FSets/FMapAVL.vo'
make[1]: *** [theories/FSets/FMapAVL.vo] Deleting file 'theories/FSets/FMapAVL.glob'
make[1]: Leaving directory '/tmp/packerbuild-1000/coq/coq/src/coq-8.4pl6'
Makefile:139: recipe for target 'world' failed
make: *** [world] Error 2
==> ERROR: A failure occurred in build().
The build failed.

anastas commented on 2015-06-10 16:50

Compilation error:

COQC theories/FSets/FMapAVL.v recipe for target 'theories/FSets/FMapAVL.vo' failed
make[1]: *** [theories/FSets/FMapAVL.vo] Killed
make[1]: *** Deleting file 'theories/FSets/FMapAVL.vo'
make[1]: *** [theories/FSets/FMapAVL.vo] Deleting file 'theories/FSets/FMapAVL.glob'
make[1]: Leaving directory '/tmp/packerbuild-1000/coq/coq/src/coq-8.4pl6'
Makefile:139: recipe for target 'world' failed
make: *** [world] Error 2
==> ERROR: A failure occurred in build().
The build failed.

zorun commented on 2015-01-29 14:57

Thanks, updated with your PKGBUILD!

Btw, I'm aware that coq 8.5 is out, but it's still a beta release. If you want coq 8.5, just create a new package coq-beta or something.

wilbowma commented on 2015-01-15 19:09

FWIW, if camlp4 is giving you trouble, Coq builds fine with camlp5-transitional. It is also flagged out of date, but hopefully will be updated soon.

Building Coq with camlp5-transitional seems necessary for ssreflect, anyway, so this might kill two birds with one change.

A modified PKDBUILD to use camlp5-transitional:

rata commented on 2014-12-25 07:06

I hope someone adopts the camlp4 package in extra and brings it up-to-date. I don't really want to make my own package and maintain myself.

zorun commented on 2014-12-25 01:21

Compiling camlp4 with the latest upstream release (4.02.1+1) fixes coq. The camlp4 package in [extra] is already flagged out-of-date, but is unfortunately also orphaned:

zorun commented on 2014-12-25 01:09

Indeed, weird. It seems more like an issue between ocaml and camlp4, though. There is a newer version of camlp4 available upstream (4.02.1+1), it might work better than the current one in [extra] (4.02.0+1).

rata commented on 2014-12-25 00:27

Compilation error:
CAMLP4O ide/coqide_main.ml4
"ocamlc.opt" -rectypes -c -I "+camlp4" -pp 'camlp4orf -impl' -impl tools/compat5.mlp
File "tools/compat5.mlp", line 1:
Error: The files /usr/lib/ocaml/pervasives.cmi
and /usr/lib/ocaml/camlp4/Camlp4.cmi make inconsistent assumptions
over interface Pervasives recipe for target 'tools/compat5.cmo' failed

zorun commented on 2014-11-20 11:03

Could you confirm that the coqide segfault is gone with the new version? (8.4pl5)

surfmaths commented on 2014-10-01 11:07


It is kind of functionnal, however coqide segfault when I try to copy/paste (either with the menu, or with the shortcut). Do you experience the same problem?

I'm not sure if it is related to my computer, to archlinux or coqide itself.
I should try a debug version (but it takes a while to compile...).

zorun commented on 2014-09-17 14:38

I've included a patch that fixes the compilation issue.

zorun commented on 2014-09-16 21:55

Thanks, OCaml 4.02.0 apparently split camlp4 into a different package, I've updated the dependencies accordingly.

As for the compilation error, it also seems to be related to OCaml 4.02.0. From the release notes [1]: "* Alternative syntax for string literals {id|...|id} (can break comments)"

The trunk version of coq apparently compiles without issue with OCaml 4.02.0.


surfmaths commented on 2014-09-16 12:20

Does not build:

OCAMLC kernel/
File "kernel/", line 229, characters 0-2:
Error: This comment contains an unterminated string literal
File "kernel/", line 229, characters 17-20:
Error: String literal begins here recipe for target 'kernel/univ.cmo' failed

surfmaths commented on 2014-09-16 12:16

Ah, it is simply a missing dependency: camlp4

surfmaths commented on 2014-09-16 12:06

Hello, 'coq' does not configure on my computer:

You have GNU Make 4.0. Good!
You have Objective-Caml 4.02.0. Good!
No Camlp4 installation found.
Configuration script failed!

'camlp4' is not found anywhere in my path. Closest one is 'safe_camlp4'.
'/usr/lib/ocaml/camlp4' might be a candidate too.

nesreka commented on 2014-06-13 07:37


8.4pl4 is out. Would it be possible to update the package?

zorun commented on 2014-05-13 08:32

Works for me:

lrwxrwxrwx root/root 0 2014-05-10 13:00 usr/bin/coqide -> coqide.opt
-rwxr-xr-x root/root 3607168 2014-05-10 13:01 usr/bin/coqide.opt

Maybe a missing dependency? Could you paste me the very beginning of the compilation? (up to "If anything in the above is wrong, please restart './configure'.")

szabba commented on 2014-05-10 10:33

It didn't build coqide for me. Any hints on what might be wrong?

zorun commented on 2014-01-02 18:16

Updated to 8.4pl3

zorun commented on 2013-10-26 12:15

Updated, thanks.

starrify commented on 2013-10-25 11:18

Please add a patch to the file `configure` as a quick fix for `make` version greater than 3.81. I believe this is a bug of `coq` and someone has reported this on its bugzilla: however it has been months and still no ofifcial fix.

A sample patch:
--- coq-8.4pl2/configure 2013-04-04 21:13:27.000000000 +0800
+++ coq-8.4pl2/ 2013-10-25 19:14:30.907501146 +0800
@@ -337,6 +337,8 @@
if [ "$MAKEVERSIONMAJOR" -eq 3 -a "$MAKEVERSIONMINOR" -ge 81 ]; then
echo "You have GNU Make $MAKEVERSION. Good!"
+ elif [ "$MAKEVERSIONMAJOR" -gt 3 ]; then
+ echo "You have GNU Make $MAKEVERSION. Good!"
#Extra support for local installation of make 3.81

starrify commented on 2013-10-25 10:47

Please add a patch to the file `configure` as a quick fix for `make` version greater than 3.81. I believe this is a bug of `coq` and someone has reported this on its bugzilla: however it has been months and still no ofifcial fix.

[pengyu@GLaDOS coq-8.4pl2]$ diff configure configure.old
< if [ "$MAKEVERSION" = "GNU Make 3.81" ]; then OK="yes";
< elif [ "$MAKEVERSION" > "GNU Make 3.81" ]; then OK="yes"; fi
> if [ "$MAKEVERSION" = "GNU Make 3.81" ]; then OK="yes"; fi

zorun commented on 2013-06-05 07:24

Thanks, the issue was only because ocaml-findlib is missing in your case (lablgtk2 presence is not auto-detected).

I've added ocaml-findlib as a makedep. I've also removed the dependency on camlp5-transitional, as coq is happy with the camlp4 version bundled with Ocaml.

Anonymous comment on 2013-06-03 14:45

I just installed this package and was not able to find `coqide`. After a quick look into the configure file, I realized that coqide must mentioned explicitly in the ./configure call. The second observation is that to find a ocaml dependency the configure scripts needs the package ocaml-finderlib.

In short: I suggest to add ocaml-finderlib as a build dependency and call ./configure with the additional flag `-coqide byte`.

zorun commented on 2013-05-13 07:23

Updated to 8.4pl2, and removed the documentation.

I've also uploaded two new coq packages:
- `coq-doc`, shipping the HTML documentation;
- `coq-nox`, that does not ship coqide, and thus does not need lablgtk. Otherwise, it's the same package as this one.

The proper way to go would be a split PKGBUILD, so that we could create an headless package `coq-core` and a separate `coqide`. However, it does not make sense in the context of the AUR (i.e. you would need *all* the dependencies to build the packages, which defeats the whole purpose of this change).

Anonymous comment on 2012-12-28 03:44

Why is the dep tree for lablgtk2 so big?
All I want is coq, not udisk or samba file sharing services and things..
Is that really necessary?
Sorry if this is not the correct place to ask?

zorun commented on 2012-11-05 10:03

@justmao945 sort of

lablgtk2 in [extra] has been rebuilt, please upgrade to 2.16.0-2.

Anonymous comment on 2012-11-02 09:46

@zorun @zaichenkov
Great, it works after rebuilding the lablgtk2 package~~ That's an ABI compatibility issue? =w=

SebRmv commented on 2012-11-01 11:41

Is it possible to build coq-ide just by itself (assuming coq is already installed)?
If yes, this could be an idea to have a separate package for coq-ide, as it is an optional tool. Or make the lablgtk2 dependency optional if possible, since it is just needed to build coq-ide. For instance:

optdepends=('lablgtk2: to build coq-ide')
makedepends=('camlp5-transitional' 'netpbm' 'hevea' 'texlive-latexextra' 'texlive-fontsextra' 'texlive-pictures')

Is there something such as optmakedepends? This would be more appropriate.

SebRmv commented on 2012-11-01 11:04

Is it possible to build coq-ide just by itself (assuming coq is already installed)?
If yes, this could be an idea to have a separate package for coq-ide, as it is an optional tool. Or make the lablgtk2 dependency optional if possible, since it is just needed to build coq-ide.

SebRmv commented on 2012-11-01 11:04

Is it possible to build coq-ide just itself (assuming coq is already installed)?
If yes, this could be an idea to have a separate package for coq-ide, as it is an optional tool. Or make the lablgtk2 dependency optional if possible, since it is just needed to build coq-ide.

zorun commented on 2012-11-01 08:11

This package builds fine with:

- `ocaml` 4.00.1-1
- `camlp5-transitional` 6.07.1-1
- a rebuilt version of `lablgtk2` 2.16.0

I've requested a rebuild of `lablgtk2` from [extra], you can either wait for the update or build it yourself.

zorun commented on 2012-11-01 07:19

The `lablgtk2` package probably needs to be rebuilt against OCaml.

Anonymous comment on 2012-10-31 21:58

justmao945, I have exactly the same error here.
Versions of the packages are as you have.
Probably this is a compatibility issue.

Anonymous comment on 2012-10-31 12:42

How to fix this error?
File "ide/coqide_main.ml4", line 1:
Files /usr/lib/ocaml/lablgtk2/lablgtk.cma(Gpointer)
and /usr/lib/ocaml/stdlib.cma(StdLabels)
make inconsistent assumptions over interface StdLabels

lablgtk2 2.16.0-1
ocaml 4.00.1-1

Anonymous comment on 2012-10-29 18:32

Tried to install the package just after "pacman -Syu" command.
camlp5-transitional-6.07-1 is installed.
Any other ideas?

zorun commented on 2012-10-29 17:51

Are you sure to have an up-to-date system? Which version of camlp5-transitional (from AUR) do you have?

Anonymous comment on 2012-10-29 14:08

Can you help me to fix the following error?
I build the package on x86_64 platform, 3.6.3-1 kernel, latest packages installed (OCaml version 4.00.1).

zorun commented on 2012-09-19 15:34

Adopted and updated with the patch from acieroid (thanks).

Note that a lot of the (long) build time is spent on documentation. Also, the resulting package is quite big once installed (145 MiB for the libs, 21 MiB for the binaries, and 57 MiB for the doc).

I'll probably split it into separate packages at some point (for instance, “coq” and “coq-doc”).

acieroid commented on 2012-09-16 18:51

Quick and easy fix for building with OCaml 4.00:

xyproto commented on 2012-08-01 09:08

Anybody else get this error?

Anonymous comment on 2012-06-28 06:33

Ok, fixed it. Sorry, I should have checked for more latex deps. Thanks again.

kamahl commented on 2012-06-27 23:57

There is a simillar error with comment.sty file.
! LaTeX Error: File `comment.sty' not found. (file Reference-Manual.tex)
It's in the package texlive-latexextra - it should be added as a make dependency too.

Anonymous comment on 2012-06-26 17:42

Thanks! I've fixed it.

pherms commented on 2012-06-26 16:38

Compilation fails for me while making the docs with

! LaTeX Error: File `epic.sty' not found. (file RecTutorial.tex)

The missing Latex package is in texlive-pictures, so I think this should be added to makedepends.

td123 commented on 2012-04-13 01:09

Due to lack of time, and trying to reorganize my focus w/ archlinux, and given that coq is not something I use anymore, I decided to let it go after a long time of maintaining it.

I know it sucks, but I already gave the other tu's a chance to adopt it and I would rather see a package have a maintainer in the aur rather than leaving it as an orphan in community.

Sorry for any inconviences this causes people.

pherms commented on 2012-04-12 08:06

Can I ask why this was removed from [community]?

pherms commented on 2010-12-08 19:56

I'm sorry, something must have changed. When I tested it, makepkg didn't fail if netpbm wasn't installed but just didn't build the docs.
Now I added it to makedepends, actually coq is not that useful without its docs,

giniu commented on 2010-12-08 13:04

The pkgbuild failed for me because I didn't had netpbm (failed because it requires pngtopnm and pnmtops)

pherms commented on 2010-05-19 12:36

I avoided to add those to makedepends as they're only needed to build the docs. I changed the script such that making the package doesn't fail if hevea and tex aren't installed, in that case the docs just wouldn't be made.
"Pause to inspect changes" just waits 5 seconds for you to decide if you rather want to abort the making of the package (the 4 lines above just print the changes since your previous build). I usually abort rebuilding the package if nothing important changed since my last build. (you can safely delete those lines if you want)

beroal commented on 2010-05-18 11:12

Thanks for the package!
Revision 13011 requires
makedepends=(... 'hevea' 'texlive-bin' 'texlive-core' 'texlive-latexextra')
Can you tell me please what is "Pause to inspect changes... " exactly doing?
Do not build with parallel make.