Package Details: coq 8.5pl1-1

Git Clone URL: https://aur.archlinux.org/coq.git (read-only)
Package Base: coq
Description: Formal proof management system. Full version that includes CoqIDE.
Upstream URL: http://coq.inria.fr/
Licenses: GPL
Submitter: td123
Maintainer: zorun
Last Packager: zorun
Votes: 55
Popularity: 0.949823
First Submitted: 2012-04-09 20:45
Last Updated: 2016-05-11 19:33

Latest Comments

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
/usr/lib/ocaml/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

@zorun

Thank you for your help.
Here is full log of "yaourt -S coq --noconfirm".
http://pastebin.com/8pPfBWgH

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 http://pastebin.com/1QsAm3Cf .

EDIT:
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:

https://bugs.archlinux.org/task/42748
http://caml.inria.fr/mantis/view.php?id=6693
https://bugzilla.redhat.com/show_bug.cgi?id=1195025

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: http://paste.aliens-lyon.fr/u3v
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/analyze.ml
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.

[1] https://github.com/nana4gonta/gentoo-prefix-overlay/blob/master/sci-mathematics/coq/files/coqide.desktop

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):

https://gist.github.com/atondwal/bd785ca9c32e2c594f23

All comments