coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Christian Doczkal <christian.doczkal AT ens-lyon.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Coq 8.8.2 is out!
- Date: Fri, 5 Oct 2018 11:46:59 +0200
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=christian.doczkal AT ens-lyon.fr; spf=Pass smtp.mailfrom=christian.doczkal AT ens-lyon.fr; spf=None smtp.helo=postmaster AT labbe.ens-lyon.fr
- Autocrypt: addr=christian.doczkal AT ens-lyon.fr; prefer-encrypt=mutual; keydata= xsFNBFIuNbYBEADAiZlQsnkRrXHOkaZ2mZIVNxzcBha3+HhZ8IhtxF4t5QXRNWFLtdwBuE8u D0GMB/Lacm/LujwcI756cPM/7PhrUFAyn1IrYHYsK4/O5gBEgbSBRjD0X8mJ0V3oIm/PtjMC YiXBJwzOMNXOeWp+HcyCR0eh2sQD94gbF9SUOKDoamNB3DbLEHKjYPJ9O3zQw/Xai624OXB0 Wk5yIW77I1mGWhwbWxeHOJ/NmhHEU38YfbxXSzCLeMv98bNTej4oA+cPtMZ94AZOSy/oroMh rsr6wA9PL7NS+B1kRbgv6a5KL9latAI7zPeXcVsYw076rL850PLez/SXDuIr9mud4v8Zvcp9 65vTK4lTAD4C4vneNRGt4iwCOIgGsAN6BgqEgr7EwLX8dAX57OXPKZj0/0TdCbu+qsoSrQ3u +Ul6k374jFeIndqg/e9NiJbHjYAuug3cZZ6mH24SXWtTd4hGWi6f26tQQcRyGiduZkw5Wn26 g0UVgps7o2zHwlp9LJVjL3pCw7a9tKOfZaH+h7dV5JsA/Oq+7F3PhTbyNagi4A9igw+0qU+n Ws/nZDVMRiUv+1HY4PG8q6iEGSfHHjwW8InYS+Ah3stTddJ0sLc+0AGutx8ueTE2Ks14c4c8 aNW5y9bNFI/6/UQmOOwGmBeYC/kjZhjhsC3dTJ9uX4pXlMhpLQARAQABzShDaHJpc3RpYW4g RG9jemthbCA8Y2hyaXN0aWFuQGRvY3prYWwuZGU+wsGYBBMBAgBCAhsDBgsJCAcDAgYVCAIJ CgsEFgIDAQIeAQIXgAIZARYhBOo4ombxzcKdfZnmgo+wd0icZLmNBQJbl/90BQkLSv0+AAoJ EI+wd0icZLmN5mMP/29bOCdd3/NNWnAlqqYCK01deHyPf/7ozwprv9FyYB2Pt6fxCeoru5Gh LKYFYhldmWVQ/nvvk4eMUfXQKosjeqlr1OjKC3JcHhop8SnoAHI7YQ6JzsJnRSZH0oXhuRYb omhUrRC5UtIfbz1UedXDreHY3tblh5BT3301iOTrw7DASreMp17xpOAHIip2tEc9fUthWCaj 6gA4F4RXpvsbkC8eeQB3DZNNKQ4jsjSC3+NZYQ6n2a+bQkGo0OHlphASn/M2ckimUhTAbhMl qrTxD5fDaEaHoom1WUl945aogFh5Y984x6QH8BknBLs+hnmcDBksZJmGIy8LrEA0urcG+NJm IFV2qvp+6wHUBwXpj8LS8hByU16u0JvGcmrUlfUX+3PM8PsJqKIZXN8WTxHu/d/D4Fo8MX2Y QA4IZ/qdybtFqV2/Q2x7d+9fBVMsGyYqnjuz5dczvOKTLsNffDBUblmxJbuuSy4GUVUPk8jO nRJyGWfyFxdko87g/5K2IO8OK+7fzueBDrx6JAEEN+prRqTPAqSEPI/ku/ddUDAohxd5oDM9 tQbC8MwDtt2OsXY2Md8AhV7NVX2rQcFHIFdE73XNtCSDV7oEjvQToQL49Wsp+qtV5F65t0MS Rc8pTg6+LocDrGRVpQFsC+MpJTvOw89clFRFqUnJ7VaO8IcSHvuTzsFNBFIuNbYBEACygpK2 VY5uya+sGZHmDD7PjgrSAmyC33ETgyrDPycRHXMW6/fVAORhoveDlxsb5EH+ci0MRoQs6yyV W66Qb5frLYO9v/A62Bggkpe9oMS00yJ3xcRLx98RqQT/6DF3Ro5Po8VgOPKKc7GmqwXfT8bx TWaFowfY3YMwT6TTGv8pMOAE1Qtn8wucbqOH8FLJdVrvAxS2zFcEhxlwqplekGFF39ItxCpz ZCkR92t63eybKwtP+pQS/LC6E+eCtyejRoounc2pYTsnLEiOEfHM3JaH90SMuTIf2f66r+Hd DoGNm+0DmJxqyE1bcguVKsxjGcdHZ0K+QZu2Dh2gjC/y4zKGI9qLxYds42lOiP7Jsd7LVZDE aZqge/3GD5LZKRlfCvUtJegoInqZ/acplNPzQgRSl6z7qKKys9Pl+o+mLEsuzydSghCIdp0j 3YQe/+Hs8Nwwfwjn0xPBGPsWz6UxeA3yPuAEa2z/edwuGdiQu8R1Bqh/g/00NqmIk5nx3WU6 871mBwhEQKWSqtRK3aZe5h3xZ8MqAwfDqkvUFn8M90JfE3qBTz+S3UuDx5BKqINrx4+p4yZy wy1HFOThilaxorvKnTBsiCTXsmOnhnJfuEUfojSWglUsCwwfqLW8QoNnHphgH70yOBhqcMV7 n/P6/CS/ZfSYK/88Nlq6ImcDiQ4T6QARAQABwsFlBBgBAgAPAhsMBQJZuPZuBQkJa/Q4AAoJ EI+wd0icZLmNCyUP/3J0d7PyWm1wVgG5Ix2x5CEjhoPUANGrY7VnGE0esB7fZHhEXwghHuoR M9CY8AwJjpxDB93obpy2IhDQEtx0sOY24e6kuBIibdcwxKXuz/JQ5rpPpxsGMiO3QJCTFO0k gcrN2Q25M+XoxqHBr36tbVv3Qf9KOTlU/IfUkzPxsJGtWGXTXSibQPlhjeTUnxFUOgg3j4uq llgXNg2D8uVwCtxw+FKcZl+pwZQ0aFtS9OLAGOvjZabrMbACt22yPGhJbp1WLRC+pHCcgL1b f1VwuBm5qz3bgCfPu/fapOrsG6+NhCTtdvkvam+Z4x+Pq1XZ4D1sokKboBsDDkeANihQf1f6 BYvAIv3qdrWrV4pcIlz53sLvkQ2Ofq6oW8Fbn9ZkDtKMAVHuWca2jJ3RARUCKshaPbzOlCf+ FwKOzahKDIBbjP6AOdbyRUBnHPvjZfVFWju7LNdNSuqSRiLnmmESPomdn28q8VoUcYamJKcs byB3YFAz/YfVWN62ADn0ojFwHGAxsdc7Ud+gEbfmc8oDiP+ecn+gk9OFrUg1EOs98OVJKm1/ 2Dy2I28zJGQBH2QQcvjzWltje+/Woqli3wx3uO5rdy/Ad/05Ieb3wBu0XIeDZpVxSCHZbOJ0 HQuQdtd65Dg20DrxVNASpY8W1pgiaBIaa60QVE7oui/c2hePTlqywsF8BBgBAgAmAhsMFiEE 6jiiZvHNwp19meaCj7B3SJxkuY0FAluX/3QFCQtK/T4ACgkQj7B3SJxkuY24YhAApwTdvRxp pSS6i8odx/5W2Qyl1kINSs5U4jHC/xFMK1IWCytC5vbbBzYIEH6rZwCU1vtIP0PcBrCwwMk2 h7YD1MpvIxVrT7+OWHxxJUsHVEs8vNGSsXMOVrA+KH6byorXuI+3oc3oCRdJydSZTxRsEQ2k aFYoPnEA6o7St3wjn5bE4CHKreIAf+OMe/c1kn3amoOuESzJrYVVqvnkQkMxTWjh+p0lHKZl 3vzkzEWMd8HqrJrSwJuJHB0XRkem5pZjnJ4OYJXk9kyJsIltym0cwxhSM4/4HMel77KJxHSh r/1YFFmL6sUp5LXff2FlVEGo/lzfgu0tqfFU4ZMM08Wxt9I1PK4IwoHIt3Tm4qZucJL13SNj o65OcM9sg7UEtQx4xOBngtHz9l4pwtyHh/Ll5dYIAsR+3psxE2YDPoYjNSI7eDPNJ4Y2zAff PavAoXjoZU/+kdBuwVigKBaP58fiqs1jaEV9rVj2ja28Yj3U8Ht5eopidC2KjKDRhudvlghP fCbIoVxOcetptrxBc7WyfwsssiAIHHUHZ1XofTdgYcffS3SlpsW9QyxouJ7AXbZTq+Jxh2zt +j2wbz6dFITBjHvFELONTQRqdruGr2z3UGHDAXVERx4HFTzFE0CDew9cxjzSsP99X9dQWOKN wXWy1wIICd3Rm5tmQJ49zkESt0o=
- Ironport-phdr: 9a23:ufZe6hFEYczg+M9JTZxzwJ1GYnF86YWxBRYc798ds5kLTJ7zps2wAkXT6L1XgUPTWs2DsrQY07WQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmDiwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KOSA38G/Xl8J+j6xVrxyuqBN934HZe46VOOZkc63aYd8XS2hMU8BMXCJBGIO8aI4PAvIfMOZYtYn9pkAOrQe/BQa2AuPk1zFGhnjq0qw70OQuCwXG1xEnEt0SsHTUttT1NLwOUeC01qbIyy/PYO5R2Tjh6YnIcQouofWXUL1ud8rR0lAjFwfFj1WXr4zpJT2V1v4UvmWd8uFuW+Wvi2s9pAFwpDii3sYsio/ThoIU0F/I7yt5wJwzKNalS0B7ecapHIZfui2GLYd7QMEvT3t1tCs7yLAKo4C3cDYUxJg/2hLSZOCLf5KK7x/hTuqdPDR1iXx/dL6iiBu/806twfDmWMauylZFtC9Fn8HMtn8T0xzT7dCKSv9n8Ui6wjmAyRrf5f9CIUAvjKbbL54gwrk2lpYJv0TDBDf6mETwjKCIakUp4vWk5uv7brn8pJKRNZV4hhz/P6ksgMCzH/o0PhYWU2ie4+u81bnj/UPjQLVNi/07irXWsJDAJcQava65Hw5V3Zwl6xqlEjim18gXnHgELF1ffBKKlJbmO1fVIPzhCfe+g1OskDFxy/DIJL3tGo/NIWTbkLf9YbZ97FZRxxY0zdBG/p5bFrUBIO/oVULqr9zZDho5MxSuzOr9CdV90JkeWWOVDaODPqPSqwzA2uV6KO6VIYQRpTzVKv4/5veog2Vqt0UaePyC3YEWc2y5F/IuD0KSc3nlhp9VGmcQvxEiTeXszlGFWixQbnKaUqQnozUqD4TgA52VFdPlu6CIwCruRs4eXWtBEF3ZSS65JbXBYO8FbWepGuEklzUFUba7TIp4jkOjshS/z6tgKKza4H9B7M6x5J1O/+TW0CoK23lsFc3EiDOASXoxmnIPQXk4xvIn+BEv+hK4yaF9xsdgO5lT6vdOC1ZoMZfWxeE8BtbpHwbQedHPRkz0Gtg=
- Openpgp: preference=signencrypt
Hello,
I currently install coq (and mathcomp, merlin, etc.) via OPAM, and I
agree with Théo on all points. Distributions like Ubuntu will take at
least a year (two for the current LTS release) before they will ship
OPAM 2.0 in their repositories. Currently, there isn't even an external
repository providing 2.0 for Ubuntu. So users would need to resort to
install scripts that dump binaries into system folders or manually set
up paths and the like. Not at all satisfactory.
Rolling Release distributions (e.g., Arch and Gentoo) should be faster,
but will still take weeks/months.
However, unless the OPAM developers/maintainers change their stance
regarding the repository for 1.2 users, this will require the Coq
developers to also provide packages for dependencies not to be found in
the 1.2 repository (I'm thinking of things like camlp5 here). This will
create a bit of extra effort.
Best,
Christian
On 05/10/18 00:48, Théo Zimmermann wrote:
> Hello,
>
> Thanks for raising this question.
> I was personally quite shocked by the decision of OPAM maintainers to
> almost freeze the OPAM 1.2 repository when OPAM 2.0 was released (seemed
> pretty aggressive to me). Especially since IIUC OPAM is not able to
> upgrade itself. But then, I am not an OPAM user myself so my view might
> be prejudiced.
>
> So let's have this discussion: please share your opinion if you have one.
>
> If we decide to continue providing an OPAM package for OPAM 1.2 users,
> it should be pretty straightforward to do so using Coq's own OPAM
> repository http://coq.inria.fr/opam/released, the same one that is
> currently used to distribute Coq plugins and libraries.
>
> If we decide against doing so, it might hinder adoption of Coq 8.8.2 and
> upcoming Coq 8.9.0 (not a good thing). It could also lead to the weird
> situation that users are able to test Coq 8.9+beta1 through
> https://coq.inria.fr/opam/core-dev/ but are then not able to upgrade
> from the beta to the final version. So a priori, I am personally in
> favor of continued OPAM 1.2 support (but again I'm not in the best
> position to form an opinion given that I don't use OPAM).
>
> Best,
> Théo
>
> Le jeu. 4 oct. 2018 à 23:42, Christian Doczkal
> <christian.doczkal AT ens-lyon.fr
>
> <mailto:christian.doczkal AT ens-lyon.fr>>
> a
> écrit :
>
> On 10/04/2018 09:08 PM, Théo Zimmermann wrote:
> > FYI, the signed Windows packages are now available on the release
> page, and the OPAM package is now ready (for OPAM 2.0 users) thanks
> to Heiko Becker.
>
> Will there be an OPAM package for OPAM 1.2.x users? As of now, OPAM
> 2.0 has yet to arrive in the Gentoo or Ubuntu repositories. Other
> distributions will likely also still ship 1.2.x.
>
> Best,
> Christian
>
Attachment:
signature.asc
Description: OpenPGP digital signature
- Re: [Coq-Club] Coq 8.8.2 is out!, Perry E. Metzger, 10/01/2018
- Re: [Coq-Club] Coq 8.8.2 is out!, Théo Zimmermann, 10/04/2018
- Re: [Coq-Club] Coq 8.8.2 is out!, Christian Doczkal, 10/04/2018
- Re: [Coq-Club] Coq 8.8.2 is out!, Théo Zimmermann, 10/05/2018
- Re: [Coq-Club] Coq 8.8.2 is out!, Christian Doczkal, 10/05/2018
- Re: [Coq-Club] Coq 8.8.2 is out!, Emilio Jesús Gallego Arias, 10/05/2018
- Re: [Coq-Club] Coq 8.8.2 is out!, Théo Zimmermann, 10/21/2018
- Re: [Coq-Club] Coq 8.8.2 is out!, Christian Doczkal, 10/21/2018
- Re: [Coq-Club] Coq 8.8.2 is out!, Vadim Zaliva, 10/24/2018
- Re: [Coq-Club] Coq 8.8.2 is out!, Théo Zimmermann, 10/24/2018
- Re: [Coq-Club] Coq 8.8.2 is out!, Christian Doczkal, 10/29/2018
- Re: [Coq-Club] Coq 8.8.2 is out!, Théo Zimmermann, 10/21/2018
- Re: [Coq-Club] Coq 8.8.2 is out!, Emilio Jesús Gallego Arias, 10/05/2018
- Re: [Coq-Club] Coq 8.8.2 is out!, Christian Doczkal, 10/05/2018
- Re: [Coq-Club] Coq 8.8.2 is out!, Théo Zimmermann, 10/05/2018
- Re: [Coq-Club] Coq 8.8.2 is out!, Christian Doczkal, 10/04/2018
- Re: [Coq-Club] Coq 8.8.2 is out!, Emilio Jesús Gallego Arias, 10/05/2018
- Re: [Coq-Club] Coq 8.8.2 is out!, Théo Zimmermann, 10/04/2018
Archive powered by MHonArc 2.6.18.