The Coq mailing list

[Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>]

Hi Donald,

Probably around an hour.  Might have been a bit less.

Using OCaml 4.02.3 because it's what I get by doing
apt-get install ocaml

Cheers,

Jeremy

On 14/1/20 5:09 pm, Donald Leung wrote:
> 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
>>>
>