Package Details: coq 8.5pl3-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: https://coq.inria.fr/
Licenses: GPL
Submitter: td123
Maintainer: zorun
Last Packager: zorun
Votes: 57
Popularity: 0.397818
First Submitted: 2012-04-09 20:45
Last Updated: 2016-12-01 22:26

Latest Comments

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]: *** [Makefile.build:1043: 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

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

Regards

Simon

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
/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"?

All comments