The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

IMHO you will probably end up recompiling everything anyway because you may have different versions of external dependencies (eg gcc and its libs) in the new machine.

P

Le sam. 23 janv. 2021 à 06:26, Lasse Blaauwbroek <lasse AT blaauwbroek.eu> a écrit :

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