The Coq mailing list

[Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>]

ok I actually sent it to coqclub... fat fingers...

Thanks,

Jason Hu

https://hustmphrrr.github.io/

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>
Sent: January 13, 2020 9:38 PM
To: coq-club AT inria.fr <coq-club AT inria.fr>
Subject: Re: [Coq-Club] installing new version of coq

 

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