5bb9839887
This PR prevents symbol clashes between (non-`@[export]`) definitions from different Lean packages. Previously, if two modules define a function with the same name and were transitively imported (even privately) by some downstream module, linking would fail due to a symbol clash. Similarly, if a user defined a symbol with the same name as one in the `Lean` library, Lean would use the core symbol even if one did not import `Lean`. This is solved by changing Lean's name mangling algorithm to include an optional package identifier. This identifier is provided by Lake via `--setup` when building a module. This information is weaved through the elaborator, interpreter, and compiler via a persistent environment extension that associates modules with their package identifier. With a package identifier, standard symbols have the form `lp_<pkg-id>_<mangled-def>`. Without one, the old scheme is used (i.e., `l_<mangled-def>`). Module initializers are also prefixed with package identifier (if any). For example, the initializer for a module `Foo` in a package `test` is now `initialize_test_Foo` (instead of `initialize_Foo`). Lake's default for native library names has also been adjusted accordingly, so that libraries can still, by default, be used as plugins. Thus, the default library name of the `lean_lib Foo` in `package test` will now be `libtest_Foo`. When using Lake to build the Lean core (i.e., `bootstrap = true`), no package identifier will be used. Thus, definitions in user packages can never have symbol clashes with core. Closes #222. |
||
|---|---|---|
| .. | ||
| dev | ||
| examples | ||
| images | ||
| latex | ||
| make | ||
| std | ||
| .gitignore | ||
| BoolExpr.lean | ||
| metaprogramming-arith.lean | ||
| perf.md | ||
| README.md | ||
| style.md | ||
| syntax_example.lean | ||
Developer Documentation and Examples
This directory contains documentation that describes how to work on
Lean itself, as well as examples that are included in documentation
that's hosted on the Lean website. The make directory contains
information on building Lean, and the dev directory describes how to
work on Lean.
The documentation section has links to documentation that describes how to use Lean itself.