Separate compilation #62
Conversation
This rewrite preserves most of the old content, but I hope it flows better and is more obviously compelling.
Yes, a reviewer asked specifically, but this caveat is awkward and the point should be clearer from the rest of the document.
Also change the later example.
| checking. Such a link-time would be effectively the same as `Require`ing all of | ||
| the modules in a library preferring their *implemenation* (`.v` file) rather | ||
| than their interface (`.vi` file). If the combined set of constraints is | ||
| satisfiable, then there is no problem. |
There was a problem hiding this comment.
The problem with universes is not so much satisfiability than the fact you can get wildly different results depending on the link order, because this affects unification and the like. It is somewhat easy to craft a Definition foo : bool. whose value in separate compilation mode depends on the scheduling order.
There was a problem hiding this comment.
because this affects unification and the like.
It is somewhat easy to craft a Definition foo : bool. whose value in separate compilation mode depends on the scheduling order.
Link-time checks happen on concrete proof terms, so what's the unification in question?
There was a problem hiding this comment.
The issue I mentioned happens for vos files, but a similar problem arises with separate compilation. Namely, there are cases where replacing the interface with the implementation will result in later files being compiled differently, breaking the abstraction boundary. For a simplified and contrived example, you can consider
Universe i j.
Lemma dummy : True.
Proof.
constr_eq Type@{i} Type@{j}.
constructor.
Qed.
Definition b : bool.
Proof.
(let _ := constr:(let _ : Type@{i} := Type@{j} in tt) in exact true) || exact false.
Defined.where the value of b depends whether the proof script of dummy has been evaluated or not at the time b is computed. In separate compilation mode, it means that an interface where dummy is an axiom won't produce the same proof as one where the proof is explicitly given, despite being clearly compatible as per the module rules. This is not specific to Qed proofs, one can also trigger this kind of behaviours with explicit constraints hidden under module interfaces.
There was a problem hiding this comment.
But in the separate compilation model we don't expect to be able to remove the interface and still compile dependants, so it's not a problem IMO
There was a problem hiding this comment.
Yes, “removing the interface breaks clients” is an intended feature. But the only existing way to fully compile this code in non-vos mode would leak the extra constraint to clients, despite opaque ascriptions; this was brought up in December and it’s concerning. I’ve seen no evidence this is a real problem (compared to the periodic universe inconsistencies we do see), but in principle it seems fixable (very invasively!) if you’re that serious about separate compilation: always defer checking of these constraints to the link-time check. But that’s independent of this proposal, and relevant to vos builds in general.
despite being clearly compatible as per the module rules
I agree that the subsumption rule would suggest ”dropping interfaces” should work, but subsumption on source-language modules doesn’t actually work (in Coq, OCaml and many other languages). Even ignoring hints etc., Import + width subtyping is enough to break subsumption: if you Import foo and foo adds a member bar, then foo changes to a more specific type, yet bar can shadow existing bar and break clients.
|
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 I believe it would be better for usability to have a pair of |
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 can also imagine some of the design might be shared between the two approaches, tho not sure how much. |
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. |
|
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. |
|
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 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 |
|
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. |
|
I naively thought that this is what "minimization" is supposed to do. |
|
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 |
| To address these problems, and support information hiding and Cardelli-style separate | ||
| compilation, in this CEP we propose a notion of Coq interface files, which we |
There was a problem hiding this comment.
Would be helpful to briefly spell out what "Cardelli-style" means. A reference would be nice, although I personally am not always able to access referenced papers.
| to today's `vos` builds (initial builds can be more parallel, and incremental | ||
| builds need to recompile fewer files). | ||
|
|
||
| NOTE: For concreteness, in this CEP we use the `.vi` extension for for interface |
There was a problem hiding this comment.
| NOTE: For concreteness, in this CEP we use the `.vi` extension for for interface | |
| NOTE: For concreteness, in this CEP we use the `.vi` extension for interface |
| Export __lib. | ||
| ``` | ||
|
|
||
| ## Only a `.v` File |
There was a problem hiding this comment.
Do you expect that this will be the most common case for the long term?
There was a problem hiding this comment.
No. I would hope that there are a lot of libraries that would have meaningful theory that could be put in a .vi file. @charguer mentioned some things like this in his standard library talk.
| - only `lib.vi`; | ||
| - or only `lib.v`. | ||
|
|
||
| ## Both a `.vi` and `.v` File |
There was a problem hiding this comment.
Are there any things that can't appear in a .vi file (or in practice wouldn't be included in a .vi file)?
| specification. However, this is an approximate specification, because the exact | ||
| semantics cannot be expressed via source-to-source transformation. | ||
|
|
||
| As a key principle: `.vi` interfaces are meant to hide implementations and |
There was a problem hiding this comment.
The use case for hiding "implementations" is primarily proofs (plus necessary definitions)?
There was a problem hiding this comment.
Qed is typically good enough to hide proofs, but you often want to hide more: both hints needed by the implementation, but also the bodies of definitions, etc.
There was a problem hiding this comment.
Not just, it can be useful to hide bodies of definitions that you do not want clients to think about though this does not work well if you want to compute on the definitions.
| suggesting an implementation strategy, we sketch a semantics as a | ||
| source-to-source transformation, to be taken as an informal and _approximate_ | ||
| specification. However, this is an approximate specification, because the exact | ||
| semantics cannot be expressed via source-to-source transformation. |
There was a problem hiding this comment.
I would much prefer a version where this can be fully implemented as a source-to-source translation (in part because that makes things easier for the bug minimizer). I think it also solves some design questions without making things significantly worse for the user.
I propose the following:
- Interfaces are interpreted as module types
- Compiling a .v file with a corresponding .vi acts as if the module type were ascribed to it (except possibly
Requires, which may be considered to be above the module type ascription as far as global side effects go) - At
Requiretime there should be three flavors: a file canRequirejust the compiled .vi file, it canRequireboth the compiled .vi file and the compiled .v file, or it canRequirejust a compiled .v file. The last should be an error if a .vi file (compiled or source) exists alongside the .v/.vo file. Requiring both the .v(o) and compiled .vi should be like Requiring the compiled .vi and then attaching bodies to the constants forPrint Assumptions, etc (in the same way it would happen for modules opaquely ascribed with a type), and also including the Requires of the .v file.
This pushes all the issues with side effects of require, universe constraints, ability to use Extraction, etc, onto the user side in a systematic way, by putting linking under the user's control (linking corresponds to requiring the compiled .v file).
There was a problem hiding this comment.
except possibly Requires, which may be considered to be above the module type ascription as far as global side effects go
To actually achieve separate compilation, the Requires would have to be inside the module and be hidden by the opaque ascription. Today this gives a warning, but in the Coq call it wasn't clear why, but until that's resolved I consider a source-to-source translation impossible today :-).
There was a problem hiding this comment.
This is what I tried to explain (very badly) by saying that an interface should morally be
Require stuff.
Module Type this.
Import some stuff.
...
End this.There are a few "actions" performed by require which don't play well with modules, which are usually seen as a linguistic construct to limit the scope of things.
Ideally, if one does not import a module, he does not get any effect. But require, today, leaks stuff, like global hints. So placing it inside a (sub) module does not do what you may think. Also, there is special code hoisting some actions at the top level, like loading ML plugins and co which is ugly and has no real use case.
Finally, it would be nice to have a header in each file which lets one compute the dependencies of the file easily. If requires are only allowed in there, then we kind of have this header. If we allow them to be anywhere, well... Similarly, require is slow, if they are all at the beginning of the file, a UI pays the cost once upfront, and then it is good to go. If they are interleaved with other sentences, well, you may need to backtrack over that slow line way more often.
To sum up, it is both an "hygienic" and would allow some code simplification if all requires were on top.
There was a problem hiding this comment.
Generally (though this is a fairly purist point of view), I have been thinking of .v files as corresponding to functors from their Required dependencies. Currently, Coq does not provide a mechanism to ascribe a type to these modules, so there is no means to abstract. With this approach, you can change what the module type being abstracted over is which provides more flexibility to the implementer of the interface. If I follow this mental model, then the second flavor of Require that you describe above means that you can "abstract over" the "natural" module type (the one that does not hide anything, including the body of opaque definitions); however, it becomes a bit odd because to typecheck those definitions you might need the body of other constants which could introduce problems.
|
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? |
|
To make the discussion more concrete, I crafted an example using what we have today. |
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] |
|
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. |
|
Just three high-level questions on https://github.com/gares/coq-defunctor, after @derkha's prodding:
|
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