Stream: Coq devs & plugin devs

Topic: Working Group on CEP62/CEP63


view this post on Zulip Enrico Tassi (Feb 23 2022 at 21:19):

Here a "doodle", please fill in by Friday 5PM Paris time, so that I can announce the date here before W.E.:
https://framadate.org/NCcsXegnmPy57Xwu

view this post on Zulip Enrico Tassi (Feb 23 2022 at 21:22):

CC @Paolo Giarrusso (I don't know how many colleagues of yours read this stream, if they don't please tag them here)

view this post on Zulip Paolo Giarrusso (Feb 23 2022 at 21:56):

Cc @Gregory Malecha @Gordon Stewart @David Swasey @David Swasey

view this post on Zulip Enrico Tassi (Feb 28 2022 at 21:41):

I forgot to announce the best date, it is "Thursday, March 3, 2022 - 2PM (Paris time)"
(4PM has the same votes, but I prefer 2PM, if you don't mind)

view this post on Zulip Enrico Tassi (Mar 01 2022 at 10:05):

It would be nice if a kernel maintainer could attend (CC @Gaëtan Gilbert @Maxime Dénès @Pierre-Marie Pédrot ).

view this post on Zulip Pierre-Marie Pédrot (Mar 01 2022 at 10:09):

I should be there.

view this post on Zulip Enrico Tassi (Mar 03 2022 at 12:56):

https://rendez-vous.renater.fr/coq-engineering

view this post on Zulip Karl Palmskog (Mar 03 2022 at 13:10):

not going to participate in the WG, but I hope I can make one comment: please distinguish between interfaces and their semantics on one hand, and implementation aspects such as separate compilation on the other. In my view, the title of CEP 62 is really misleading

view this post on Zulip Paolo Giarrusso (Mar 03 2022 at 13:14):

@Karl Palmskog "separate compilation" is a semantic concept by Cardelli; even if arguably it's a questionable name, it's standard.

view this post on Zulip Karl Palmskog (Mar 03 2022 at 13:16):

SML modules/functors/signatures is to me the standard of any kind of interfaces, and SML '97 does to my knowledge not even specify anything about compilation.

view this post on Zulip Paolo Giarrusso (Mar 03 2022 at 13:19):

@Karl Palmskog well, http://portal.acm.org/citation.cfm?doid=1159876.1159883 adds separate compilation to Standard ML

view this post on Zulip Paolo Giarrusso (Mar 03 2022 at 13:20):

authors include both "core SML people" (Karl Crary, Robert Harper), and David Swasey who's coauthoring the CEP

view this post on Zulip Enrico Tassi (Mar 03 2022 at 15:34):

Here the toy: https://github.com/gares/coq-defunctor

view this post on Zulip Paolo Giarrusso (Mar 03 2022 at 22:58):

in later discussion, we realized that using opaque ascription (as in Module A : A.interface.) is not strictly necessary, since clients aren’t importing the implementation files. Using Module A <: A.interface. gets closer to the opt-in ascription that @Jason Gross was suggesting.

view this post on Zulip Paolo Giarrusso (Mar 03 2022 at 23:06):

The downside is that Cardelli's "separate compilation" guarantee, or rather the "compositional typechecking" one, is only as good as the import discipline. C++ friend declaration arguably have better ergonomics.

view this post on Zulip Notification Bot (Mar 04 2022 at 07:17):

Enrico Tassi has marked this topic as resolved.

view this post on Zulip Notification Bot (Mar 04 2022 at 07:17):

Enrico Tassi has marked this topic as unresolved.

view this post on Zulip Enrico Tassi (Mar 04 2022 at 07:19):

Paolo Giarrusso said:

in later discussion, we realized that using opaque ascription (as in Module A : A.interface.) is not strictly necessary, since clients aren’t importing the implementation files. Using Module A <: A.interface. gets closer to the opt-in ascription that Jason Gross was suggesting.

Indeed. A single file coud implement even two interfaces in one go. This suggests that the link command needs to address more than a 1:1 relation

view this post on Zulip Paolo Giarrusso (Mar 04 2022 at 08:30):

You can already combine module types via Include/<+, and this is somewhat extensively tested by Coq's numeric library.

view this post on Zulip Paolo Giarrusso (Mar 04 2022 at 08:39):

But in general, even if I argued for automatically doing the translation or enforcing it, there are indeed cases needing a more flexible "source language"; so we should just use Link directly, and encode any rules we'd like in a linter.

view this post on Zulip Paolo Giarrusso (Mar 04 2022 at 08:40):

linting infrastructure is also needed, but it'd be a separate discussion

view this post on Zulip Maxime Dénès (Mar 04 2022 at 08:51):

Depending on what you call linter, my current work on having a separate parsing phase for the vernacular language may help. Namely if the linting is done on static criteria that does not require execution.


Last updated: Feb 05 2023 at 21:03 UTC