Package Details: coq 8.5pl2-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: 56
Popularity: 0.657955
First Submitted: 2012-04-09 20:45
Last Updated: 2016-07-11 21:06

Latest Comments

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.


All comments