The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

See https://github.com/coq/www/pull/138

Le mar. 14 janv. 2020 à 09:11, 
<Rajeev.Gore AT anu.edu.au>
 a écrit :
>
>
> Hi Theo,
>
> my only request would be to somehow build-in a workaround for the "m4 not 
> found" problem.
>
> I did some searching when I originally ran into this and it appears to also 
> plague windows installations of Coq. It took some time
> for the penny to drop that I could just install m4 myself, but a (more) 
> naive user might not think of this.
>
> best wishes,
> raj
>
> On 14 January 2020 Théo Zimmermann 
> (theo.zimmi AT gmail.com)
>  writes:
> > Hi,
> >
> > Glad to help! Feel free to propose some changes to the file
> > https://github.com/coq/www/blob/master/pages/opam-using.html by opening a
> > pull request.
> >
> > Cheers,
> > Théo
> >
> > Le mar. 14 janv. 2020 à 06:55, Donald Leung 
> > <i.donaldl AT me.com>
> >  a écrit :
> >
> > > > Just one piece of advice: please tell novices such as I that the make
> > > sometimes takes quite a bit of time. I thought that it had
> > > hung because it did not do anything for about ten minutes, but just as I
> > > was typing an email to you to say so, it finished :)
> > >
> > > You probably need to develop a bit of patience, then ;-) From my
> > > experience, a build time of >= 10 minutes isn’t all that uncommon - for
> > > example, VST ( https://vst.cs.princeton.edu ) normally takes around 70
> > > minutes to build.
> > >
> > > Rajeev.Gore AT anu.edu.au於2020年1月14日
> > >  09:59寫道：
> > >
> > >
> > > Hi Theo, Laurent and Benoit,
> > >
> > > here is what I did.
> > >
> > > add-apt-repository ppa:avsm/ppa
> > > apt update
> > > apt install opam
> > > opam init
> > > eval $(opam env)
> > >
> > > All went well so far and opam --version gives me 2.0.4.
> > >
> > > I was not brave enough to try to switch ocaml compiler so I left it as 
> > > it
> > > was: ocaml --version gives me
> > > The Ocaml toplevel, version 4.05.0
> > >
> > > Then I went to https://coq.inria.fr/opam-using.html and tried
> > > opam pin add coq 8.10.2
> > >
> > > But it complained about not finding m4 so I just did a sudo apt install
> > > m4, which thankfully worked.
> > >
> > > Then the following all worked:
> > > opam pin add coq 8.10.2
> > > opam repo add coq-released https://coq.inria.fr/opam/released
> > > opam install coq-coqprime
> > >
> > > Just one piece of advice: please tell novices such as I that the make
> > > sometimes takes quite a bit of time. I thought that it had
> > > hung because it did not do anything for about ten minutes, but just as I
> > > was typing an email to you to say so, it finished :)
> > >
> > > Thank you for all of your prompt help!
> > >
> > > best wishes,
> > > raj
> > > --
> > > Rajeev Gore'
> > > Professor, Logic and Computation Group, and
> > > Associate Director of Research,
> > > Research School of Computer Science
> > > ANU College of Engineering and Computer Science
> > > The Australian National University
> > > Canberra ACT 2601
> > > Tel:   +61-2-61 25 86 03
> > > Fax:   +61-2-61 25 86 51
> > > Email: 
> > > Rajeev.Gore AT anu.edu.au
> > >  
> > > <Rajeev.Gore AT anu.edu.au>
> > > Web:   http://arp.anu.edu.au/~rpg
> > > ANU CRICOS Provider Number - 00120C
> > >
> > >
> > >
> >    Hi,
> >    Glad to help! Feel free to propose some changes to the
> >    file [1]https://github.com/coq/www/blob/master/pages/opam-using.html by
> >    opening a pull request.
> >    Cheers,
> >    Tho
> >
> >    Le mar. 14 janv. 2020 06:55, Donald Leung 
> > <[2]i.donaldl AT me.com>
> >  a
> >    crit :
> >
> >    > Just one piece of advice: please tell novices such as I that the make
> >    sometimes takes quite a bit of time. I thought that it had
> >    hung because it did not do anything for about ten minutes, but just as
> >    I was typing an email to you to say so, it finished :)
> >    You probably need to develop a bit of patience, then ;-) From my
> >    experience, a build time of >= 10 minutes isn t all that uncommon - for
> >    example, VST ( [3]https://vst.cs.princeton.edu ) normally takes around
> >    70 minutes to build.
> >
> >    
> > [4]Rajeev.Gore AT anu.edu.au
> >  2020 1 14 09:59
> >
> >    Hi Theo, Laurent and Benoit,
> >    here is what I did.
> >    add-apt-repository ppa:avsm/ppa
> >    apt update
> >    apt install opam
> >    opam init
> >    eval $(opam env)
> >    All went well so far and opam --version gives me 2.0.4.
> >    I was not brave enough to try to switch ocaml compiler so I left it as
> >    it was: ocaml --version gives me
> >    The Ocaml toplevel, version 4.05.0
> >    Then I went to [5]https://coq.inria.fr/opam-using.html and tried
> >    opam pin add coq 8.10.2
> >    But it complained about not finding m4 so I just did a sudo apt install
> >    m4, which thankfully worked.
> >    Then the following all worked:
> >    opam pin add coq 8.10.2
> >    opam repo add coq-released [6]https://coq.inria.fr/opam/released
> >    opam install coq-coqprime
> >    Just one piece of advice: please tell novices such as I that the make
> >    sometimes takes quite a bit of time. I thought that it had
> >    hung because it did not do anything for about ten minutes, but just as
> >    I was typing an email to you to say so, it finished :)
> >    Thank you for all of your prompt help!
> >    best wishes,
> >    raj
> >    --
> >    Rajeev Gore'
> >    Professor, Logic and Computation Group, and
> >    Associate Director of Research,
> >    Research School of Computer Science
> >    ANU College of Engineering and Computer Science
> >    The Australian National University
> >    Canberra ACT 2601
> >    Tel:   +61-2-61 25 86 03
> >    Fax:   +61-2-61 25 86 51
> >    [7]Email: 
> > Rajeev.Gore AT anu.edu.au
> >    Web:   [8]http://arp.anu.edu.au/~rpg
> >    ANU CRICOS Provider Number - 00120C
> >
> > References
> >
> >    1. https://github.com/coq/www/blob/master/pages/opam-using.html
> >    2. 
> > mailto:i.donaldl AT me.com
> >    3. https://vst.cs.princeton.edu/
> >    4. 
> > mailto:Rajeev.Gore AT anu.edu.au
> >    5. https://coq.inria.fr/opam-using.html
> >    6. https://coq.inria.fr/opam/released
> >    7. 
> > mailto:Rajeev.Gore AT anu.edu.au
> >    8. http://arp.anu.edu.au/~rpg
>
>
> --
> Rajeev Gore'
> Professor, Logic and Computation Group, and
> Associate Director of Research,
> Research School of Computer Science
> ANU College of Engineering and Computer Science
> The Australian National University
> Canberra ACT 2601
> Tel:   +61-2-61 25 86 03
> Fax:   +61-2-61 25 86 51
> Email: 
> Rajeev.Gore AT anu.edu.au
> Web:   http://arp.anu.edu.au/~rpg
> ANU CRICOS Provider Number - 00120C
>