The Coq mailing list

[Dan Krejsa <dan.krejsa AT gmail.com>]

Hi,

To answer my own question:  the AUR camlp5 package needed to be modified to build static libraries.  See the comment by jmnotin on 2013-12-17 at

https://aur.archlinux.org/packages/camlp5/

- Dan

On Sat, Feb 15, 2014 at 2:59 PM, Dan Krejsa <dan.krejsa AT gmail.com> wrote:

Hi,

I cloned the coq repository from git://scm.gforge.inria.fr/coq/coq.git and I am trying to build it on Arch Linux.  I'm running into an error in the linking step:

-------------
[dlkrejsa@shadow coq]$ make world
make --warn-undefined-variable --no-builtin-rules -f Makefile.build "world"
make[1]: Entering directory '/home/dlkrejsa/git/coq'
CHECK revision
COQMKTOP -o bin/coqtop
gcc: error: /usr/lib/ocaml/camlp5/gramlib.a: No such file or directory
File "caml_startup", line 1:
Error: Error during linking
Makefile.build:223: recipe for target 'bin/coqtop' failed
make[1]: *** [bin/coqtop] Error 2
make[1]: Leaving directory '/home/dlkrejsa/git/coq'
Makefile:138: recipe for target 'world' failed
make: *** [world] Error 2
-------------

(This is a rebuild, but the same error occurred on the first build attempt.)

/usr/lib/ocaml/camlp5/gramlib.a does not exist, but the directory exists and has files like this in it:

[dlkrejsa@shadow coq]$ ls /usr/lib/ocaml/camlp5/gramlib*
/usr/lib/ocaml/camlp5/gramlib.cma  /usr/lib/ocaml/camlp5/gramlib.cmxa

Any suggestions?

- Dan