Skip to content

Option for precompiling whole packages #2757

Open
@Kha

Description

@Kha

We're starting to learn that precompiling individual modules can be costly and have other resource constraints after all. While mathlib may need a solution providing custom granularity of precompilation that is yet to be designed, this issue is about a much simpler solution that makes sense for medium-size projects like Aesop: precompile the entire package into a single dynlib and load that one in dependencies. Note though that the dynlib should contain only code from that specific package and link to other dynlibs for dependencies, otherwise we get into duplicate symbol trouble again.

Specifically, the logic implemented in Nix is:

  • precompilePackage defaults to precompileModules
  • If a package does not request precompilation, but a dependency of it does, precompilePackage is automatically used. I.e. std4 would be precompiled as a package even if mathlib4 requests a finer-grained setup for itself.
  • precompilePackage does not affect compilation within the package; but if any module of the package is loaded from another package, the whole package dynlib is loaded.

Metadata

Metadata

Assignees

No one assigned

    Labels

    LakeLake related issueP-lowWe are not planning to work on this issueenhancementNew feature or request

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions