-
Notifications
You must be signed in to change notification settings - Fork 374
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Module system enabling separate compilation #416
Comments
It may be worth looking at Musa Al-hassy's "Do-it-Yourself Module Systems" (PhD thesis and defense slides). It targets Agda, and so much of it is likely applicable to Lean as well, while providing a powerful model of how the functionality of module systems can be achieved without introducing a second "module language" with all of its downsides - while also providing powerful tools for composition and reinterpretation of interfaces. |
@eternaleye This issue is about second-class, unparameterized modules in the sense of compilation units, so I'm not sure that work is applicable here. We certainly don't want to represent module signatures (shallowly) as Lean types. |
Would this be a relevant pointer to Racket's phase separation? |
I found the answer to my own question so removing to reduce the noise on the issue. |
Currently
import
truly imports everything from a module, includingprivate
declarations and transitively imported declarations. Thus if we make any change at all that is reflected in the .olean output file, we have no choice but to recompile every downstream module.This issue usually is solved by use of a "proper" module system that allows sufficient information hiding, e.g. by exporting only the signatures of declarations (and not even that for private declarations). In the simplest case, this can be done literally in a "signature" .olean file, in which case the build system can forego rebuilding downstream modules (that in fact import only the signature file) if the file is unchanged. However, note that this does not a priori prevent rebuilds on other kinds of changes such as adding a new (public) declaration, which would be much harder to prevent.
A module system with proper information hiding would not only avoid rebuilds, but also follow general good software practices and enable further ones such as semantic versioning. However, some aspects of Lean (and similar ITPs) complicate the design of such a system:
abbrev
,[reducible]
, and similar should automatically do), or we have to import the full .olean file after all. Any library aiming to make the most out of the module system should strive to prove all relevant properties about a definition inside the definition's module so that downstream modules can rely on these theorems instead of having to unfold the definition. However, if a module is split into multiple parts merely for code organization, then importing the full .olean files within that group should be fine, retaining access to the definition bodies within the group and separate compilation outside of it. If a definition is sufficiently simple/stable that changes to it are not expected, it can still be fully exported using some marker as mentioned above, of course.Int
-indexed phase system for our use cases.[inline]
and[specialize]
, there is no way around exporting the definition bodies (or rather their IR) if we want to these attributes to work cross module. Then there are some cases where the body affects the ABI, e.g. in type synonyms such asdef MyUnboxedUInt := UInt16
. Finally, some cross-module information we are currently using such as lifted closed terms should probably be limited/disabled, at least by default, so it does not defeat separate compilation.The text was updated successfully, but these errors were encountered: