Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] problems installing coqprime

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] problems installing coqprime


Chronological Thread 
  • From: Donald Leung <i.donaldl AT me.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] problems installing coqprime
  • Date: Tue, 14 Jan 2020 13:54:25 +0800
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=i.donaldl AT me.com; spf=Pass smtp.mailfrom=i.donaldl AT me.com; spf=None smtp.helo=postmaster AT pv50p00im-tydg10021701.me.com
  • Ironport-phdr: 9a23:w78KVh+EcZ3EcP9uRHKM819IXTAuvvDOBiVQ1KB30+kcTK2v8tzYMVDF4r011RmVBN6dsa0dwLqI+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxhGiTanf79/Lgi6oQrSu8QXnIBvNrs/xhzVr3VSZu9Y33loJVWdnxb94se/4ptu+DlOtvwi6sBNT7z0c7w3QrJEAjsmNXs15NDwuhnYUQSP/HocXX4InRdOHgPI8Qv1Xpb1siv9q+p9xCyXNtD4QLwoRTiv6bpgRRn1gykFKjE56nnahMxsg61UvRyvqRJ/zZDWb4+WM/RzZbnScc8fRWdbXsZdSy5MD4WhZIUPFeoBOuNYopHzqVsJqxuxHw2sC/7ywTFOmHD2wKs60+s8GgzB3QwsBc8BsHPSrNrvMKcdTOS1wbLNzTrddf9ZxTD96I3Rfx0nvPqCU7Vwcc/LxkkuEQPIllSQqYr/PzOUzOsBqWab7/B4We21jW4ntht9rSayyccxkIXGnJ8Vxkjc9SVjwYY1I8G3R1BnYd6jFptcrT+VOJZrQs4kXmpmuz46x6UbtZO5ZiQHyJcqywTeZvCdc4WF7QrvWPuMLTtmnn5pZa+zihKo/US9yODxWNO43EtKoydLlNTHq2oD2AbJ6sedT/tw5keh1iiL1wDU8uxEOV40mKrHJ5453rI8ipsTsUHaEi/qmET5kaCWelg49uS09ejrf7frqoOBO4NujwHxLL4ildC4AeQ9KgQOXm6b9vqg1LD74EH0Qq9Gg/01n6XDsZ3WP8QWq6GhDw9QyIkj6hK/Dzm80NQfmHkKNFNFdAiagIjuPVHBOvT4Auq7g1m3lTdk2erKMaHmApXINnTDiqvufa5h605Azwo+1cxQ55VNCr0YPP3zXlLxu8fDAx8iMw20xv7nB89n2oMfX2KPGK6ZP7nIvV+G/OJ8a9WLMYQSoXP2L+Uvz//ol34w31EHLoez2p5CRHe+F/Bqa2GUfHzjyoMAV2sNuAM6QOjCjVDEWjlWMSXhF5kg7y02Xdr1RbzIQZqg1eTYgHWLW6ZOb2UDMWiiVG/yftXWXvpKYyWXcJc4z240EIO5Qopk7imA8Q/3z708d7jM5HBArcq71d0w+/zfmkhqrWYtUJzElWSACWpzmzFQHm5k7OVEuUV4j2y7/+19iv1cG8ZU4qMbVwp8PpnZnbV3

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





Archive powered by MHonArc 2.6.18.

Top of Page