Skip to content
This repository was archived by the owner on Oct 25, 2023. It is now read-only.

Imports are only precompiled if importer is set to precompiled #83

Closed
tydeu opened this issue Jun 23, 2022 · 0 comments
Closed

Imports are only precompiled if importer is set to precompiled #83

tydeu opened this issue Jun 23, 2022 · 0 comments
Labels
bug Something isn't working
Milestone

Comments

@tydeu
Copy link
Member

tydeu commented Jun 23, 2022

From precompileModules documentation:

Whether to compile each module into a native shared library that is loaded whenever the module is imported

The last part doesn't seem to be the case currently. If I enable precompilation for Aesop (a prime example for a library-level precompilation use case btw) and then import it into my project which does not have precompilation enabled, no Aesop dynlibs are loaded.

Originally posted by @Kha in #47 (comment)

@tydeu tydeu added the bug Something isn't working label Jun 23, 2022
@tydeu tydeu added this to the v3.2.0 milestone Jun 23, 2022
@tydeu tydeu closed this as completed in cc23002 Jun 24, 2022
Kha pushed a commit to Kha/lean4 that referenced this issue Jul 17, 2023
Kha pushed a commit to Kha/lean4 that referenced this issue Jul 17, 2023
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
bug Something isn't working
Projects
None yet
Development

No branches or pull requests

1 participant