Lemmas about `private` defs are not `private` by default

YaelDillies commented 3 months ago

First, I am not sure whether this should be a RFC or a bug report. The current behavior is confusing and seemingly has no use cases, which is why I have opted for a bug report.

Prerequisites

Please put an X between the brackets as you perform the following steps:

[x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues
[x] Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to Mathlib or Batteries.
[x] Test your test case against the latest nightly release, for example on https://live.lean-lang.org/#project=lean-nightly (You can also use the settings there to switch to “Lean nightly”)

Description

Lemmas about private definitions are not private by default. One needs to add the private keyword explicitly.

Context

I keep forgetting that this is the current behavior, so I sometimes accidentally add non-private lemmas about private definitions to Mathlib, the latest in date being https://github.com/leanprover-community/mathlib4/pull/15000.

Steps to Reproduce

Consider the following MWE

private def foo : Nat := 0

theorem foo_eq_zero : foo = 0 := rfl

#print foo -- `foo` is `private`
#print foo_eq_zero -- `foo_eq_zero` is not

Expected behavior: foo_eq_zero is private Actual behavior: foo_eq_zero is not private

Versions

4.11.0-nightly-2024-08-11"

Impact

Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.

digama0 commented 3 months ago

I don't think the current behavior should change - if you don't make it private yourself then it shouldn't be private, but the example looks like a good reason for a linter warning to trigger (EDIT: or, as sebastian points out below, an error inside an abstract module), and that's exactly what rust does as well:

struct Foo;
pub fn foo() -> Foo { Foo }
fn main() {}

    Checking rust-test v0.1.0 (/home/mario/Documents/rust-test)
warning: type `Foo` is more private than the item `foo`
 --> src/main.rs:2:1
  |
2 | pub fn foo() -> Foo { Foo }
  | ^^^^^^^^^^^^^^^^^^^ function `foo` is reachable at visibility `pub`
  |
note: but type `Foo` is only usable at visibility `pub(crate)`
 --> src/main.rs:1:1
  |
1 | struct Foo;
  | ^^^^^^^^^^
  = note: `#[warn(private_interfaces)]` on by default

warning: `rust-test` (bin "rust-test") generated 1 warning
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.06s

Kha commented 3 months ago

This would likely be enforced when you opt into #416 in the future

leanprover / lean4