lambdapi
lambdapi copied to clipboard
Optimize loading mechanism in lambdapi
When requiring a module A which itself requires another module B, then B itself is loaded: https://github.com/Deducteam/lambdapi/blob/557de40f483080df08e6e3f2e1e44ffe3feb5a8b/src/handle/compile.ml#L75 even if what is exported from A may not actually depend on B. Some static analysis is necessary to know what dependency actually needs to be loaded. For instance, A may contain an opaque symbol (theorem) whose definition (proof) may depend on B symbols or rules but whose statement does not.