# I cannot build Bignums

**URL:** <https://discourse.rocq-prover.org/t/i-cannot-build-bignums/363>\
**Category:** Using Rocq\
**Created:** [July 24, 2019, 11:05am UTC](https://discourse.rocq-prover.org/t/i-cannot-build-bignums/363 "2019-07-24T11:05:46Z")\
**Posts on this page:** 4\
**Page:** 1

<div class="post-metadata">

**Author:** ![kindaro](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/kindaro/32/146_2.png) [@kindaro](https://discourse.rocq-prover.org/u/kindaro)\
**Post date:** [July 24, 2019, 11:05am UTC](https://discourse.rocq-prover.org/t/i-cannot-build-bignums/363/1 "2019-07-24T11:05:46Z")

</div>

Hello!

I cloned [this repository](https://github.com/coq/bignums), 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
```

---

<div class="post-metadata">

**Author:** ![Lyxia](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lyxia/32/75_2.png) [@Lyxia](https://discourse.rocq-prover.org/u/Lyxia)\
**Post date:** [July 24, 2019, 11:23am UTC](https://discourse.rocq-prover.org/t/i-cannot-build-bignums/363/2 "2019-07-24T11:23:55Z")

</div>

Bignum on the `master` branch requires Coq 8.10. Try a different version, such as the one tagged `V8.9.0` (see [releases](https://github.com/coq/bignums/releases)).

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

---

<div class="post-metadata">

**Author:** ![Lyxia](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lyxia/32/75_2.png) [@Lyxia](https://discourse.rocq-prover.org/u/Lyxia)\
**Post date:** [July 24, 2019, 11:25am UTC](https://discourse.rocq-prover.org/t/i-cannot-build-bignums/363/3 "2019-07-24T11:25:45Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![kindaro](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/kindaro/32/146_2.png) [@kindaro](https://discourse.rocq-prover.org/u/kindaro)\
**Post date:** [July 24, 2019, 3:14pm UTC](https://discourse.rocq-prover.org/t/i-cannot-build-bignums/363/4 "2019-07-24T15:14:04Z")

</div>

@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!