feat: do not export def bodies by default (#8221)

This PR adjusts the experimental module system to not export the bodies
of `def`s unless opted out by the new attribute `@[expose]` on the `def`
or on a surrounding `section`.

---------

Co-authored-by: Markus Himmel <[email protected]>

Author: Kha

script/benchReelabRss.lean

@@ -8,12 +8,12 @@ open Lean.JsonRpc
 Tests language server memory use by repeatedly re-elaborate a given file.
 
 NOTE: only works on Linux for now.
-ot to touch the imports for usual files.
 -/
 
 def main (args : List String) : IO Unit := do
   let leanCmd :: file :: iters :: args := args | panic! "usage: script <lean> <file> <#iterations> <server-args>..."
-  let uri := s!"file:///{file}"
+  let file ← IO.FS.realPath file
+  let uri := s!"file://{file}"
   Ipc.runWith leanCmd (#["--worker", "-DstderrAsMessages=false"] ++ args ++ #[uri]) do
   -- for use with heaptrack:
   --Ipc.runWith "heaptrack" (#[leanCmd, "--worker", "-DstderrAsMessages=false"] ++ args ++ #[uri]) do

src/Init/BinderNameHint.lean

@@ -40,5 +40,5 @@ This gadget is supported by
 It is ineffective in other positions (hyptheses of rewrite rules) or when used by other tactics
 (e.g. `apply`).
 -/
-@[simp ↓]
+@[simp ↓, expose]
 def binderNameHint {α : Sort u} {β : Sort v} {γ : Sort w} (v : α) (binder : β) (e : γ) : γ := e

src/Init/Control/Except.lean

@@ -127,7 +127,7 @@ end Except
 /--
 Adds exceptions of type `ε` to a monad `m`.
 -/
-def ExceptT (ε : Type u) (m : Type u → Type v) (α : Type u) : Type v :=
+@[expose] def ExceptT (ε : Type u) (m : Type u → Type v) (α : Type u) : Type v :=
   m (Except ε α)
 
 /--

src/Init/Control/ExceptCps.lean

@@ -18,7 +18,7 @@ Adds exceptions of type `ε` to a monad `m`.
 Instead of using `Except ε` to model exceptions, this implementation uses continuation passing
 style. This has different performance characteristics from `ExceptT ε`.
 -/
-def ExceptCpsT (ε : Type u) (m : Type u → Type v) (α : Type u) := (β : Type u) → (α → m β) → (ε → m β) → m β
+@[expose] def ExceptCpsT (ε : Type u) (m : Type u → Type v) (α : Type u) := (β : Type u) → (α → m β) → (ε → m β) → m β
 
 namespace ExceptCpsT
 

src/Init/Control/Id.lean

@@ -34,7 +34,7 @@ def containsFive (xs : List Nat) : Bool := Id.run do
 true
 ```
 -/
-def Id (type : Type u) : Type u := type
+@[expose] def Id (type : Type u) : Type u := type
 
 namespace Id
 
@@ -56,7 +56,7 @@ Runs a computation in the identity monad.
 This function is the identity function. Because its parameter has type `Id α`, it causes
 `do`-notation in its arguments to use the `Monad Id` instance.
 -/
-@[always_inline, inline]
+@[always_inline, inline, expose]
 protected def run (x : Id α) : α := x
 
 instance [OfNat α n] : OfNat (Id α) n :=

src/Init/Control/Lawful/Instances.lean

@@ -7,7 +7,8 @@ module
 
 prelude
 import Init.Control.Lawful.Basic
-import Init.Control.Except
+import all Init.Control.Except
+import all Init.Control.State
 import Init.Control.StateRef
 import Init.Ext
 
@@ -98,7 +99,7 @@ end ExceptT
 
 instance : LawfulMonad (Except ε) := LawfulMonad.mk'
   (id_map := fun x => by cases x <;> rfl)
-  (pure_bind := fun _ _ => rfl)
+  (pure_bind := fun _ _ => by rfl)
   (bind_assoc := fun a _ _ => by cases a <;> rfl)
 
 instance : LawfulApplicative (Except ε) := inferInstance
@@ -247,7 +248,7 @@ instance : LawfulMonad (EStateM ε σ) := .mk'
     match x s with
     | .ok _ _ => rfl
     | .error _ _ => rfl)
-  (pure_bind := fun _ _ => rfl)
+  (pure_bind := fun _ _ => by rfl)
   (bind_assoc := fun x _ _ => funext <| fun s => by
     dsimp only [EStateM.instMonad, EStateM.bind]
     match x s with

src/Init/Control/Option.lean

@@ -20,7 +20,7 @@ instance : ToBool (Option α) := ⟨Option.isSome⟩
 Adds the ability to fail to a monad. Unlike ordinary exceptions, there is no way to signal why a
 failure occurred.
 -/
-def OptionT (m : Type u → Type v) (α : Type u) : Type v :=
+@[expose] def OptionT (m : Type u → Type v) (α : Type u) : Type v :=
   m (Option α)
 
 /--

src/Init/Control/State.lean

@@ -22,7 +22,7 @@ Adds a mutable state of type `σ` to a monad.
 Actions in the resulting monad are functions that take an initial state and return, in `m`, a tuple
 of a value and a state.
 -/
-def StateT (σ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
+@[expose] def StateT (σ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
   σ → m (α × σ)
 
 /--
@@ -47,7 +47,7 @@ A tuple-based state monad.
 Actions in `StateM σ` are functions that take an initial state and return a value paired with a
 final state.
 -/
-@[reducible]
+@[expose, reducible]
 def StateM (σ α : Type u) : Type u := StateT σ Id α
 
 instance {σ α} [Subsingleton σ] [Subsingleton α] : Subsingleton (StateM σ α) where

src/Init/Control/StateCps.lean

@@ -18,7 +18,7 @@ The State monad transformer using CPS style.
 An alternative implementation of a state monad transformer that internally uses continuation passing
 style instead of tuples.
 -/
-def StateCpsT (σ : Type u) (m : Type u → Type v) (α : Type u) := (δ : Type u) → σ → (α → σ → m δ) → m δ
+@[expose] def StateCpsT (σ : Type u) (m : Type u → Type v) (α : Type u) := (δ : Type u) → σ → (α → σ → m δ) → m δ
 
 namespace StateCpsT
 

src/Init/Control/StateRef.lean

@@ -17,7 +17,7 @@ A state monad that uses an actual mutable reference cell (i.e. an `ST.Ref ω σ`
 
 The macro `StateRefT σ m α` infers `ω` from `m`. It should normally be used instead.
 -/
-def StateRefT' (ω : Type) (σ : Type) (m : Type → Type) (α : Type) : Type := ReaderT (ST.Ref ω σ) m α
+@[expose] def StateRefT' (ω : Type) (σ : Type) (m : Type → Type) (α : Type) : Type := ReaderT (ST.Ref ω σ) m α
 
 /-! Recall that `StateRefT` is a macro that infers `ω` from the `m`. -/