Merge branch 'master' of https://github.com/leanprover/lean4 into async-kernel

Author: Kha

doc/dev/release_checklist.md

@@ -147,16 +147,10 @@ We'll use `v4.7.0-rc1` as the intended release version in this example.
   - You can monitor this at `https://github.com/leanprover/lean4/actions/workflows/ci.yml`, looking for the `v4.7.0-rc1` tag.
   - This step can take up to an hour.
 - (GitHub release notes) Once the release appears at https://github.com/leanprover/lean4/releases/
-  - Edit the release notes on Github to select the "Set as a pre-release box".
-  - If release notes have been written already, copy the section of `RELEASES.md` for this version into the Github release notes
-    and use the title "Changes since v4.6.0 (from RELEASES.md)".
-  - Otherwise, in the "previous tag" dropdown, select `v4.6.0`, and click "Generate release notes".
+  - Verify that the release is marked as a prerelease (this should have been done automatically by the CI release job).
+  - In the "previous tag" dropdown, select `v4.6.0`, and click "Generate release notes".
     This will add a list of all the commits since the last stable version.
-    - Delete anything already mentioned in the hand-written release notes above.
     - Delete "update stage0" commits, and anything with a completely inscrutable commit message.
-    - Briefly rearrange the remaining items by category (e.g. `simp`, `lake`, `bug fixes`),
-      but for minor items don't put any work in expanding on commit messages.
-  - (How we want to release notes to look is evolving: please update this section if it looks wrong!)
 - Next, we will move a curated list of downstream repos to the release candidate.
   - This assumes that there is already a *reviewed* branch `bump/v4.7.0` on each repository
     containing the required adaptations (or no adaptations are required).

src/Init/Data/BitVec/Basic.lean

@@ -20,6 +20,8 @@ We define many of the bitvector operations from the
 of SMT-LIBv2.
 -/
 
+set_option linter.missingDocs true
+
 /--
 A bitvector of the specified width.
 
@@ -34,9 +36,9 @@ structure BitVec (w : Nat) where
   O(1), because we use `Fin` as the internal representation of a bitvector. -/
   toFin : Fin (2^w)
 
-@[deprecated (since := "2024-04-12")]
-protected abbrev Std.BitVec := _root_.BitVec
-
+/--
+Bitvectors have decidable equality. This should be used via the instance `DecidableEq (BitVec n)`.
+-/
 -- We manually derive the `DecidableEq` instances for `BitVec` because
 -- we want to have builtin support for bit-vector literals, and we
 -- need a name for this function to implement `canUnfoldAtMatcher` at `WHNF.lean`.

src/Init/Data/BitVec/Bitblast.lean

@@ -28,6 +28,8 @@ https://github.com/mhk119/lean-smt/blob/bitvec/Smt/Data/Bitwise.lean.
 
 -/
 
+set_option linter.missingDocs true
+
 open Nat Bool
 
 namespace Bool

src/Init/Data/BitVec/Folds.lean

@@ -8,6 +8,8 @@ import Init.Data.BitVec.Lemmas
 import Init.Data.Nat.Lemmas
 import Init.Data.Fin.Iterate
 
+set_option linter.missingDocs true
+
 namespace BitVec
 
 /--

src/Init/Data/BitVec/Lemmas.lean

@@ -12,6 +12,8 @@ import Init.Data.Nat.Lemmas
 import Init.Data.Nat.Mod
 import Init.Data.Int.Bitwise.Lemmas
 
+set_option linter.missingDocs true
+
 namespace BitVec
 
 /--

src/Init/Data/Int/Basic.lean

@@ -322,8 +322,8 @@ protected def pow (m : Int) : Nat → Int
   | 0      => 1
   | succ n => Int.pow m n * m
 
-instance : HPow Int Nat Int where
-  hPow := Int.pow
+instance : NatPow Int where
+  pow := Int.pow
 
 instance : LawfulBEq Int where
   eq_of_beq h := by simp [BEq.beq] at h; assumption

src/Lean/Elab/Frontend.lean

@@ -88,7 +88,7 @@ deriving Nonempty
 
 open Language in
 /--
-Variant of `IO.processCommands` that allows for potential incremental reuse. Pass in result of a
+Variant of `IO.processCommands` that allows for potential incremental reuse. Pass in the result of a
 previous invocation done with the same state (but usually different input context) to allow for
 reuse.
 -/
@@ -131,47 +131,6 @@ def process (input : String) (env : Environment) (opts : Options) (fileName : Op
   let s ← IO.processCommands inputCtx { : Parser.ModuleParserState } (Command.mkState env {} opts)
   pure (s.commandState.env, s.commandState.messages)
 
-/--
-Parses values of options registered during import and left by the C++ frontend as strings, fails if
-any option names remain unknown.
--/
-def reparseOptions (opts : Options) : IO Options := do
-  let mut opts := opts
-  let decls ← getOptionDecls
-  for (name, val) in opts do
-    let .ofString val := val
-      | continue  -- Already parsed by C++
-    -- Options can be prefixed with `weak` in order to turn off the error when the option is not
-    -- defined
-    let weak := name.getRoot == `weak
-    if weak then
-      opts := opts.erase name
-    let name := name.replacePrefix `weak Name.anonymous
-    let some decl := decls.find? name
-      | unless weak do
-          throw <| .userError s!"invalid -D parameter, unknown configuration option '{name}'
-
-If the option is defined in this library, use '-D{`weak ++ name}' to set it conditionally"
-
-    match decl.defValue with
-    | .ofBool _ =>
-      match val with
-      | "true"  => opts := opts.insert name true
-      | "false" => opts := opts.insert name false
-      | _ =>
-        throw <| .userError s!"invalid -D parameter, invalid configuration option '{val}' value, \
-          it must be true/false"
-    | .ofNat _ =>
-      let some val := val.toNat?
-        | throw <| .userError s!"invalid -D parameter, invalid configuration option '{val}' value, \
-            it must be a natural number"
-      opts := opts.insert name val
-    | .ofString _ => opts := opts.insert name val
-    | _ => throw <| .userError s!"invalid -D parameter, configuration option '{name}' \
-              cannot be set in the command line, use set_option command"
-
-  return opts
-
 @[export lean_run_frontend]
 def runFrontend
     (input : String)

src/Lean/Elab/MutualDef.lean

@@ -323,6 +323,10 @@ private def declValToTerminationHint (declVal : Syntax) : TermElabM TerminationH
   else
     return .none
 
+def instantiateMVarsProfiling (e : Expr) : MetaM Expr := do
+  profileitM Exception s!"instantiate metavars" (← getOptions) do
+    instantiateMVars e
+
 private def elabFunValues (headers : Array DefViewElabHeader) : TermElabM (Array Expr) :=
   headers.mapM fun header => do
     let mut reusableResult? := none
@@ -348,7 +352,7 @@ private def elabFunValues (headers : Array DefViewElabHeader) : TermElabM (Array
           elabTermEnsuringType valStx type <* synthesizeSyntheticMVarsNoPostponing
         -- NOTE: without this `instantiatedMVars`, `mkLambdaFVars` may leave around a redex that
         -- leads to more section variables being included than necessary
-        let val ← instantiateMVars val
+        let val ← instantiateMVarsProfiling val
         mkLambdaFVars xs val
     if let some snap := header.bodySnap? then
       snap.new.resolve <| some {
@@ -389,7 +393,7 @@ private def instantiateMVarsAtHeader (header : DefViewElabHeader) : TermElabM De
 
 private def instantiateMVarsAtLetRecToLift (toLift : LetRecToLift) : TermElabM LetRecToLift := do
   let type ← instantiateMVars toLift.type
-  let val ← instantiateMVars toLift.val
+  let val ← instantiateMVarsProfiling toLift.val
   pure { toLift with type, val }
 
 private def typeHasRecFun (type : Expr) (funFVars : Array Expr) (letRecsToLift : List LetRecToLift) : Option FVarId :=
@@ -597,7 +601,7 @@ private def pickMaxFVar? (lctx : LocalContext) (fvarIds : Array FVarId) : Option
   fvarIds.getMax? fun fvarId₁ fvarId₂ => (lctx.get! fvarId₁).index < (lctx.get! fvarId₂).index
 
 private def preprocess (e : Expr) : TermElabM Expr := do
-  let e ← instantiateMVars e
+  let e ← instantiateMVarsProfiling e
   -- which let-decls are dependent. We say a let-decl is dependent if its lambda abstraction is type incorrect.
   Meta.check e
   pure e
@@ -708,7 +712,7 @@ private def mkLetRecClosures (sectionVars : Array Expr) (mainFVarIds : Array FVa
       -- This can happen when this particular let-rec has nested let-rec that have been resolved in previous iterations.
       -- This code relies on the fact that nested let-recs occur before the outer most let-recs at `letRecsToLift`.
       -- Unresolved nested let-recs appear as metavariables before they are resolved. See `assignExprMVar` at `mkLetRecClosureFor`
-      let valNew ← instantiateMVars letRecsToLift[i]!.val
+      let valNew ← instantiateMVarsProfiling letRecsToLift[i]!.val
       letRecsToLift := letRecsToLift.modify i fun t => { t with val := valNew }
       -- We have to recompute the `freeVarMap` in this case. This overhead should not be an issue in practice.
       freeVarMap ← mkFreeVarMap sectionVars mainFVarIds recFVarIds letRecsToLift
@@ -821,10 +825,10 @@ def main (sectionVars : Array Expr) (mainHeaders : Array DefViewElabHeader) (mai
     let letRecsToLift ← letRecsToLift.mapM fun toLift => withLCtx toLift.lctx toLift.localInstances do
       Meta.check toLift.type
       Meta.check toLift.val
-      return { toLift with val := (← instantiateMVars toLift.val), type := (← instantiateMVars toLift.type) }
+      return { toLift with val := (← instantiateMVarsProfiling toLift.val), type := (← instantiateMVars toLift.type) }
     let letRecClosures ← mkLetRecClosures sectionVars mainFVarIds recFVarIds letRecsToLift
     -- mkLetRecClosures assign metavariables that were placeholders for the lifted declarations.
-    let mainVals    ← mainVals.mapM (instantiateMVars ·)
+    let mainVals    ← mainVals.mapM (instantiateMVarsProfiling ·)
     let mainHeaders ← mainHeaders.mapM instantiateMVarsAtHeader
     let letRecClosures ← letRecClosures.mapM fun closure => do pure { closure with toLift := (← instantiateMVarsAtLetRecToLift closure.toLift) }
     -- Replace fvarIds for functions being defined with closed terms
@@ -927,7 +931,7 @@ where
           try
             let values ← elabFunValues headers
             Term.synthesizeSyntheticMVarsNoPostponing
-            values.mapM (instantiateMVars ·)
+            values.mapM (instantiateMVarsProfiling ·)
           catch ex =>
             logException ex
             headers.mapM fun header => mkSorry header.type (synthetic := true)
@@ -961,7 +965,7 @@ where
                   data := e.toMessageData opts
                 }
               typeCheckedPromise.resolve <|
-                .mk { diagnostics := (← Snapshot.Diagnostics.ofMessageLog msgLog) } #[])
+                .mk { diagnostics := (← Snapshot.Diagnostics.ofMessageLog msgLog) } #[]
           processDeriving headers
       for view in views, header in headers do
         -- NOTE: this should be the full `ref`, and thus needs to be done after any snapshotting

src/Lean/Elab/PreDefinition/Basic.lean

@@ -7,6 +7,9 @@ prelude
 import Init.ShareCommon
 import Lean.Compiler.NoncomputableAttr
 import Lean.Util.CollectLevelParams
+import Lean.Util.NumObjs
+import Lean.Util.NumApps
+import Lean.PrettyPrinter
 import Lean.Meta.AbstractNestedProofs
 import Lean.Meta.ForEachExpr
 import Lean.Elab.RecAppSyntax
@@ -17,7 +20,6 @@ namespace Lean.Elab
 open Meta
 open Term
 
-
 /--
   A (potentially recursive) definition.
   The elaborator converts it into Kernel definitions using many different strategies.
@@ -98,15 +100,33 @@ private def compileDecl (decl : Declaration) : TermElabM Bool := do
       throw ex
   return true
 
+register_builtin_option diagnostics.threshold.proofSize : Nat := {
+  defValue := 16384
+  group    := "diagnostics"
+  descr    := "only display proof statistics when proof has at least this number of terms"
+}
+
+private def reportTheoremDiag (d : TheoremVal) : TermElabM Unit := do
+  if (← isDiagnosticsEnabled) then
+    let proofSize ← d.value.numObjs
+    if proofSize > diagnostics.threshold.proofSize.get (← getOptions) then
+      let sizeMsg := MessageData.trace { cls := `size } m!"{proofSize}" #[]
+      let constOccs ← d.value.numApps (threshold := diagnostics.threshold.get (← getOptions))
+      let constOccsMsg ← constOccs.mapM fun (declName, numOccs) => return MessageData.trace { cls := `occs } m!"{MessageData.ofConst (← mkConstWithLevelParams declName)} ↦ {numOccs}" #[]
+      -- let info
+      logInfo <| MessageData.trace { cls := `theorem } m!"{d.name}" (#[sizeMsg] ++ constOccsMsg)
+
 private def addNonRecAux (preDef : PreDefinition) (compile : Bool) (all : List Name) (applyAttrAfterCompilation := true) : TermElabM Unit :=
   withRef preDef.ref do
     let preDef ← abstractNestedProofs preDef
     let decl ←
       match preDef.kind with
       | DefKind.«theorem» =>
-        pure <| Declaration.thmDecl {
+        let d := {
           name := preDef.declName, levelParams := preDef.levelParams, type := preDef.type, value := preDef.value, all
         }
+        reportTheoremDiag d
+        pure <| Declaration.thmDecl d
       | DefKind.«opaque»  =>
         pure <| Declaration.opaqueDecl {
           name := preDef.declName, levelParams := preDef.levelParams, type := preDef.type, value := preDef.value

src/Lean/Elab/PreDefinition/Main.lean

@@ -151,12 +151,8 @@ def shouldUseWF (preDefs : Array PreDefinition) : Bool :=
     preDef.termination.terminationBy? matches some {structural := false, ..} ||
     preDef.termination.decreasingBy?.isSome
 
-/--
-Checks the given pre-definitions in the kernel and adds them to the environment. If `postponeCheck`
-is `true`, the kernel check may be postponed, in which case the environment and declaration are
-returned on which `Environment.addDecl` should be called at some later point to perform the check.
--/
-def addPreDefinitionsCore (preDefs : Array PreDefinition) (postponeCheck := false) : TermElabM (Option (Environment × Declaration)) := withLCtx {} {} do
+private def addPreDefinitionsCore (preDefs : Array PreDefinition) (postponeCheck : Bool) :
+    TermElabM (Option (Environment × Declaration)) := withLCtx {} {} do
   profileitM Exception "process pre-definitions" (← getOptions) do
     withTraceNode `Elab.def.processPreDef (fun _ => return m!"process pre-definitions") do
       for preDef in preDefs do
@@ -231,9 +227,20 @@ def addPreDefinitionsCore (preDefs : Array PreDefinition) (postponeCheck := fals
             catch _ => s.restore
       return none
 
+/-- Checks the given pre-definitions in the kernel and adds them to the environment. -/
 def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit :=
   addPreDefinitionsCore preDefs (postponeCheck := false) |> discard
 
+/--
+Checks the given pre-definitions in the kernel and adds them to the environment. Depending on the
+involved definitions, the kernel check may be postponed, in which case the environment and
+declaration are returned on which `Environment.addDecl` should be called at some later point to
+perform the check.
+-/
+def addPreDefinitionsWithPostpone (preDefs : Array PreDefinition) :
+    TermElabM (Option (Environment × Declaration)) :=
+  addPreDefinitionsCore preDefs (postponeCheck := true)
+
 builtin_initialize
   registerTraceClass `Elab.definition.body
   registerTraceClass `Elab.definition.scc

src/Lean/Expr.lean

@@ -1452,28 +1452,26 @@ partial def betaRev (f : Expr) (revArgs : Array Expr) (useZeta := false) (preser
   else
     let sz := revArgs.size
     let rec go (e : Expr) (i : Nat) : Expr :=
+      let done (_ : Unit) : Expr :=
+        let n := sz - i
+        mkAppRevRange (e.instantiateRange n sz revArgs) 0 n revArgs
       match e with
-      | Expr.lam _ _ b _ =>
+      | .lam _ _ b _ =>
         if i + 1 < sz then
           go b (i+1)
         else
-          let n := sz - (i + 1)
-          mkAppRevRange (b.instantiateRange n sz revArgs) 0 n revArgs
-      | Expr.letE _ _ v b _ =>
+          b.instantiate revArgs
+      | .letE _ _ v b _ =>
         if useZeta && i < sz then
           go (b.instantiate1 v) i
         else
-          let n := sz - i
-          mkAppRevRange (e.instantiateRange n sz revArgs) 0 n revArgs
-      | Expr.mdata k b =>
+          done ()
+      | .mdata _ b =>
         if preserveMData then
-          let n := sz - i
-          mkMData k (mkAppRevRange (b.instantiateRange n sz revArgs) 0 n revArgs)
+          done ()
         else
           go b i
-      | b =>
-        let n := sz - i
-        mkAppRevRange (b.instantiateRange n sz revArgs) 0 n revArgs
+      | _ => done ()
     go f 0
 
 /--