coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] installing coq using opam

From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] installing coq using opam
Date: Sat, 23 Jan 2021 16:20:48 +1100
Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=anu.edu.au; dmarc=pass action=none header.from=anu.edu.au; dkim=pass header.d=anu.edu.au; arc=none
Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=QqoLkUbZWp909/T9FN6L9jwopPkVze2JyDplS7vSNGE=; b=CHrsRzVSRrjXXfJpmkJex7A9wGpXOX3ORB8BJwJoUg2yl+2VfWQKJEcBefLrut7997+KtahwH7vmbUsRp8ntfh8oRazByWjcdU2SISf1UngI+3/0ar7iTvaR8UEQ+cROSfQVD5uWjXzYfOINRbSbXHM97tSSoeVGZfUo5dmXG8YAV8bYn01NxPG9EjjxnuSu79x7oOFdaHP1u4iu2i0TzVJcdrL74jnbxacIuQ2bCBiU29IsHUSGqZrZdjFXehGw2TENn3p32QiE4OswwkHlCFr8WQlJWhVadNowb8EUlJiFRminKCwIayoMR6wRcjGoy+KeerfZ+eIfMGhPI/wNRw==
Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=LBHKFcBpMKVITxn6TBnzSE6mqeC2OKULCaqARyE2d01wfyYE4pifpjv2xqSWMe429VYMzghzgcw1m0pF0H0e54gwgxuVjDgUVcvaNPyiKuamWyN25TxRUl258p6GFL6zQn9D1fGfNMQjNGYgVQK72K5ewEuCsDh8DfPeVDZGkXcP2UF5v3GK1HgvaqzFlR0sUATZa/iWGwerjzBLDwiMnXLM8KhhtMFXABUgkyiQEb5r4th9+De/KbjT+Z7A7nyN1qA+/5NJhS59ogB0sK7Mc5lFyM1Bw9/s95vsJrqwjbATZyn8XKGky3RImQuW5wn5NK0n1PZHEW92sfpsqpnITQ==
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.mailfrom=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-SY4-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:t4Ap6x/RTN0mtf9uRHKM819IXTAuvvDOBiVQ1KB21O8cTK2v8tzYMVDF4r011RmVBNSdsq0P1rqe8/i5HzBZvtDZ6DFKWacPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3wOgVvO+v6BJPZgdip2OCu4Z3TZBhDiCagbb9oIxi6sAHcutMLjYZgJao8yhjEqWZMd+hK2G9kP12ekwv+68uq4JJv7yFcsO89+sBdVqn3Y742RqFCAjQ8NGA16szrtR3dQgaK+3ARTGYYnAdWDgbc9B31UYv/vSX8tupmxSmVJtb2QqwuWTSj9KhkVhnlgzoaOjEj8WHXjstwjL9HoB+kuhdyzZLYbJ2TOfFjZa7WY88USnRdUcZQTyxBA52zb40TD+oaIO1Uq5Dxq0YSoReiAAWhAv7kxD1ViX/sxaA0zeQvHxzF0gIuEd0BrHvarNT6O6oJTeC4zrPFwSnfY/5Y2zrw7pXDfBA7ofGLWLJ9ac7fxlc1Fwzbi1WRqZHuMT2P2eUDqGib6OxgXv+ohmAjtQ5xuCagxsIsi4XTiIwa0F7F9T5+wIYzPtC3Ukh7YcO+HJROqi6aKpF6Tdk/Q2xxvisx17IJt4KhcicQ1JQn2wDQa+aBc4WQ/h/uWumfLzd3in55Zb6xiBi//0i8xuD/WcS531JHozRbntXRtH0AyxLd5tSbR/Z/+kqsxzKC2gTO5+xFIE06mqzWIIMizL4ojpcevljPEjXrlEnqjqKabFgo9vSq5uj9ZrjrqYeQOoBwhw3kL6gjmdGzDf4mPgQQXGWX4/mw2b3l8EbkWrtFlOc2nbPcsJ3CJcQUuKq5AwhN34s/5RmxEiuq3MkBkXcaLl1IdwuLj4/yNF7QOvz4Cuq/g0i3nzds2vDGOKDuDo/VLnjZl7fhYahy5FJAyAoyytBf4YhYCrYcIPLvXk/xs9vYDhwjPwOoxObnDc1x1oIYWW2RHq+UKKzfvUOS6u4yP+WBZpUZtCvhJ/Un/fLjiXA0lUcYfaaz3JsXbH64Hu5hI0WceXfihskOEX0UsQo7TO3mklOMXiRdZnapWKI84Co2B5igDYfeXIyinqGO3DqhEpJMe2BKEkqMHmvwd4WYR/cMbzqfLdNmkjwdTLSuV4sh1Qy1uwLh0LpmLu/U+jUCup751dh14ffTlRAo+jBuAcSdyTLFc2YhtWQRDxQywao39Ud60xKI1bVyq/1eD91aof1TBFQUL5nZms53Ed33S0rtd8iST1DuFverGzw0X5QdysAVZEBVEtO/yB3PwmyjHulGxPSwGJUo//eEjDDKLMFnxiODjfF51gh0co50LWSjw5VH2U3WDo/NnV+ekv/wJ60awWjA+HrFxHfc5RgFAj41ar3MWDUkXmWTrdn94R+dHZaTMux+dzBwlYuFIKYMbcD1h1JbQvulIM7Zf2+6h2a3A1CP26+Ia43pPW4a2XeEURRWo0Uo5X+DcDMGKGK5uWuHVm5nE0+pbk/xt+Bj+iu2

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

[Coq-Club] installing coq using opam, Jeremy Dawson, 01/23/2021
- Re: [Coq-Club] installing coq using opam, Lasse Blaauwbroek, 01/23/2021
  - Re: [Coq-Club] installing coq using opam, Pierre Courtieu, 01/23/2021