The Coq mailing list

[Donald Leung <i.donaldl AT me.com>]

Hi Jeremy,

Just out of interest, how long did you wait for the `opam init` command? Also 
note that Coq 8.10.2 can only be compiled with OCaml >= 4.05.0 so you would 
not be able to install Coq 8.10.2 even if your OCaml 4.02.3 installation were 
successful. Any reason why you would need to use OCaml 4.02.3 in particular?

Cheers,
Donald

> Jeremy Dawson 
> <Jeremy.Dawson AT anu.edu.au>於2020年1月14日
>  11:53寫道：
> 
> Hi, thanks,
> 
> I found how the opam site gives the option to simply download the 
> executable, so I did that, so now using opam 2.0.5
> and doing opam init -n --compiler=ocaml-base-compiler.4.02.3
> I still get that it hangs at the point
> Processing: [default: http]
> 
> Thanks
> 
> Jeremy
> 
> On 14/1/20 1:38 pm, Jason -Zhong Sheng- Hu wrote:
>> 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
>>