fix test

Suggestion on
[Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.23guard_msgs.20variant.3A.20don't.20care.20about.20whitespace/near/434906526)

.github/workflows/check-stage0.yml

@@ -0,0 +1,27 @@
+name: Check for stage0 updates on the merge queue
+
+# We only want to run this on merge_group checks, but github uses the same
+# list of requires checks for PR → queue and queue → master, so
+# this needs to run (without doing anything) for pull_request as well.
+on:
+  merge_group:
+  pull_request:
+
+jobs:
+  check-stage0-on-queue:
+    runs-on: ubuntu-latest
+    if: github.event_name == 'merge_group'
+    steps:
+    - uses: actions/checkout@v4
+      with:
+        ref: ${{ github.event.pull_request.head.sha }}
+        filter: blob:none
+        fetch-depth: 2
+    - run: |
+        if git diff HEAD^..HEAD --name-only -- stage0 |
+          grep -q -v -x -F $'stage0/src/stdlib_flags.h\nstage0/src/lean.mk.in'
+        then
+          echo "Found changes to stage0/, please do not merge using the merge queue." | tee "$GITHUB_STEP_SUMMARY"
+          exit 1
+        fi
+      shell: bash

CODEOWNERS

@@ -21,11 +21,6 @@
 /src/Lean/Server/ @mhuisi
 /src/Lean/Widget/ @Vtec234
 /src/runtime/io.cpp @joehendrix
-/src/Init/Data/ @semorrison
-/src/Init/Data/Array/Lemmas.lean @digama0
-/src/Init/Data/List/Lemmas.lean @digama0
-/src/Init/Data/List/BasicAux.lean @digama0
-/src/Init/Data/Array/Subarray.lean @david-christiansen
 /src/Lean/Elab/Tactic/RCases.lean @digama0
 /src/Init/RCases.lean @digama0
 /src/Lean/Elab/Tactic/Ext.lean @digama0
@@ -44,4 +39,5 @@
 /src/Lean/Elab/Tactic/Guard.lean @digama0
 /src/Init/Guard.lean @digama0
 /src/Lean/Server/CodeActions/ @digama0
+/src/Init/Data/Array/Subarray.lean @david-christiansen
 

RELEASES.md

@@ -79,9 +79,9 @@ v4.8.0 (development in progress)
   Field notation can be disabled on a function-by-function basis using the `@[pp_nodot]` attribute.
 
 * Added options `pp.mvars` (default: true) and `pp.mvars.withType` (default: false).
-  When `pp.mvars` is false, metavariables pretty print as `?_`,
-  and when `pp.mvars.withType` is true, metavariables pretty print with a type ascription.
-  These can be set when using `#guard_msgs` to make tests not rely on the unique ids assigned to anonymous metavariables.
+  When `pp.mvars` is false, expression metavariables pretty print as `?_` and universe metavariables pretty print as `_`.
+  When `pp.mvars.withType` is true, expression metavariables pretty print with a type ascription.
+  These can be set when using `#guard_msgs` to make tests not depend on the particular names of metavariables.
   [#3798](https://github.com/leanprover/lean4/pull/3798).
 
 * Added `@[induction_eliminator]` and `@[cases_eliminator]` attributes to be able to define custom eliminators

doc/examples/Certora2022/ex8.lean

@@ -4,16 +4,16 @@ def ack : Nat → Nat → Nat
   | 0,   y   => y+1
   | x+1, 0   => ack x 1
   | x+1, y+1 => ack x (ack (x+1) y)
-termination_by ack x y => (x, y)
+termination_by x y => (x, y)
 
 def sum (a : Array Int) : Int :=
   let rec go (i : Nat) :=
-     if i < a.size then
+     if _ : i < a.size then
         a[i] + go (i+1)
      else
         0
+  termination_by a.size - i
   go 0
-termination_by go i => a.size - i
 
 set_option pp.proofs true
 #print sum.go

doc/examples/ICERM2022/ctor.lean

@@ -4,43 +4,42 @@ open Lean Meta
 
 def ctor (mvarId : MVarId) (idx : Nat) : MetaM (List MVarId) := do
   /- Set `MetaM` context using `mvarId` -/
-  withMVarContext mvarId do 
+  mvarId.withContext do
     /- Fail if the metavariable is already assigned. -/
-    checkNotAssigned mvarId `ctor
+    mvarId.checkNotAssigned `ctor
     /- Retrieve the target type, instantiateMVars, and use `whnf`. -/
-    let target ← getMVarType' mvarId
+    let target ← mvarId.getType'
     let .const declName us := target.getAppFn
       | throwTacticEx `ctor mvarId "target is not an inductive datatype"
     let .inductInfo { ctors, .. } ← getConstInfo declName
       | throwTacticEx `ctor mvarId "target is not an inductive datatype"
     if idx = 0 then
-      throwTacticEx `ctor mvarId "invalid index, it must be > 0"  
+      throwTacticEx `ctor mvarId "invalid index, it must be > 0"
     else if h : idx - 1 < ctors.length then
-      apply mvarId (.const ctors[idx - 1] us)
+      mvarId.apply (.const ctors[idx - 1] us)
     else
-      throwTacticEx `ctor mvarId "invalid index, inductive datatype has only {ctors.length} contructors"  
+      throwTacticEx `ctor mvarId "invalid index, inductive datatype has only {ctors.length} contructors"
 
 open Elab Tactic
 
-elab "ctor" idx:num : tactic => 
+elab "ctor" idx:num : tactic =>
   liftMetaTactic (ctor · idx.getNat)
 
-example (p : Prop) : p := by 
+example (p : Prop) : p := by
   ctor 1 -- Error
 
-example (h : q) : p ∨ q := by 
+example (h : q) : p ∨ q := by
   ctor 0 -- Error
   exact h
 
-example (h : q) : p ∨ q := by 
+example (h : q) : p ∨ q := by
   ctor 3 -- Error
   exact h
 
-example (h : q) : p ∨ q := by 
+example (h : q) : p ∨ q := by
   ctor 2
   exact h
 
-example (h : q) : p ∨ q := by 
+example (h : q) : p ∨ q := by
   ctor 1
-  exact h -- Error 
-
+  exact h -- Error

doc/examples/ICERM2022/meta.lean

@@ -5,15 +5,15 @@ open Lean Meta
 def ex1 (declName : Name) : MetaM Unit := do
   let info ← getConstInfo declName
   IO.println s!"{declName} : {← ppExpr info.type}"
-  if let some val := info.value? then 
+  if let some val := info.value? then
     IO.println s!"{declName} : {← ppExpr val}"
-    
+
 #eval ex1 ``Nat
 
 def ex2 (declName : Name) : MetaM Unit := do
   let info ← getConstInfo declName
   trace[Meta.debug] "{declName} : {info.type}"
-  if let some val := info.value? then 
+  if let some val := info.value? then
     trace[Meta.debug] "{declName} : {val}"
 
 #eval ex2 ``Add.add
@@ -30,9 +30,9 @@ def ex3 (declName : Name) : MetaM Unit := do
       trace[Meta.debug] "{x} : {← inferType x}"
 
 def myMin [LT α] [DecidableRel (α := α) (·<·)] (a b : α) : α :=
-  if a < b then 
+  if a < b then
     a
-  else 
+  else
     b
 
 set_option trace.Meta.debug true in
@@ -40,7 +40,7 @@ set_option trace.Meta.debug true in
 
 def ex4 : MetaM Unit := do
   let nat := mkConst ``Nat
-  withLocalDeclD `a nat fun a => 
+  withLocalDeclD `a nat fun a =>
   withLocalDeclD `b nat fun b => do
     let e ← mkAppM ``HAdd.hAdd #[a, b]
     trace[Meta.debug] "{e} : {← inferType e}"
@@ -66,15 +66,17 @@ open Elab Term
 
 def ex5 : TermElabM Unit := do
   let nat := Lean.mkConst ``Nat
-  withLocalDeclD `a nat fun a => do 
+  withLocalDeclD `a nat fun a => do
   withLocalDeclD `b nat fun b => do
     let ab ← mkAppM ``HAdd.hAdd #[a, b]
-    let stx ← `(fun x => if x < 10 then $(← exprToSyntax ab) + x else x + $(← exprToSyntax a))
+    let abStx ← exprToSyntax ab
+    let aStx ← exprToSyntax a
+    let stx ← `(fun x => if x < 10 then $abStx + x else x + $aStx)
     let e ← elabTerm stx none
     trace[Meta.debug] "{e} : {← inferType e}"
     let e := mkApp e (mkNatLit 5)
     let e ← whnf e
     trace[Meta.debug] "{e}"
-       
+
 set_option trace.Meta.debug true in
 #eval ex5

doc/examples/NFM2022/nfm8.lean

@@ -4,16 +4,16 @@ def ack : Nat → Nat → Nat
   | 0,   y   => y+1
   | x+1, 0   => ack x 1
   | x+1, y+1 => ack x (ack (x+1) y)
-termination_by ack x y => (x, y)
+termination_by x y => (x, y)
 
 def sum (a : Array Int) : Int :=
   let rec go (i : Nat) :=
-     if i < a.size then
+     if _ : i < a.size then
         a[i] + go (i+1)
      else
         0
+  termination_by a.size - i
   go 0
-termination_by go i => a.size - i
 
 set_option pp.proofs true
 #print sum.go

src/Init/Data/Array/Lemmas.lean

@@ -5,7 +5,6 @@ Authors: Mario Carneiro
 -/
 prelude
 import Init.Data.Nat.MinMax
-import Init.Data.Nat.Lemmas
 import Init.Data.List.Lemmas
 import Init.Data.Fin.Basic
 import Init.Data.Array.Mem
@@ -188,8 +187,7 @@ theorem anyM_stop_le_start [Monad m] (p : α → m Bool) (as : Array α) (start
 theorem mem_def (a : α) (as : Array α) : a ∈ as ↔ a ∈ as.data :=
   ⟨fun | .mk h => h, Array.Mem.mk⟩
 
-/-! # get -/
-
+/-- # get -/
 @[simp] theorem get_eq_getElem (a : Array α) (i : Fin _) : a.get i = a[i.1] := rfl
 
 theorem getElem?_lt
@@ -219,7 +217,7 @@ theorem get!_eq_getD [Inhabited α] (a : Array α) : a.get! n = a.getD n default
 @[simp] theorem get!_eq_getElem? [Inhabited α] (a : Array α) (i : Nat) : a.get! i = (a.get? i).getD default := by
   by_cases p : i < a.size <;> simp [getD_get?, get!_eq_getD, p]
 
-/-! # set -/
+/-- # set -/
 
 @[simp] theorem getElem_set_eq (a : Array α) (i : Fin a.size) (v : α) {j : Nat}
       (eq : i.val = j) (p : j < (a.set i v).size) :
@@ -242,7 +240,7 @@ theorem getElem_set (a : Array α) (i : Fin a.size) (v : α) (j : Nat)
     (ne : i.val ≠ j) : (a.set i v)[j]? = a[j]? := by
   by_cases h : j < a.size <;> simp [getElem?_lt, getElem?_ge, Nat.ge_of_not_lt, ne, h]
 
-/-! # setD -/
+/- # setD -/
 
 @[simp] theorem set!_is_setD : @set! = @setD := rfl
 
@@ -268,44 +266,4 @@ theorem getElem?_setD_eq (a : Array α) {i : Nat} (p : i < a.size) (v : α) : (a
   by_cases h : i < a.size <;>
     simp [setD, Nat.not_lt_of_le, h,  getD_get?]
 
-/-! # ofFn -/
-
-@[simp] theorem size_ofFn_go {n} (f : Fin n → α) (i acc) :
-    (ofFn.go f i acc).size = acc.size + (n - i) := by
-  if hin : i < n then
-    unfold ofFn.go
-    have : 1 + (n - (i + 1)) = n - i :=
-      Nat.sub_sub .. ▸ Nat.add_sub_cancel' (Nat.le_sub_of_add_le (Nat.add_comm .. ▸ hin))
-    rw [dif_pos hin, size_ofFn_go f (i+1), size_push, Nat.add_assoc, this]
-  else
-    have : n - i = 0 := Nat.sub_eq_zero_of_le (Nat.le_of_not_lt hin)
-    unfold ofFn.go
-    simp [hin, this]
-termination_by n - i
-
-@[simp] theorem size_ofFn (f : Fin n → α) : (ofFn f).size = n := by simp [ofFn]
-
-theorem getElem_ofFn_go (f : Fin n → α) (i) {acc k}
-    (hki : k < n) (hin : i ≤ n) (hi : i = acc.size)
-    (hacc : ∀ j, ∀ hj : j < acc.size, acc[j] = f ⟨j, Nat.lt_of_lt_of_le hj (hi ▸ hin)⟩) :
-    haveI : acc.size + (n - acc.size) = n := Nat.add_sub_cancel' (hi ▸ hin)
-    (ofFn.go f i acc)[k]'(by simp [*]) = f ⟨k, hki⟩ := by
-  unfold ofFn.go
-  if hin : i < n then
-    have : 1 + (n - (i + 1)) = n - i :=
-      Nat.sub_sub .. ▸ Nat.add_sub_cancel' (Nat.le_sub_of_add_le (Nat.add_comm .. ▸ hin))
-    simp only [dif_pos hin]
-    rw [getElem_ofFn_go f (i+1) _ hin (by simp [*]) (fun j hj => ?hacc)]
-    cases (Nat.lt_or_eq_of_le <| Nat.le_of_lt_succ (by simpa using hj)) with
-    | inl hj => simp [get_push, hj, hacc j hj]
-    | inr hj => simp [get_push, *]
-  else
-    simp [hin, hacc k (Nat.lt_of_lt_of_le hki (Nat.le_of_not_lt (hi ▸ hin)))]
-termination_by n - i
-
-@[simp] theorem getElem_ofFn (f : Fin n → α) (i : Nat) (h) :
-    (ofFn f)[i] = f ⟨i, size_ofFn f ▸ h⟩ :=
-  getElem_ofFn_go _ _ _ (by simp) (by simp) nofun
-
-
 end Array

src/Init/Data/List/BasicAux.lean

@@ -5,7 +5,6 @@ Author: Leonardo de Moura
 -/
 prelude
 import Init.Data.Nat.Linear
-import Init.Ext
 
 universe u
 
@@ -44,14 +43,6 @@ See also `get?` and `get!`.
 def getD (as : List α) (i : Nat) (fallback : α) : α :=
   (as.get? i).getD fallback
 
-@[ext] theorem ext : ∀ {l₁ l₂ : List α}, (∀ n, l₁.get? n = l₂.get? n) → l₁ = l₂
-  | [], [], _ => rfl
-  | a :: l₁, [], h => nomatch h 0
-  | [], a' :: l₂, h => nomatch h 0
-  | a :: l₁, a' :: l₂, h => by
-    have h0 : some a = some a' := h 0
-    injection h0 with aa; simp only [aa, ext fun n => h (n+1)]
-
 /--
 Returns the first element in the list.
 

src/Init/Data/List/Lemmas.lean

@@ -274,19 +274,6 @@ theorem get?_reverse {l : List α} (i) (h : i < length l) :
 
 @[simp] theorem getD_cons_succ : getD (x :: xs) (n + 1) d = getD xs n d := rfl
 
-theorem ext_get {l₁ l₂ : List α} (hl : length l₁ = length l₂)
-    (h : ∀ n h₁ h₂, get l₁ ⟨n, h₁⟩ = get l₂ ⟨n, h₂⟩) : l₁ = l₂ :=
-  ext fun n =>
-    if h₁ : n < length l₁ then by
-      rw [get?_eq_get, get?_eq_get, h n h₁ (by rwa [← hl])]
-    else by
-      have h₁ := Nat.le_of_not_lt h₁
-      rw [get?_len_le h₁, get?_len_le]; rwa [← hl]
-
-@[simp] theorem get_map (f : α → β) {l n} :
-    get (map f l) n = f (get l ⟨n, length_map l f ▸ n.2⟩) :=
-  Option.some.inj <| by rw [← get?_eq_get, get?_map, get?_eq_get]; rfl
-
 /-! ### take and drop -/
 
 @[simp] theorem take_append_drop : ∀ (n : Nat) (l : List α), take n l ++ drop n l = l
@@ -404,14 +391,6 @@ theorem foldr_eq_foldrM (f : α → β → β) (b) (l : List α) :
 
 theorem foldr_self (l : List α) : l.foldr cons [] = l := by simp
 
-theorem foldl_map (f : β₁ → β₂) (g : α → β₂ → α) (l : List β₁) (init : α) :
-    (l.map f).foldl g init = l.foldl (fun x y => g x (f y)) init := by
-  induction l generalizing init <;> simp [*]
-
-theorem foldr_map (f : α₁ → α₂) (g : α₂ → β → β) (l : List α₁) (init : β) :
-    (l.map f).foldr g init = l.foldr (fun x y => g (f x) y) init := by
-  induction l generalizing init <;> simp [*]
-
 /-! ### mapM -/
 
 /-- Alternate (non-tail-recursive) form of mapM for proofs. -/

src/Init/Notation.lean

@@ -492,9 +492,12 @@ The attribute `@[deprecated]` on a declaration indicates that the declaration
 is discouraged for use in new code, and/or should be migrated away from in
 existing code. It may be removed in a future version of the library.
 
-`@[deprecated myBetterDef]` means that `myBetterDef` is the suggested replacement.
+* `@[deprecated myBetterDef]` means that `myBetterDef` is the suggested replacement.
+* `@[deprecated myBetterDef "use myBetterDef instead"]` allows customizing the deprecation message.
+* `@[deprecated (since := "2024-04-21")]` records when the deprecation was first applied.
 -/
-syntax (name := deprecated) "deprecated" (ppSpace ident)? : attr
+syntax (name := deprecated) "deprecated" (ppSpace ident)? (ppSpace str)?
+    (" (" &"since" " := " str ")")? : attr
 
 /--
 The `@[coe]` attribute on a function (which should also appear in a

src/Lean/Attributes.lean

@@ -183,7 +183,6 @@ structure ParametricAttribute (α : Type) where
   deriving Inhabited
 
 structure ParametricAttributeImpl (α : Type) extends AttributeImplCore where
-  /-- This is used as the target for go-to-definition queries for simple attributes -/
   getParam : Name → Syntax → AttrM α
   afterSet : Name → α → AttrM Unit := fun _ _ _ => pure ()
   afterImport : Array (Array (Name × α)) → ImportM Unit := fun _ => pure ()

src/Lean/Level.lean

@@ -428,15 +428,18 @@ def Result.imax : Result → Result → Result
   | f, Result.imaxNode Fs => Result.imaxNode (f::Fs)
   | f₁, f₂                => Result.imaxNode [f₁, f₂]
 
-def toResult : Level → Result
+def toResult (l : Level) (mvars : Bool) : Result :=
+  match l with
   | zero       => Result.num 0
-  | succ l     => Result.succ (toResult l)
-  | max l₁ l₂  => Result.max (toResult l₁) (toResult l₂)
-  | imax l₁ l₂ => Result.imax (toResult l₁) (toResult l₂)
+  | succ l     => Result.succ (toResult l mvars)
+  | max l₁ l₂  => Result.max (toResult l₁ mvars) (toResult l₂ mvars)
+  | imax l₁ l₂ => Result.imax (toResult l₁ mvars) (toResult l₂ mvars)
   | param n    => Result.leaf n
   | mvar n     =>
-    let n := n.name.replacePrefix `_uniq (Name.mkSimple "?u");
-    Result.leaf n
+    if mvars then
+      Result.leaf <| n.name.replacePrefix `_uniq (Name.mkSimple "?u")
+    else
+      Result.leaf `_
 
 private def parenIfFalse : Format → Bool → Format
   | f, true  => f
@@ -471,17 +474,17 @@ protected partial def Result.quote (r : Result) (prec : Nat) : Syntax.Level :=
 
 end PP
 
-protected def format (u : Level) : Format :=
-  (PP.toResult u).format true
+protected def format (u : Level) (mvars : Bool) : Format :=
+  (PP.toResult u mvars).format true
 
 instance : ToFormat Level where
-  format u := Level.format u
+  format u := Level.format u (mvars := true)
 
 instance : ToString Level where
-  toString u := Format.pretty (Level.format u)
+  toString u := Format.pretty (format u)
 
-protected def quote (u : Level) (prec : Nat := 0) : Syntax.Level :=
-  (PP.toResult u).quote prec
+protected def quote (u : Level) (prec : Nat := 0) (mvars : Bool := true) : Syntax.Level :=
+  (PP.toResult u (mvars := mvars)).quote prec
 
 instance : Quote Level `level where
   quote := Level.quote

src/Lean/Linter/Deprecated.lean

@@ -15,17 +15,23 @@ register_builtin_option linter.deprecated : Bool := {
   descr := "if true, generate deprecation warnings"
 }
 
-builtin_initialize deprecatedAttr : ParametricAttribute (Option Name) ←
+structure DeprecationEntry where
+  newName? : Option Name := none
+  text? : Option String := none
+  since? : Option String := none
+  deriving Inhabited
+
+builtin_initialize deprecatedAttr : ParametricAttribute DeprecationEntry ←
   registerParametricAttribute {
     name := `deprecated
     descr := "mark declaration as deprecated",
     getParam := fun _ stx => do
-     match stx with
-     | `(attr| deprecated $[$id?]?) =>
-       let some id := id? | return none
-       let declNameNew ← Elab.realizeGlobalConstNoOverloadWithInfo id
-       return some declNameNew
-     | _  => throwError "invalid `[deprecated]` attribute"
+      let `(attr| deprecated $[$id?]? $[$text?]? $[(since := $since?)]?) := stx
+        | throwError "invalid `[deprecated]` attribute"
+      let newName? ← id?.mapM Elab.realizeGlobalConstNoOverloadWithInfo
+      let text? := text?.map TSyntax.getString
+      let since? := since?.map TSyntax.getString
+      return { newName?, text?, since? }
   }
 
 def isDeprecated (env : Environment) (declName : Name) : Bool :=
@@ -34,12 +40,13 @@ def isDeprecated (env : Environment) (declName : Name) : Bool :=
 def _root_.Lean.MessageData.isDeprecationWarning (msg : MessageData) : Bool :=
   msg.hasTag (· == ``deprecatedAttr)
 
-def getDeprecatedNewName (env : Environment) (declName : Name) : Option Name :=
-  (deprecatedAttr.getParam? env declName).getD none
+def getDeprecatedNewName (env : Environment) (declName : Name) : Option Name := do
+  (← deprecatedAttr.getParam? env declName).newName?
 
 def checkDeprecated [Monad m] [MonadEnv m] [MonadLog m] [AddMessageContext m] [MonadOptions m] (declName : Name) : m Unit := do
   if getLinterValue linter.deprecated (← getOptions) then
-    match deprecatedAttr.getParam? (← getEnv) declName with
-    | none => pure ()
-    | some none => logWarning <| .tagged ``deprecatedAttr m!"`{declName}` has been deprecated"
-    | some (some newName) => logWarning <| .tagged ``deprecatedAttr m!"`{declName}` has been deprecated, use `{newName}` instead"
+    let some attr := deprecatedAttr.getParam? (← getEnv) declName | pure ()
+    logWarning <| .tagged ``deprecatedAttr <| attr.text?.getD <|
+      match attr.newName? with
+      | none => s!"`{declName}` has been deprecated"
+      | some newName => s!"`{declName}` has been deprecated, use `{newName}` instead"

src/Lean/Meta/ExprDefEq.lean

@@ -1757,10 +1757,21 @@ private def isDefEqDeltaStep (t s : Expr) : MetaM DeltaStepResult := do
     | .lt => unfold t (return .unknown) (k · s)
     | .gt => unfold s (return .unknown) (k t ·)
     | .eq =>
-      unfold t
-        (unfold s (return .unknown) (k t ·))
-        (fun t => unfold s (k t s) (k t ·))
+      -- Remark: if `t` and `s` are both some `f`-application, we use `tryHeuristic`
+      -- if `f` is not a projection. The projection case generates a performance regression.
+      if tInfo.name == sInfo.name && !(← isProjectionFn tInfo.name) then
+        if t.isApp && s.isApp && (← tryHeuristic t s) then
+          return .eq
+        else
+          unfoldBoth t s
+      else
+        unfoldBoth t s
 where
+  unfoldBoth (t s : Expr) : MetaM DeltaStepResult := do
+    unfold t
+      (unfold s (return .unknown) (k t ·))
+      (fun t => unfold s (k t s) (k t ·))
+
   k (t s : Expr) : MetaM DeltaStepResult := do
     let t ← whnfCore t
     let s ← whnfCore s

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -71,9 +71,11 @@ def delabSort : Delab := do
   match l with
   | Level.zero => `(Prop)
   | Level.succ .zero => `(Type)
-  | _ => match l.dec with
-    | some l' => `(Type $(Level.quote l' max_prec))
-    | none    => `(Sort $(Level.quote l max_prec))
+  | _ =>
+    let mvars ← getPPOption getPPMVars
+    match l.dec with
+    | some l' => `(Type $(Level.quote l' (prec := max_prec) (mvars := mvars)))
+    | none    => `(Sort $(Level.quote l (prec := max_prec) (mvars := mvars)))
 
 /--
 Delaborator for `const` expressions.
@@ -96,7 +98,8 @@ def delabConst : Delab := do
         c := c₀
     pure <| mkIdent c
   else
-    `($(mkIdent c).{$[$(ls.toArray.map quote)],*})
+    let mvars ← getPPOption getPPMVars
+    `($(mkIdent c).{$[$(ls.toArray.map (Level.quote · (prec := 0) (mvars := mvars)))],*})
 
   let stx ← maybeAddBlockImplicit stx
   if (← getPPOption getPPTagAppFns) then

src/Lean/PrettyPrinter/Delaborator/Options.lean

@@ -82,7 +82,8 @@ register_builtin_option pp.instantiateMVars : Bool := {
 register_builtin_option pp.mvars : Bool := {
   defValue := true
   group    := "pp"
-  descr    := "(pretty printer) display names of metavariables when true, and otherwise display them as '?_'"
+  descr    := "(pretty printer) display names of metavariables when true, \
+    and otherwise display them as '?_' (for expression metavariables) and as '_' (for universe level metavariables)"
 }
 register_builtin_option pp.mvars.withType : Bool := {
   defValue := false

src/Lean/Util/TestExtern.lean

@@ -8,8 +8,9 @@ import Lean.Elab.SyntheticMVars
 import Lean.Elab.Command
 import Lean.Meta.Tactic.Unfold
 import Lean.Meta.Eval
+import Lean.Compiler.ImplementedByAttr
 
-open Lean Elab Meta Command Term
+open Lean Elab Meta Command Term Compiler
 
 syntax (name := testExternCmd) "test_extern " term : command
 
@@ -18,14 +19,15 @@ syntax (name := testExternCmd) "test_extern " term : command
     let t ← elabTermAndSynthesize t none
     match t.getAppFn with
     | .const f _ =>
-      if isExtern (← getEnv) f then
+      let env ← getEnv
+      if isExtern env f || (getImplementedBy? env f).isSome then
         let t' := (← unfold t f).expr
-        let r := mkApp (.const ``reduceBool []) (← mkAppM ``BEq.beq #[t, t'])
+        let r := mkApp (.const ``reduceBool []) (← mkDecide (← mkEq t t'))
         if ! (← evalExpr Bool (.const ``Bool []) r) then
           throwError
             ("native implementation did not agree with reference implementation!\n" ++
             m!"Compare the outputs of:\n#eval {t}\n and\n#eval {t'}")
       else
-        throwError "test_extern: {f} does not have an @[extern] attribute"
+        throwError "test_extern: {f} does not have an @[extern] attribute or @[implemented_by] attribute"
     | _ => throwError "test_extern: expects a function application"
   | _ => throwUnsupportedSyntax

src/lake/Lake/Load/Main.lean

@@ -174,6 +174,8 @@ def Workspace.updateAndMaterialize
         liftM (m := IO) <| throw e -- only ignore manifest on a bare `lake update`
       logWarning s!"{rootName}: ignoring previous manifest because it failed to load: {e}"
     resolveDepsAcyclic ws.root fun pkg resolve => do
+      if let some pkg := (← getThe Workspace).findPackage? pkg.name then
+        return pkg
       let inherited := pkg.name != ws.root.name
       -- Materialize this package's dependencies first
       let deps ← pkg.depConfigs.mapM fun dep => fetchOrCreate dep.name do
@@ -243,6 +245,8 @@ def Workspace.materializeDeps
   let rootPkg := ws.root
   let (root, ws) ← StateT.run (s := ws) <| StateT.run' (s := mkNameMap Package) do
     resolveDepsAcyclic rootPkg fun pkg resolve => do
+      if let some pkg := (← getThe Workspace).findPackage? pkg.name then
+        return pkg
       let topLevel := pkg.name = rootPkg.name
       let deps := pkg.depConfigs
       if topLevel then

src/lake/examples/deps/bar/lake-manifest.expected.json

@@ -0,0 +1,29 @@
+{"version": 7,
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"type": "path",
+   "name": "root",
+   "manifestFile": "lake-manifest.json",
+   "inherited": true,
+   "dir": "./../foo/../a/../root",
+   "configFile": "lakefile.lean"},
+  {"type": "path",
+   "name": "a",
+   "manifestFile": "lake-manifest.json",
+   "inherited": true,
+   "dir": "./../foo/../a",
+   "configFile": "lakefile.lean"},
+  {"type": "path",
+   "name": "b",
+   "manifestFile": "lake-manifest.json",
+   "inherited": true,
+   "dir": "./../foo/../b",
+   "configFile": "lakefile.lean"},
+  {"type": "path",
+   "name": "foo",
+   "manifestFile": "lake-manifest.json",
+   "inherited": false,
+   "dir": "./../foo",
+   "configFile": "lakefile.lean"}],
+ "name": "bar",
+ "lakeDir": ".lake"}

src/lake/examples/deps/test.sh

@@ -6,6 +6,11 @@ LAKE=${LAKE:-../../.lake/build/bin/lake}
 ./clean.sh
 
 $LAKE -d bar build --update
+# Test that the update produces the expected manifest.
+# Serves as a regression test to ensure that multiples of a package in
+# the dependency tree do not produce duplicate entries in the manifest.
+# https://github.com/leanprover/lean4/pull/3957
+diff --strip-trailing-cr bar/lake-manifest.expected.json bar/lake-manifest.json
 $LAKE -d foo build --update
 
 ./foo/.lake/build/bin/foo
@@ -29,6 +34,7 @@ test ! -d foo/.lake/build
 ./clean.sh
 
 $LAKE -d bar -f lakefile.toml build --update
+diff --strip-trailing-cr bar/lake-manifest.expected.json bar/lake-manifest.json
 $LAKE -d foo -f lakefile.toml build --update
 
 ./foo/.lake/build/bin/foo

tests/lean/deprecated.lean

@@ -17,14 +17,14 @@ def f1 (x : Nat) := x + 1
 
 def Foo.g1 := 10
 
-@[deprecated Foo.g1]
+@[deprecated Foo.g1 (since := "2022-07-24")]
 def f2 (x : Nat) := x + 1
 
 @[deprecated g1]
 def f3 (x : Nat) := x + 1
 
 open Foo
-@[deprecated g1]
+@[deprecated g1 "use g1 instead, f4 is not a good name"]
 def f4 (x : Nat) := x + 1
 
 #eval f2 0 + 1

tests/lean/deprecated.lean.expected.out

@@ -7,5 +7,5 @@ deprecated.lean:23:13-23:15: error: unknown constant 'g1'
 deprecated.lean:30:6-30:8: warning: `f2` has been deprecated, use `Foo.g1` instead
 2
 2
-deprecated.lean:33:6-33:8: warning: `f4` has been deprecated, use `Foo.g1` instead
+deprecated.lean:33:6-33:8: warning: use g1 instead, f4 is not a good name
 2

tests/lean/run/3965.lean

@@ -0,0 +1,206 @@
+section Mathlib.Logic.Function.Iterate
+
+universe u v
+
+variable {α : Type u}
+
+/-- Iterate a function. -/
+def Nat.iterate {α : Sort u} (op : α → α) : Nat → α → α := sorry
+
+notation:max f "^["n"]" => Nat.iterate f n
+
+theorem Function.iterate_succ' (f : α → α) (n : Nat) : f^[n.succ] = f ∘ f^[n] := sorry
+
+end Mathlib.Logic.Function.Iterate
+
+section Mathlib.Data.Quot
+
+variable {α : Sort _}
+
+noncomputable def Quot.out {r : α → α → Prop} (q : Quot r) : α := sorry
+
+end Mathlib.Data.Quot
+
+section Mathlib.Init.Order.Defs
+
+universe u
+variable {α : Type u}
+
+section Preorder
+
+class Preorder (α : Type u) extends LE α, LT α where
+
+variable [Preorder α]
+
+theorem lt_of_lt_of_le : ∀ {a b c : α}, a < b → b ≤ c → a < c := sorry
+
+end Preorder
+
+variable [LE α]
+
+theorem le_total : ∀ a b : α, a ≤ b ∨ b ≤ a := sorry
+
+end Mathlib.Init.Order.Defs
+
+section Mathlib.Order.RelClasses
+
+universe u
+
+class IsWellOrder (α : Type u) (r : α → α → Prop) : Prop
+
+end Mathlib.Order.RelClasses
+
+section Mathlib.Order.SetNotation
+
+universe u v
+variable {α : Type u} {ι : Sort v}
+
+class SupSet (α : Type _) where
+
+def iSup [SupSet α] (s : ι → α) : α := sorry
+
+end Mathlib.Order.SetNotation
+
+section Mathlib.SetTheory.Ordinal.Basic
+
+noncomputable section
+
+universe u v w
+
+variable {α : Type u}
+
+structure WellOrder : Type (u + 1) where
+  α : Type u
+
+instance Ordinal.isEquivalent : Setoid WellOrder := sorry
+
+def Ordinal : Type (u + 1) := Quotient Ordinal.isEquivalent
+
+instance (o : Ordinal) : LT o.out.α := sorry
+
+namespace Ordinal
+
+def typein (r : α → α → Prop) [IsWellOrder α r] (a : α) : Ordinal := sorry
+
+instance partialOrder : Preorder Ordinal := sorry
+
+theorem typein_lt_self {o : Ordinal} (i : o.out.α) :
+    @typein _ (· < ·) sorry i < o := sorry
+
+instance : SupSet Ordinal := sorry
+
+end Ordinal
+
+end
+
+end Mathlib.SetTheory.Ordinal.Basic
+
+section Mathlib.SetTheory.Ordinal.Arithmetic
+
+noncomputable section
+
+universe u v w
+
+namespace Ordinal
+
+def sup {ι : Type u} (f : ι → Ordinal.{max u v}) : Ordinal.{max u v} :=
+  iSup f
+
+def lsub {ι} (f : ι → Ordinal) : Ordinal :=
+  sup f
+
+def blsub₂ (o₁ o₂ : Ordinal) (op : {a : Ordinal} → (a < o₁) → {b : Ordinal} → (b < o₂) → Ordinal) :
+    Ordinal :=
+  lsub (fun x : o₁.out.α × o₂.out.α => op (typein_lt_self x.1) (typein_lt_self x.2))
+
+theorem lt_blsub₂ {o₁ o₂ : Ordinal}
+    (op : {a : Ordinal} → (a < o₁) → {b : Ordinal} → (b < o₂) → Ordinal) {a b : Ordinal}
+    (ha : a < o₁) (hb : b < o₂) : op ha hb < blsub₂ o₁ o₂ op := sorry
+
+
+end Ordinal
+
+end
+
+end Mathlib.SetTheory.Ordinal.Arithmetic
+
+section Mathlib.SetTheory.Ordinal.FixedPoint
+
+noncomputable section
+
+universe u v
+
+namespace Ordinal
+
+section
+
+variable {ι : Type u} {f : ι → Ordinal.{max u v} → Ordinal.{max u v}}
+
+def nfpFamily (f : ι → Ordinal → Ordinal) (a : Ordinal) : Ordinal :=
+  sup (List.foldr f a)
+
+end
+
+section
+
+variable {f : Ordinal.{u} → Ordinal.{u}}
+
+def nfp (f : Ordinal → Ordinal) : Ordinal → Ordinal :=
+  nfpFamily fun _ : Unit => f
+
+theorem lt_nfp {a b} : a < nfp f b ↔ ∃ n, a < f^[n] b := sorry
+
+end
+
+end Ordinal
+
+end
+
+end Mathlib.SetTheory.Ordinal.FixedPoint
+
+section Mathlib.SetTheory.Ordinal.Principal
+
+universe u v w
+
+namespace Ordinal
+
+def Principal (op : Ordinal → Ordinal → Ordinal) (o : Ordinal) : Prop :=
+  ∀ ⦃a b⦄, a < o → b < o → op a b < o
+
+theorem principal_nfp_blsub₂ (op : Ordinal → Ordinal → Ordinal) (o : Ordinal) :
+    Principal op (nfp (fun o' => blsub₂.{u, u, u} o' o' (@fun a _ b _ => op a b)) o) :=
+  fun a b ha hb => by
+  rw [lt_nfp] at *
+  rcases ha with ⟨m, hm⟩
+  rcases hb with ⟨n, hn⟩
+  rcases le_total
+    ((fun o' => blsub₂.{u, u, u} o' o' (@fun a _ b _ => op a b))^[m] o)
+    ((fun o' => blsub₂.{u, u, u} o' o' (@fun a _ b _ => op a b))^[n] o) with h | h
+  · refine ⟨n+1, ?_⟩
+    rw [Function.iterate_succ']
+    -- after https://github.com/leanprover/lean4/pull/3965 this requires `lt_blsub₂.{u}` or we get
+    -- `stuck at solving universe constraint max u ?u =?= u`
+    -- Note that there are two solutions: 0 and u. Both of them work.
+    exact lt_blsub₂.{u} (@fun a _ b _ => op a b) (lt_of_lt_of_le hm h) hn
+  · sorry
+
+-- Trying again with 0
+theorem principal_nfp_blsub₂' (op : Ordinal → Ordinal → Ordinal) (o : Ordinal) :
+    Principal op (nfp (fun o' => blsub₂.{u, u, u} o' o' (@fun a _ b _ => op a b)) o) :=
+  fun a b ha hb => by
+  rw [lt_nfp] at *
+  rcases ha with ⟨m, hm⟩
+  rcases hb with ⟨n, hn⟩
+  rcases le_total
+    ((fun o' => blsub₂.{u, u, u} o' o' (@fun a _ b _ => op a b))^[m] o)
+    ((fun o' => blsub₂.{u, u, u} o' o' (@fun a _ b _ => op a b))^[n] o) with h | h
+  · refine ⟨n+1, ?_⟩
+    rw [Function.iterate_succ']
+    -- universe 0 also works here
+    exact lt_blsub₂.{0} (@fun a _ b _ => op a b) (lt_of_lt_of_le hm h) hn
+  · sorry
+
+
+end Ordinal
+
+end Mathlib.SetTheory.Ordinal.Principal

tests/lean/run/3965_2.lean

@@ -0,0 +1,98 @@
+section Mathlib.Init.Order.Defs
+
+universe u
+
+variable {α : Type u}
+
+class PartialOrder (α : Type u) extends LE α, LT α where
+
+theorem le_antisymm [PartialOrder α] : ∀ {a b : α}, a ≤ b → b ≤ a → a = b := sorry
+
+end Mathlib.Init.Order.Defs
+
+section Mathlib.Init.Data.Nat.Lemmas
+
+namespace Nat
+
+instance : PartialOrder Nat where
+  le := Nat.le
+  lt := Nat.lt
+
+section Find
+
+variable {p : Nat → Prop}
+
+private def lbp (m n : Nat) : Prop :=
+  m = n + 1 ∧ ∀ k ≤ n, ¬p k
+
+variable [DecidablePred p] (H : ∃ n, p n)
+
+private def wf_lbp {p : Nat → Prop} (H : ∃ n, p n) : WellFounded (@lbp p) := sorry
+
+protected noncomputable def findX : { n // p n ∧ ∀ m < n, ¬p m } :=
+  @WellFounded.fix _ (fun k => (∀ n < k, ¬p n) → { n // p n ∧ ∀ m < n, ¬p m }) lbp (wf_lbp H)
+    sorry 0 sorry
+
+protected noncomputable def find {p : Nat → Prop} [DecidablePred p] (H : ∃ n, p n) : Nat :=
+  (Nat.findX H).1
+
+protected theorem find_spec : p (Nat.find H) := sorry
+
+protected theorem find_min' {m : Nat} (h : p m) : Nat.find H ≤ m := sorry
+
+end Find
+
+end Nat
+
+end Mathlib.Init.Data.Nat.Lemmas
+
+section Mathlib.Logic.Basic
+
+theorem Exists.fst {b : Prop} {p : b → Prop} : Exists p → b
+  | ⟨h, _⟩ => h
+
+end Mathlib.Logic.Basic
+
+section Mathlib.Order.Basic
+
+open Function
+
+def PartialOrder.lift {α β} [PartialOrder β] (f : α → β) : PartialOrder α where
+  le x y := f x ≤ f y
+  lt x y := f x < f y
+
+end Mathlib.Order.Basic
+
+section Mathlib.Data.Fin.Basic
+
+instance {n : Nat} : PartialOrder (Fin n) :=
+  PartialOrder.lift Fin.val
+
+end Mathlib.Data.Fin.Basic
+
+section Mathlib.Data.Fin.Tuple.Basic
+
+universe u v
+
+namespace Fin
+
+variable {n : Nat}
+
+def find : ∀ {n : Nat} (p : Fin n → Prop) [DecidablePred p], Option (Fin n)
+  | 0, _p, _ => none
+  | n + 1, p, _ => by
+    exact
+      Option.casesOn (@find n (fun i ↦ p (i.castLT sorry)) _)
+        (if _ : p (Fin.last n) then some (Fin.last n) else none) fun i ↦
+        some (i.castLT sorry)
+
+theorem nat_find_mem_find {p : Fin n → Prop} [DecidablePred p]
+    (h : ∃ i, ∃ hin : i < n, p ⟨i, hin⟩) :
+    (⟨Nat.find h, (Nat.find_spec h).fst⟩ : Fin n) ∈ find p := by
+  rcases hf : find p with f | f
+  · sorry
+  · exact Option.some_inj.2 (le_antisymm sorry (Nat.find_min' _ ⟨f.2, sorry⟩))
+
+end Fin
+
+end Mathlib.Data.Fin.Tuple.Basic

tests/lean/run/ppMVars.lean

@@ -1,3 +1,4 @@
+import Lean.Elab.BuiltinNotation
 /-!
 # Testing `pp.mvars`
 -/
@@ -9,6 +10,12 @@ Default values
 /-- info: ?a : Nat -/
 #guard_msgs in #check (?a : Nat)
 
+/-- info: ⊢ Sort ?u.1 -/
+#guard_msgs (info, drop all) in
+example : (by_elab do return .sort (.mvar (.mk (.num `_uniq 1)))) := by
+  trace_state
+  sorry
+
 /-!
 Turning off `pp.mvars`
 -/
@@ -21,6 +28,18 @@ set_option pp.mvars false
 /-- info: ?_ : Nat -/
 #guard_msgs in #check (_ : Nat)
 
+/-- info: ⊢ Sort _ -/
+#guard_msgs (info, drop all) in
+example : (by_elab do return .sort (.mvar (.mk (.num `_uniq 1)))) := by
+  trace_state
+  sorry
+
+/-- info: ⊢ Type _ -/
+#guard_msgs (info, drop all) in
+example : Type _ := by
+  trace_state
+  sorry
+
 end
 
 /-!

tests/lean/run/utf8英語.lean

@@ -1,7 +1,6 @@
 import Lean.Util.TestExtern
 
-instance : BEq ByteArray where
-  beq x y := x.data == y.data
+deriving instance DecidableEq for ByteArray
 
 test_extern String.toUTF8 ""
 test_extern String.toUTF8 "\x00"

tests/lean/test_extern.lean

@@ -1,9 +1,15 @@
 import Lean.Util.TestExtern
 
-instance : BEq ByteArray where
-  beq x y := x.data == y.data
+deriving instance DecidableEq for ByteArray
 
 test_extern Nat.add 12 37
 test_extern 4 + 5
 
 test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 1 ⟨#[4, 5, 6, 7, 8, 9, 10, 11, 12, 13]⟩ 0 6
+
+def f := 3
+
+@[implemented_by f]
+def g := 4
+
+test_extern g

tests/lean/test_extern.lean.expected.out

@@ -1 +1,3 @@
-test_extern.lean:7:0-7:17: error: test_extern: HAdd.hAdd does not have an @[extern] attribute
+test_extern.lean:6:0-6:17: error: test_extern: HAdd.hAdd does not have an @[extern] attribute or @[implemented_by] attribute
+test_extern.lean:15:0-15:13: error: native implementation did not agree with reference implementation!
+Compare the outputs of: #eval g  and #eval 4