fix: mark exported stubs of `partial` definitions as unsafe This PR fixes a soundness bug in the module system. A `partial` definition lost its `partial` marking when it crossed a module boundary, so downstream modules could use it from safe declarations. Again, this issue can only be exploited using metaprogramming. When a module exports a definition whose body stays private, `addDeclCore` publishes an axiom stub in its place. The stub's `isUnsafe` flag was computed as `defn.safety == .unsafe`, which is false for `DefinitionSafety.partial`, so a `partial` definition was summarized as an ordinary safe axiom. The fix computes it as `defn.safety != .safe` instead.
This is the repository for Lean 4.
See Install Lean.
Please read our Contribution Guidelines first.
See Building Lean.