coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Install Coq from OPAM page is gone

From: Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>
To: Théo Zimmermann <theo.zimmi AT gmail.com>, "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Install Coq from OPAM page is gone
Date: Wed, 20 Feb 2019 23:30:02 +0000
Accept-language: en-CA, en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=fdhzs2010 AT hotmail.com; spf=Pass smtp.mailfrom=fdhzs2010 AT hotmail.com; spf=Pass smtp.helo=postmaster AT NAM01-BN3-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:2jMeaRzovqOkxQXXCy+O+j09IxM/srCxBDY+r6Qd2usWIJqq85mqBkHD//Il1AaPAd2Lraocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HQbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDwULs6Wymt771zRRHolikJKiI5/m/UhMx+jq1UvB2uqgdlzILIfI2YLuZycr/Acd4cWGFPXtxRVytEAo6ka4UAFfEBPeFer4LgvlcBrhu+BQ6qBOPg1zRGm3/20rM80+QuCA3NwQ4uH88Tu3nTotX6KacSUOGuzKXW0TnPcu9a1Cz96IjPbhAhpOuDXbN0ccbL1UYvEAbFg0yWpIf4MT2V0eENvHKa7+pmTe+vimgnqxtwoje13MsshJPJi4QIwV7H7SV02Ik4KcGiREN/f9KoCodcuzuaOodqWs8iTX9ntSUmxrADvJO0ZzQFx4gkyhPacPOLb4mF7xDmWeufOjh3nnJodbexhxuz8kWtyOvxXdSu3llQtCpKiNzMu2gN1xPN7siHTeNw8F+91DiIywzf9/hILF0sm6fVMpIhxaU/mYQJvUTEAy/2hF75jKiLdkUi5+ek8fznYq/hpp+AKYB7lh3+MqUpmsy5G+g4NRUOX3Sf+eS7073j/lf1T6lNjv0ziqXZsZbaKtoHpqOhDAJZzpwv5hKhAzu8zNgUh3kKIE5ddBKClYfpOlXOIP7iDfe4hlShiDlryO3GPrzgGZXBMGTPnKr9cbtm605czxYzzdVF6JJVDrENOu78Wkj0tNDAFB82LxS0w/r7CNV6zo4RRWWPAraAPKzOtV+I+/kgLvKXZI4VvTb9M+Iq6+TvjX8/g18dfLOm0YEZaHCiTbxaJBClYfvrteUAFGIHpA83Suqi3EGCXDkVdXe3WqMU6TQyCYbgBoDGEMTlyreGxWKwGoBcTmFAEFGFV3nyPc3QUPAVLSmWP8VJkzoeVLHnRZV3hj+0swqv6bN8Keycvx8YspTsnON16uvc0FkS6HQgAcidwXrXFzgstmMPWzo/3aQ5qkt4nATQmZNkiuBVQIQAr8hCVR03YMaFnr5KTuvqUweERe+nDVOvQ9GoGzY0F4ljw9gSZk98H5OpiRWRhnP2UY9QrKSCAdkPyoyZx2L4fp0vy3Ha0aAgix8tRc4dbTT71J46zBDaAsvyq2vcl6uucvhDjgjk0T/aiECo5wRfWgM2VrjZV3cCYEeQtc7++k7JU76pD/IgLxdFzsmBbKBNb4+wgA==

thx, the redirection is working already.

note that even google failed to grab the new url!

Sincerely Yours,

Jason Hu

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Théo Zimmermann <theo.zimmi AT gmail.com>
Sent: February 20, 2019 6:23 PM
To: Coq Club
Subject: Re: [Coq-Club] Install Coq from OPAM page is gone

Hi Jason,

Indeed, this page has been moved (to https://coq.inria.fr/opam-using.html). The bug tracker of either the main Coq repository / the Coq opam archive / the Coq website would all be places that are OK to report this. It turns out that we were already aware of this problem (from day one actually) and a fix (adding a redirection) has been ready for a while but forgotten before being merged. I just did merge it so hopefully the redirection should be set up in a few minutes. If it isn't, feel free to reply here or open a bug report.

Théo

Le mer. 20 févr. 2019 à 23:23, Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com> a écrit :

Hi,

the usual page showing instructions to install coq from opam is gone: https://coq.inria.fr/opam/www/using.html

Installing Coq via OPAM | The Coq Proof Assistant

What is OPAM. OPAM is the package manager for the OCaml programming language, the language in which Coq is implemented. Instructions on how to install OPAM itself are available on the OPAM website. By following the instructions on this web page one installs the last stable version of Coq and all additional packages in the directory ~/opam-coq.8.8.2. ...

coq.inria.fr

Is there any place I can report this?

Thanks,

Jason

[Coq-Club] Install Coq from OPAM page is gone, Jason -Zhong Sheng- Hu, 02/20/2019
- Re: [Coq-Club] Install Coq from OPAM page is gone, Théo Zimmermann, 02/21/2019
  - Re: [Coq-Club] Install Coq from OPAM page is gone, Jason -Zhong Sheng- Hu, 02/21/2019