Separate compilation

[gmalecha]

Based on our abstract at CoqPL'22.

https://popl22.sigplan.org/details/CoqPL-2022-papers/6/A-Case-for-Lightweight-Interfaces-in-Coq

https://www.youtube.com/watch?v=5lS6pmM8ewk&list=PLyrlk8Xaylp60WScVlfaTd53Zwb_ERADO&index=7

[ppedrot]

FTR, I am not very convinced by the fact that we really want a vi file separate from the v file in Coq, despite the argumentation from the abstract. In the ML realm, It perfectly makes sense because the interface is typically reduced to types, but this is not is not the case for Coq. A typical Coq interface exports a lot of stuff that you definitely don't want to copy-paste between files. Sometimes you can't even write it properly because it's autogenerated in some way, e.g. Equations and the like, and you care about the proof term but you don't want to copy-paste the horrendous output of Print with Set Printing All. Not even mentioning the fact that some terms are not even parsable in a faithful way.

I believe it would be better for usability to have a pair of public / private attributes to selectively export stuff. Otherwise we are at risk of introducing an unwieldy system that will not be used on a large scale.

[Blaisorblade]

A typical Coq interface exports a lot of stuff that you definitely don't want to copy-paste between files.

We agree that we'd want a mechanism to avoid the copy-paste ergonomically, even if that is not discussed in the above CEP (a colleague was working on this problem).

• I'm certain that public/private would be more convenient in some cases, while .vi files would be better in some others where implementations aren't enlightening, and I can see why you'd think the first is more common. Moreover, in principle the two interfaces could be equivalent ways to access the same functionality: if you imagine you had a Coq parser, you can split a file with #[private] attributes into a .vi and .v file and viceversa by source-code transformation.
• OTOH, would you have to extend each top-level command to support a #[private] attribute, both in code and in the semantics? Would #[private] Require be skipped when producing a .vio file? Reusing opaque ascription seems conceptually simpler.

I can also imagine some of the design might be shared between the two approaches, tho not sure how much.

[ejgallego]

I am not very convinced by the fact that we really want a vi file separate from the v file in Coq

I am very convinced we don't want that in fact indeed, but thanks a lot for doing the proposal, hopefully we can all discuss on the WG these coming days.

[gmalecha]

Thanks for the feedback. I will look forward to discussing. Coq is clearly a very complex system with a lot of pieces, adding a new piece to it should be carefully considered. In my mind, there are a few things at play here and they muddy the waters quite a bit.

The proposal itself adds nothing to the core language of Coq, but there are many well founded concerns about the way that it interoperates with existing features of Coq. To me, this suggests that there are concerns about the design of the core language. In this proposal, those concerns seem to be related to module types and functors, and my rough summary of them from the discussion is that they are clearly broken to the point that it is questionable (at least by some) whether they should be fixed at all or if instead Coq should go the Haskell route and abandon them entirely. That may be a discussion to consider very seriously, and if the choice is to abandon them entirely, then I might very well fall on the side of not accepting this proposal.

Regarding the statement that the interface is much larger in dependent type theory than in simpler languages such as Ocaml, I definitely agree. And I also agree that there are clearly modules where the implementation is (almost) the interface, e.g. Coq.Bool.Bool, etc. (I say "almost" because if the interface was truly the implementation, then there would be no Qed-d definitions in those files, but that is not the case.) But in many uses of Coq this is not so, and program verification is one of those cases but (I do not believe) the only one.

[gares]

I like this proposal and I think it is indeed the opportunity to remedy the universe leakage mess. All the rest seems to me a improved .vio/.vos thing, which is kind of working already modulo universes. I mean, I don't see any blocking issues in providing the interface beforehand (as a separate files or as attributes, again it seems a detail to me). I personally don't consider the link-time-check for universes a good solution (even if it is the best I could suggest myself when I coded the .vio/-quick thing).

About universes we do have a few commands already to name universes and impose constraints on them. I wonder if it would be feasible to mandate such declarations in .vi files and also have a mode where Coq resolves the typical ambiguity of Type not to a Type_j for a fresh j, but to one of these named universes part of the public API. We did experiment with this feature a long ago in Matita where the universe graph has to be defined once and for all in the first file, and then any universe variable would have to be resolved to one existing node in the graph, as some point. We did not test it in the large, but I was wondering if the industrial-scale use case you have in mind could fit this frame or not at all.

The funny story is that math-comp compiles with 3 universes. It used to be true, maybe it is still. I would not be scared of declaring by hand a graph with, say, 5 nodes and have Coq assign all my Type_j to a named node before saving the .vo file. I clearly see a class of users that benefits from full ambiguity and universe inference, but for the others I believe separate compilation is doable (in a sound way).

[ppedrot]

About universes, one feature I've been trying to implement without much success was to extend the private universe feature to monomorphic universes. That is, levels and constraints local to a Qed proof that do not affect the global graph should not be declared globally. Furthermore, if there are constraints that still affect the global graph (typically by transitivity) you get a warning except if you annotate the definition accordingly. In this model, only constraints coming from accessible data (types and defined bodies) are part of the public interface.

[gares]

I naively thought that this is what "minimization" is supposed to do.

[ejgallego]

Hi folks, I've added a topic to schedule a possible meeting https://coq.zulipchat.com/#narrow/stream/314095-Coq-Hackathon.20and.20Working.20Group.2C.20Winter.202022/topic/.2Evi.20Interfaces.20Proposal

[Blaisorblade]

We agree that we'd want a mechanism to avoid the copy-paste ergonomically, even if that is not discussed in the above CEP (a colleague was working on this problem).

Regarding copy-paste, the anonymous colleague @gstew5 now posted https://github.com/coq/ceps/pull/63 :-)

[maximedenes]

Separate compilation is of course a (very) desirable feature.

Similarly to others above, my personal opinion is that separating implementation and interfaces in two files brings more disadvantages than benefits : duplication, cross-files errors (when an interface is not satisfied). To me, a solution based on (public/private) attributes would be superior, if it comes with proper tooling : IDEs being able to describe a (documented) interface, efficient separate compilation, etc.

Could we sketch an attribute-based solution?

[gares]

To make the discussion more concrete, I crafted an example using what we have today. I guess it is not satisfactory to you, but I have an hard time understanding why. Here it is: https://github.com/gares/coq-defunctor/tree/master

[ejgallego]

Could we sketch an attribute-based solution?

Indeed I have a feeling similar to @maximedenes , but I don't know enough yet about the problem.

I am in particular missing a good description of the problem in the CEP, which if I read it correctly, jumps directly to propose a solution. Do we have that somewhere?

[github interface and I don't get along sometimes too well]

[ejgallego]

I did give to this some more thought, and I think that we should not use files to track leakage, but the document model should take care of it, as it is done for opaque or incomplete proofs already in the Flèche prototype (and I've got quite confident in that it works)

That is to say, when checking a document, a delta that only updates the implementation should not force re-checking of the parts not depending on it.

[Blaisorblade]

Just three high-level questions on https://github.com/gares/coq-defunctor, after @derkha's prodding:

1. can we enable Link for individual definitions, beyond just modules?
2. does Linking a constant A_impl with A create a definitional equality A_impl = A? The same question extends to modules with constants in an obvious way (intuitively, if you over-simplify modules as name -> option term functions, the extension is pointwise: do you get def. eq.s for each constant that's linked to a parameter?).
3. users can write inconsistent Link statements — detecting them when loaded together will prevent proofs of False, but should they also be detected more eagerly?