Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] installing new version of coq

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] installing new version of coq


Chronological Thread 
  • From: Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] installing new version of coq
  • Date: Tue, 14 Jan 2020 02:38:49 +0000
  • Accept-language: en-CA, en-US
  • Arc-authentication-results: i=1; mx.microsoft.com 1; spf=none; dmarc=none; dkim=none; 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=Crc97nTHfSq83HtJWFmpmoSycClFfmoJNfjifDQvnhU=; b=gAwKcRvf3yQ8wIIz5Xy7CzBsNgEGpcfDdUB5GJ7TRwBjtWollFB7Up/V/rP1g6dhpUCSoCP79Y5l7/pG6f171NtK7q1NdaV1AMhQAzAqmComDkBxWrqOHJtHtVFUnahYhr7sdi61Gr0Lhoxna9mIq9Bk5Kkz9i9VO8oL96FWO2xwvgRcLc6QSBZwskWp7yTWre1Tad5vH5FIRH95B4Dtrl1088ekuDVgbNiCTASSTHWuITGRx+8Sd+2DuIY3T2m+D3aUK/LYXLlrLjtq4YnUglrDQq4wVI1/nLR9HlK4ajI1k5LbHMe+kt+e/58W9M6LYOQwncYmmeV9bEJFgpurTA==
  • Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=j2cHc1aWPfSmU9yZpgu8mqypioO+freiNJWomhY7v9wFpM4zZ+zo6Mtd6Cr63cJj3YT1m/mh3m6X6Yxp9BO5Suqtbaa82XD5JrT1wzsitgVsJ22+a6ySL3rFeqYfvI6K7n9JQ50I8JscEYnB8AxxTxolAWX+qlXxV4ihygvHE53nEzxKiPtj0GHCmn7FHNvkfx9VOpFK0sRN/OAl9RloDnahpeQsSe0xH2OHGTQmr04NbA0MTfUhkKWkQGm5N6gwm5yXiK8TNcTgIFYn/+7Dl8PJsw5H7vrP0jNuVM62wtWr2H72FU4fPy3glbLS7su7Gt3oHbp+TqbFWprlXQG2Iw==
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=fdhzs2010 AT hotmail.com; spf=Pass smtp.mailfrom=fdhzs2010 AT hotmail.com; spf=Pass smtp.helo=postmaster AT NAM10-MW2-obe.outbound.protection.outlook.com
  • Ironport-phdr: 9a23:EPqLyhLQcguQm+Rn+9mcpTZWNBhigK39O0sv0rFitYgXKvz8rarrMEGX3/hxlliBBdydt6sfzbCJ6uu8BCQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTagb75+Ngu6oAfMusUZjoZvKrs6xwfUrHdPZ+lY335jK0iJnxb76Mew/Zpj/DpVtvk86cNOUrj0crohQ7BAAzsoL2465MvwtRneVgSP/WcTUn8XkhVTHQfI6gzxU4rrvSv7sup93zSaPdHzQLspVzmu87tnRRn1gygAKjA57XrXitRug61HvBKvqRt/w4vOb4GUMvp1Y6fRcNweSGZEWMtaSi5PDZ6mb4YXD+QPI/tWr5XzqVUNoxuxBxWjC+z0xzBSmnP6wbc33/g9HQ3Y2gErAtIAsG7TrNXwLKocVfq6zLLPzTXFcvhawDTy6IjPchAnrvGHQK9+ccrPxkkpGAPJl0ibp474PziI0ekNvXWU7+phVOK0lWIrtxx9riS0y8csjYnJmocVxUrF9SV92oo6Odq4SEtibNOiDZBeuSaaN45sTcMjRWFloCE6xaEctp6+eCgG0pMnxwTQa/CfcoiI5AjjVOeLLjtiinJlYqqzhxmz8Ui8yu38S9K73ExLripCitXMuXEN1wDT6siaUfR941yh1iiV1w/P7eFEJ1w0mrTdK5492LI/ip0TsUHFEyTrm0v2lLebe0o49uSy7+nrfK/qq5CCO4NuiAzzPbwimsKhDuk7LgQDWm2W+eqh27L//ED0RalFg/IqnabCtZ3XJtgUqrC9DgJQ0Ysv9wywAjG729oCh3YHNkhKeBefgojpJV7OJPf4AO+njVmwlzln2uzKMqTmDJrNMHTPibDhcq1j5EJGzwoz0Mxf6IlTCrEcJvL8R1X9tMTCDh8+Lwy73froCMl81oMZX2KDGKiZML7OsV+M4eIvJOqMaJUJtzb6Lvgp///ujXknll8BZaSk0ocbZGq8E/h4OUmUbmTgjs0DHGoFpgY+SfbliFyGUT5dfXayWKc86yk1CI27DYfCR5utjKKd0CumApFbfWBGCleQEXftbYqEWvMMZDiOLc9mlzwITaKhRJM51RGyqA/6zKJqIfbT+i0BrJ7syNx15/DImhwp7jx1D8Gd03mXQG1un2MIQSU23KFlrkBnxFeDy/swv/sNX9dU/rZCVhowHZ/a1e1zTd7oEEqVddCQDV2iX9+OADcrT9t3zcVYMGhnHND3rBnY2CziRo0VkLqETKc0/6TTmjDROo4pxXrGxrJ71wB+astIKWivh6o5/A/WUd2a236FnrqnIPxPlBXG832OmDbf5RAKYEtLSazAGEsnSA7TpNX96FnFSub1W7QgLg5IyMrEIaxPOISw0Qd2Acz7MdGbWFqf3n+qDE/TlLOLcI/jemFb1yLYWhBdzlIjuE2ePA17PR+P5mLTCDsySgDJSma1qaxblyn+SUU5iQaXc0dmyry5vAYPguCRQO8S2bRCvzo9rzJzHxC22NeEUtc=

I don't send to the whole coqclub because I am not certain about it. however, I kind of remember someone mentioned that later coq versions will no longer support opam 1. all repos for opam 1 will be put into a frozen state, and they will eventually be decommissioned. you might want to wait for a more official person for a confirmation.

Thanks,
Jason Hu
https://hustmphrrr.github.io/

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
Sent: January 13, 2020 9:28 PM
To: coq-club AT inria.fr <coq-club AT inria.fr>
Subject: [Coq-Club] installing new version of coq
 

Hi,

I'm trying to do this, following instructions at the website
https://coq.inria.fr/opam-using.html

jeremy@cecs-042179:~$ opam pin add coq 8.10.2
[ERROR] Package coq has no version 8.10.2

then I try a separate root (instructions near the bottom of the page)

export OPAMROOT=~/opam-coq.8.10.2 # no dot

opam init -n --compiler=ocaml-base-compiler.4.02.3

this gave

Cannot find
/home/users/jeremy/opam-coq.8.10.2/compilers/ocaml-base-compiler.4.02.3/ocaml-base-compiler.4.02.3/ocaml-base-compiler.4.02.3.comp:
ocaml-base-compiler.4.02.3 is not a valid compiler name.

OK, maybe this is because I'm running opam version 1.2.2
so I use the command that I have noted as having used a year ago

opam init -n --comp 4.02.3 # for opam 1
this puts a lot of stuff in the directory ~/opam-coq.8.10.2 but then hangs,
jeremy@cecs-042179:~/coq$ opam init -n --comp 4.02.3
Checking for available remotes: rsync and local, git, mercurial, darcs.
Perfect!

=-=- Fetching repository information
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-
[default] synchronized from https://opam.ocaml.org
[NOTE] The repository 'default' will be *permanently* redirected to
        https://opam.ocaml.org/1.2.2 (opam-version < "2.0~")
Processing: [default: http]

Obviously it hasn't done all it needs to do, because
opam pin add coq 8.10.2
[ERROR] Package coq has no version 8.10.2

Are there instructions available for using opam version 1?

(I tried installing opam, using instructions at
  https://opam.ocaml.org/doc/Install.html using the instruction
  sh <(curl -sL https://raw.githubusercontent.com/ocaml/opam/master/shell
/install.sh)
but (even when specifying to install in my own directory) required root
access)

Thanks,

Jeremy




Archive powered by MHonArc 2.6.18.

Top of Page