The Coq mailing list

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

Hi Raj,

On 1/13/20 11:48 AM, 
Rajeev.Gore AT anu.edu.au
 wrote:
> 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?

1. You are using an old version of Opam.

2. You did not do "opam init".

Have a look at here on how to upgrade/install opam 2.0 :
https://opam.ocaml.org/blog/opam-2-0-0/

Once opam is installed it is important to do `opam init` as this will
create the `.opam` repository:

```
opam init
eval $(opam env)
```

A good practice is to create a switch and install a more recent ocaml
compiler than the one proposed by Ubuntu.
You can see the one proposed by opam with:

```
opam switch list-available
```

You chose an ocaml-base-compiler from that list e.g.  4.08.1

```
opam switch create your-project-name 4.08.1
eval $(opam env)

```

After which you can do:
```
opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
opam update
```

This will add the repositories for the latest coq versions and coq packages.

From this point onward, you can do:
```
opam install coqide coq-coqprime
```

Good Luck.

> 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/
>