The Coq mailing list

[Benoît Viguier <beviguier AT gmail.com>]

Hi Raj,

The version of Ubuntu is not really helping. More importantly, which version of Coq are using?

I would suggest you try using this version (instead of the gforge.inria.fr one which we don't know when it was last updated):

https://github.com/thery/coqprime

It is available via Opam in the extra dev repo:

https://github.com/coq/opam-coq-archive/blob/master/extra-dev/packages/coq-coqprime/coq-coqprime.dev/opam

opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
      
      
opam install coq-coqprime

On 1/13/20 11:14 AM, Rajeev.Gore AT anu.edu.au wrote:

Hi all,

I am not sure whether this is the proper mailing list for asking this question, so apologies in advance if it is not.

I am trying to install coqprime. But at a certain point, I get the error below.

I am using ubuntu 18.04 and I tried to follow the instructions here http://coqprime.gforge.inria.fr/
under the heading "If your number has more than 100 decimal digits ".

A quick search on the "Unable to local library" showed some discussions about how one can replace -I with -R but I am afraid that
I am not competent to understand the details.

What am I doing wrong please?

raj

rajeevgore@rajeevgore-900X3C-900X3D-900X4C-900X4D:~/CoqPrime/coqprime$ make all
cd Tactic; make all
make[1]: Entering directory '/home/rajeevgore/CoqPrime/coqprime/Tactic'
coqc  -q  -I .   Tactic
make[1]: Leaving directory '/home/rajeevgore/CoqPrime/coqprime/Tactic'
cd N; make all
make[1]: Entering directory '/home/rajeevgore/CoqPrime/coqprime/N'
coqc  -q  -I . -I ../Tactic   NatAux
File "./NatAux.v", line 15, characters 15-21:
Error: Unable to locate library Tactic.
Makefile:112: recipe for target 'NatAux.vo' failed
make[1]: *** [NatAux.vo] Error 1
make[1]: Leaving directory '/home/rajeevgore/CoqPrime/coqprime/N'
Makefile:2: recipe for target 'all' failed
make: *** [all] Error 2