coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Plugins, type-checking, and universe constraints

From: e AT x80.org (Emilio Jesús Gallego Arias)
To: Talia Ringer <tringer AT cs.washington.edu>
Cc: Coq-Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Plugins, type-checking, and universe constraints
Date: Fri, 13 Apr 2018 13:23:54 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=e AT x80.org; spf=Pass smtp.mailfrom=e AT x80.org; spf=Pass smtp.helo=postmaster AT x80.org
Ironport-phdr: 9a23:7/NIFRe5pvHHDUB1olZu1fNylGMj4u6mDksu8pMizoh2WeGdxcuybB7h7PlgxGXEQZ/co6odzbaO6Oa4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahb75+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v9LlgRgP2hygbNj456GDXhdJ2jKJHuxKquhhzz5fJbI2JKPZye6XQds4YS2VcRMZcTyxPDJ2hYYsIAeoPM+RXoYrzqFQBsRSwChKhBP/2yjJSmnP6wbc33uYnHArb3AIgBdUOsHHModrrL6oTXuO4wLXSwTXEdfNW1ir25IzHfBAkoPGMWbNwcc3MwkcrCQzFlU+IqZf4ND2UzOsNt2yb4PRvVeKolmUqtxtxojm1ycc3j4XEgJ8exF7D9SV82ok1JNu4RVZ0Yd6lDJtQtzyaOJBsTsw+RGFovSA3waAFt56jZCUG1Zcqyh3FZ/CZbYSF4wjvWPuTLDtlnn5pZbyyiwiq/UWjy+DwTMi53VRQoidBiNXAq2wB2h3V58OaUPVy5F2h1iyK1w3L6uFLP0Q0la3DJp8uwbM8ioAfsUPZHi/5gEn2jamWeVs4+uWw9ujqYbbrqoWCO4NqiwzyKLkil86iDegiLwQDUXaX9fy51LL5/E35RLtKjucxkqncqJ3VO98Wp6G6DgNJyIoj7Ay/Dzi+3NQCgXYHNE5FeA6Aj4XxJ17OJ+n4Ae6jjFSojTdk3OvLPqbhA5XINnjMiq3tfbd7605GyQo818pT55xOCuJJHPWmZkb1tdWQNB4/PAGui7L7EtR72Y4EcWmURLCQK6PTt1CU4eRpLuWRMtw7ojH4fvUN9662y3gjlhddUKyo2ZoQIFK1BWZ9a2qQZX7hjdBJOH0LtxF/H7+is0GLTTMGPyX6ZKk7/DxuTdv+Vd6SFLDou6SI2WKAJrMTY2lHDl6WFnK5JZXUA7ELci3Ae5Y9wAxBbqCoTsoa7T/rrBXzmuh3frKS/TcX58q6iYpFotbLnBR3zgRaSsSQ12bcHXEkxiUPXTBkha0=
Organization: X80 Heavy Industries

Hi Talia,

Talia Ringer
<tringer AT cs.washington.edu>
writes:

> Also, it would be useful I think to have documentation of best practices
> for plugin developers, beyond the new API which is a start. It can still be
> difficult as a plugin developer to know which of my many options are better
> for which situations. I can help by curating things I've been confused
> about in the past, so you know what questions a plugin developer might have.

I hope that 8.9 will use Dune/odoc to present the ML API as modular set
of libraries, apart from a much needed high-level overview we hope to
improve significantly the code documentation itself. Please see:

https://github.com/coq/coq/issues/7155

Also please open the needed issues as Théo pointed out, thanks!

Best,
E.

[Coq-Club] Plugins, type-checking, and universe constraints, Talia Ringer, 04/10/2018
- Re: [Coq-Club] Plugins, type-checking, and universe constraints, Sylvain Boulmé, 04/10/2018
  - Re: [Coq-Club] Plugins, type-checking, and universe constraints, Matthieu Sozeau, 04/10/2018
- Re: [Coq-Club] Plugins, type-checking, and universe constraints, Emilio Jesús Gallego Arias, 04/11/2018
  - Re: [Coq-Club] Plugins, type-checking, and universe constraints, Talia Ringer, 04/13/2018
    - Re: [Coq-Club] Plugins, type-checking, and universe constraints, Théo Zimmermann, 04/13/2018
    - Re: [Coq-Club] Plugins, type-checking, and universe constraints, Sylvain Boulmé, 04/13/2018
    - Re: [Coq-Club] Plugins, type-checking, and universe constraints, Emilio Jesús Gallego Arias, 04/13/2018