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

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

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

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/compat.ml', 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
Makefile.build:920: 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().
Aborting...
The build failed.

anastas commented on 2015-06-10 16:50

Compilation error:

COQC theories/FSets/FMapAVL.v
Makefile.build:920: 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().
Aborting...
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.

bluephoenix47 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: http://sprunge.us/VcOb

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:

https://www.archlinux.org/packages/extra/x86_64/camlp4/

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
OCAMLDEP ide/coqide_main.ml
"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
Makefile.build:563: 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

Thanks!

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.

[1] https://sympa.inria.fr/sympa/arc/caml-list/2014-05/msg00116.html

surfmaths commented on 2014-09-16 12:20

Does not build:

OCAMLC kernel/univ.ml
File "kernel/univ.ml", line 229, characters 0-2:
Error: This comment contains an unterminated string literal
File "kernel/univ.ml", line 229, characters 17-20:
Error: String literal begins here
Makefile.build:853: 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

Hey,

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: https://coq.inria.fr/bugs/show_bug.cgi?id=3137 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/configure.new 2013-10-25 19:14:30.907501146 +0800
@@ -337,6 +337,8 @@
MAKEVERSIONMINOR=`echo $MAKEVERSION | cut -d. -f2`
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!"
else
OK="no"
#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: https://coq.inria.fr/bugs/show_bug.cgi?id=3137 however it has been months and still no ofifcial fix.

[pengyu@GLaDOS coq-8.4pl2]$ diff configure configure.old
346,347c346
< 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?
Cheers,
Edward
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:

depends=('ocaml')
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?
http://pastebin.com/Qnkx8SAm
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: http://paste.awesom.eu/KjY

xyproto commented on 2012-08-01 09:08

Anybody else get this error? http://ix.io/2Hf

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

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