coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Théo Zimmermann <theo.zimmi AT gmail.com>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] problems installing coqprime
- Date: Tue, 14 Jan 2020 08:56:59 +0100
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=theo.zimmi AT gmail.com; spf=Pass smtp.mailfrom=theo.zimmi AT gmail.com; spf=None smtp.helo=postmaster AT mail-ua1-f53.google.com
- Ironport-phdr: 9a23:4D+zmB2W0lL9fJGssmDT+DRfVm0co7zxezQtwd8ZseIfL/ad9pjvdHbS+e9qxAeQG9mCsLQe1LOd6vm5EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCezbL9oMhm7rxjdusYLjYd/N6o61wfErGZPd+lK321jOEidnwz75se+/Z5j9zpftvc8/MNeUqv0Yro1Q6VAADspL2466svrtQLeTQSU/XsTTn8WkhtTDAfb6hzxQ4r8vTH7tup53ymaINH2QLUpUjms86tnVBnlgzocOjUn7G/YlNB/jKNDoBKguRN/xZLUYJqIP/Z6Z6/RYM8WSXZEUstXSidPAJ6zb5EXAuUOM+ZXrYnzqVUNoxWjGwejGPjixSVUinLsx6A2z/gtHAPA0Qc9H9wOqnPUrNDtOakMUeCy1q7Iwi3AYPNX3Df97ZbHcgokof6WW7Jwd9faxE4zFwPFkFqQrpbpPjKU1uQItmib7vFtVe2qi2E9qgFxpiKjydsrionMn48YzE3P+yt+wIYwP9K4SUh7bMalEJtWrSGaNpF5TtksQ2FyoCo10LsGuYOhcCcU1Zsn2gTTZOaac4SQ+hLjTueRITFki317ZLK/gBCy/VK+xeLhS8m4yFlKritZktnMq3ACzAbf5dSASvt45kuh2DCP1xrS6u5eO0w4j6TbK4Qnz7UtlZQTqVzOEjHqlEjylqObdUUp9vK25+j5fLnqvJ+ROoFyhwrjKKohgNa/Dv49MgUWX2iU5+C81Lr78E38WrpKj/k2nrDEsJ/AOMgXv6C5Dg9b34o55Ba/CDCm0NscnXYZNl5KZBWHj43xN1HPJvD3E+u/jkyynDt3w/3KJL7sD5XXInTdjrvtY6xx5k5SxQYryNBQ/ZNUCrUPIPLpXU/xscTVDgM5MwOqxObrEtR81oIbWWKKA6+UK6zSsVqS6eIuJ+mAfpMauDH4K/Q9/f7hkWc5mUMBfamuxZYYdHe4Hu1/L0qFZXrsn8wOHHwRvgs+SezqkEeNXSRSZ3a0RaI85ys0BJioDYfZFciRh+mq2z7zNZlLbCgSAVeVVHzsao+sWvEWaSvULNU3wRIeUr30d4+g0iactQr/xqBiJ+zSsnkEtZ/kksp04ujSvR43/D1wSc+a1jfeHClPgmoUSmpuj+hEqktnxwLGiPAg2qAKJZlo//pMFzwCG9vE1eUjUoL9XwvAepGCT1P0Goz7UwF0dco4xpo1W2g4G9imiUqejS+jArtQirXSQZJpqeTT2H/+I8s7wHHDhvF43gsWB/BXPGjjvZZRsg3aBorHiUKczv/4eqEV3SqL/2CGnzOD
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
Web: http://arp.anu.edu.au/~rpg
ANU CRICOS Provider Number - 00120C
- [Coq-Club] problems installing coqprime, Rajeev.Gore, 01/13/2020
- Re: [Coq-Club] problems installing coqprime, Benoît Viguier, 01/13/2020
- Re: [Coq-Club] problems installing coqprime, Rajeev.Gore, 01/13/2020
- Re: [Coq-Club] problems installing coqprime, Théo Zimmermann, 01/13/2020
- Re: [Coq-Club] problems installing coqprime, Rajeev.Gore, 01/14/2020
- Re: [Coq-Club] problems installing coqprime, Donald Leung, 01/14/2020
- Re: [Coq-Club] problems installing coqprime, Théo Zimmermann, 01/14/2020
- Re: [Coq-Club] problems installing coqprime, Rajeev.Gore, 01/14/2020
- Re: [Coq-Club] problems installing coqprime, Théo Zimmermann, 01/14/2020
- Re: [Coq-Club] problems installing coqprime, Théo Zimmermann, 01/14/2020
- Re: [Coq-Club] problems installing coqprime, Donald Leung, 01/14/2020
- Re: [Coq-Club] problems installing coqprime, Rajeev.Gore, 01/14/2020
- Re: [Coq-Club] problems installing coqprime, Théo Zimmermann, 01/13/2020
- Re: [Coq-Club] problems installing coqprime, Laurent Thery, 01/13/2020
- Re: [Coq-Club] problems installing coqprime, Benoît Viguier, 01/13/2020
- Re: [Coq-Club] problems installing coqprime, Rajeev.Gore, 01/13/2020
- Re: [Coq-Club] problems installing coqprime, Benoît Viguier, 01/13/2020
Archive powered by MHonArc 2.6.18.