The Coq mailing list

[<Rajeev.Gore AT anu.edu.au>]

Hi Benoit,

I am using 8.6-5build1 (apparently :)

The reason I am using ubuntu 18.04 is because the webpage that I mentioned 
previously says it was tested on ubuntu 18.04.

I did the following:

 - I did a sudo apt install opam in my home directory (which appears to have 
worked)

 - I literally typed in "opam repo add coq-extra-dev 
https://coq.inria.fr/opam/extra-dev"; but it complained with

   # opam-version 1.2.2
   # os           linux
   File /home/rajeevgore/.opam/config does not exist

I did a quick search on ".opam/config does not exist" but could not find 
anything useful.

What am doing wrong please?

thanks,
raj

On 13 January 2020 Benoît Viguier 
(beviguier AT gmail.com)
 writes:
> 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
> >
> >
>    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):
> 
>    [1]https://github.com/thery/coqprime
> 
>    It is available via Opam in the extra dev repo:
> 
>    [2]https://github.com/coq/opam-coq-archive/blob/master/extra-dev/packag
>    es/coq-coqprime/coq-coqprime.dev/opam
>      *
> opam repo add coq-extra-dev [3]https://coq.inria.fr/opam/extra-dev
>      *
> opam install coq-coqprime
> 
>    On 1/13/20 11:14 AM, 
> [4]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 
> [5]http://co
> qprime.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 ho
> w 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
> 
> References
> 
>    1. https://github.com/thery/coqprime
>    2. 
> https://github.com/coq/opam-coq-archive/blob/master/extra-dev/packages/coq-coqprime/coq-coqprime.dev/opam
>    3. https://coq.inria.fr/opam/extra-dev
>    4. 
> mailto:Rajeev.Gore AT anu.edu.au
>    5. http://coqprime.gforge.inria.fr/


-- 
Rajeev Gore'             
Professor, Logic and Computation Group, and
Associate Director of Research,
Research School of Computer Science
ANU College of Engineering and Computer Science
The Australian National University
Canberra ACT 2601
Tel:   +61-2-61 25 86 03 
Fax:   +61-2-61 25 86 51  
Email: 
Rajeev.Gore AT anu.edu.au
Web:   http://arp.anu.edu.au/~rpg
ANU CRICOS Provider Number - 00120C