Package Details: coq 8.5pl3-1

Git Clone URL: (read-only)
Package Base: coq
Description: Formal proof management system. Full version that includes CoqIDE.
Upstream URL:
Licenses: GPL
Submitter: td123
Maintainer: zorun
Last Packager: zorun
Votes: 58
Popularity: 0.942810
First Submitted: 2012-04-09 20:45
Last Updated: 2016-12-01 22:26

Latest Comments

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.

All comments