I cannot build Bignums

Using Coq
1

Hello!

I cloned this repository, went in and issued the command make.

What happened is an error:

% make
make -f Makefile.coq Makefile
make[1]: Entering directory '/srv/src/bignums'
make[1]: Nothing to be done for 'Makefile'.
make[1]: Leaving directory '/srv/src/bignums'
make -f Makefile.coq all
make[1]: Entering directory '/srv/src/bignums'
CAMLOPT -c -for-pack Bignums_syntax_plugin bignums_syntax.ml
findlib: [WARNING] cannot read directory /dev/null: Not a directory
File "bignums_syntax.ml", line 102, characters 22-26:
Error: Unbound constructor GInt
make[2]: *** [Makefile.coq:611: bignums_syntax.cmx] Error 2
make[1]: *** [Makefile.coq:327: all] Error 2
make[1]: Leaving directory '/srv/src/bignums'
make: *** [Makefile:2: all] Error 2

Do I need to install some dependencies first? How should I go about it?

I am on Linux. Here are the versions I use:

% ocaml --version
The OCaml toplevel, version 4.07.1
% coqc --version
The Coq Proof Assistant, version 8.9.1 (May 2019)
compiled on May 31 2019 15:34:51 with OCaml 4.07.1
% git describe --long
V8.8.0-18-g33ae5d5
2

Bignum on the master branch requires Coq 8.10. Try a different version, such as the one tagged V8.9.0 (see releases).

GInt is a new constructor for primitive ints added to Coq 8.10.

3

Oh wait nevermind, you’re already on V8.8.0… What does git status say?

EDIT: I misunderstood git describe and my original comment was correct.

4

@Lyxia I was actually on current master, which is after V8.10+beta1. It so happens that git describe by default considers only annotated tags, and apparently V8.8.0 is the last annotated tag in history.

V8.9.0 got built without any problems, so problem solved!