The Coq mailing list

[Lasse Blaauwbroek <lasse AT blaauwbroek.eu>]

Hi Jeremy,

This is likely because your username on the second computer is 
different. The files in .opam are generally path-dependent. So if you 
are going to copy your ~/.opam form one computer to another, you should 
make sure that all paths on those computers are the same.

I don't know why 'opam init' is creating a folder 'opam-coq.8.8.2' for you.

Regards,
Lasse

On 1/23/21 6:20 AM, Jeremy Dawson wrote:
> Hi,
>
> I'm trying to install Coq 8.11 using opam.
>
> I'm managed this fine on one computer.
>
> And I've copied the entire contents of ~/.opam from that computer to 
> the other one.
>
> but on the second one, when I run opam env
> it tells me to run opam init first (which seems odd since I've copied 
> the entire contents of ~/.opam from a computer where it all works
>
> So I do that, it creates a directory called opam-coq.8.8.2,
> and when I run opam env it comes up with lots of variable settings 
> involving /home/jeremy/opam-coq.8.8.2
>
> So, questions - where does it get the knowledge that I was previously 
> running opam-coq.8.8.2, why does it insist on setting me up to use 
> that, and how do I stop it?
>
> This is driving me nuts.
>
> Grateful for any help
>
> Jeremy