fix: remove inhabited

This PR corrects the `Inhabited` instance of `StdGen` to use a valid
initial state for the pseudorandom number generator. Previously, the
`default` generator had the property that `Prod.snd (stdNext default) =
default`, so it would produce only constant sequences.

[Zulip
discussion](https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/inhabited.20instance.20for.20StdGen.20isn't.20very.20random/with/533247146)

.github/workflows/build-template.yml

@@ -205,7 +205,7 @@ jobs:
         id: test
         run: |
           ulimit -c unlimited  # coredumps
-          time ctest --preset ${{ matrix.CMAKE_PRESET || 'release' }} --test-dir build/$TARGET_STAGE -j$NPROC --output-junit test-results.xml ${{ matrix.CTARGET_OPTIONS }}
+          time ctest --preset ${{ matrix.CMAKE_PRESET || 'release' }} --test-dir build/$TARGET_STAGE -j$NPROC --output-junit test-results.xml
         if: (matrix.wasm || !matrix.cross) && (inputs.check-level >= 1 || matrix.test)
       - name: Test Summary
         uses: test-summary/action@v2
@@ -235,9 +235,13 @@ jobs:
         if: matrix.test-speedcenter
       - name: Check rebootstrap
         run: |
+          set -e
           # clean rebuild in case of Makefile changes/Lake does not detect uncommited stage 0
           # changes yet
-          make -C build update-stage0 && make -C build/stage1 clean-stdlib && make -C build -j$NPROC
+          make -C build update-stage0
+          make -C build/stage1 clean-stdlib
+          time make -C build -j$NPROC
+          time ctest --preset ${{ matrix.CMAKE_PRESET || 'release' }} --test-dir build/stage1 -j$NPROC
         if: matrix.check-rebootstrap
       - name: CCache stats
         if: always()

src/Init/Data/List/MapIdx.lean

@@ -61,7 +61,7 @@ proof that the index is valid.
 `List.mapIdxM` is a variant that does not provide the function with evidence that the index is
 valid.
 -/
-@[inline] def mapFinIdxM [Monad m] (as : List α) (f : (i : Nat) → α → (h : i < as.length) → m β) : m (List β) :=
+@[inline, expose] def mapFinIdxM [Monad m] (as : List α) (f : (i : Nat) → α → (h : i < as.length) → m β) : m (List β) :=
   go as #[] (by simp)
 where
   /-- Auxiliary for `mapFinIdxM`:
@@ -78,7 +78,7 @@ found, returning the list of results.
 `List.mapFinIdxM` is a variant that additionally provides the function with a proof that the index
 is valid.
 -/
-@[inline] def mapIdxM [Monad m] (f : Nat → α → m β) (as : List α) : m (List β) := go as #[] where
+@[inline, expose] def mapIdxM [Monad m] (f : Nat → α → m β) (as : List α) : m (List β) := go as #[] where
   /-- Auxiliary for `mapIdxM`:
   `mapIdxM.go [a₀, a₁, ...] acc = acc.toList ++ [f acc.size a₀, f (acc.size + 1) a₁, ...]` -/
   @[specialize] go : List α → Array β → m (List β)

src/Init/Data/Random.lean

@@ -36,7 +36,14 @@ structure StdGen where
   s1 : Nat
   s2 : Nat
 
-instance : Inhabited StdGen := ⟨{ s1 := 0, s2 := 0 }⟩
+/-- Returns a standard number generator. -/
+def mkStdGen (s : Nat := 0) : StdGen :=
+  let q  := s / 2147483562
+  let s1 := s % 2147483562
+  let s2 := q % 2147483398
+  ⟨s1 + 1, s2 + 1⟩
+
+instance : Inhabited StdGen := ⟨mkStdGen⟩
 
 /-- The range of values returned by `StdGen` -/
 def stdRange := (1, 2147483562)
@@ -77,13 +84,6 @@ instance : RandomGen StdGen := {
   split  := stdSplit
 }
 
-/-- Returns a standard number generator. -/
-def mkStdGen (s : Nat := 0) : StdGen :=
-  let q  := s / 2147483562
-  let s1 := s % 2147483562
-  let s2 := q % 2147483398
-  ⟨s1 + 1, s2 + 1⟩
-
 /--
 Auxiliary function for randomNatVal.
 Generate random values until we exceed the target magnitude.

src/Init/Data/String/Basic.lean

@@ -485,6 +485,7 @@ Examples:
 * `"tea".firstDiffPos "teas" = ⟨3⟩`
 * `"teas".firstDiffPos "tea" = ⟨3⟩`
 -/
+@[expose]
 def firstDiffPos (a b : String) : Pos :=
   let stopPos := a.endPos.min b.endPos
   let rec loop (i : Pos) : Pos :=
@@ -511,7 +512,7 @@ Examples:
 * `"red green blue".extract ⟨4⟩ ⟨100⟩ = "green blue"`
 * `"L∃∀N".extract ⟨2⟩ ⟨100⟩ = "green blue"`
 -/
-@[extern "lean_string_utf8_extract"]
+@[extern "lean_string_utf8_extract", expose]
 def extract : (@& String) → (@& Pos) → (@& Pos) → String
   | ⟨s⟩, b, e => if b.byteIdx ≥ e.byteIdx then "" else ⟨go₁ s 0 b e⟩
 where

src/Lean/Compiler/IR/RC.lean

@@ -20,7 +20,8 @@ that introduce the instructions `release` and `set`
 -/
 
 structure VarInfo where
-  type : IRType
+  isPossibleRef : Bool
+  isDefiniteRef: Bool
   persistent : Bool
   inheritsBorrowFromParam : Bool
   deriving Inhabited
@@ -44,26 +45,30 @@ def getJPParams (ctx : Context) (j : JoinPointId) : Array Param :=
   ctx.localCtx.getJPParams j |>.get!
 
 def getJPLiveVars (ctx : Context) (j : JoinPointId) : LiveVarSet :=
-  ctx.jpLiveVarMap.get? j |>.getD {}
+  ctx.jpLiveVarMap.get! j
 
 def mustConsume (ctx : Context) (x : VarId) : Bool :=
   let info := getVarInfo ctx x
-  info.type.isPossibleRef && !info.inheritsBorrowFromParam
+  info.isPossibleRef && !info.inheritsBorrowFromParam
 
 @[inline] def addInc (ctx : Context) (x : VarId) (b : FnBody) (n := 1) : FnBody :=
   let info := getVarInfo ctx x
-  if n == 0 then b else .inc x n (!info.type.isDefiniteRef) info.persistent b
+  if n == 0 then b else .inc x n (!info.isDefiniteRef) info.persistent b
 
 @[inline] def addDec (ctx : Context) (x : VarId) (b : FnBody) : FnBody :=
   let info := getVarInfo ctx x
-  .dec x 1 (!info.type.isDefiniteRef) info.persistent b
+  .dec x 1 (!info.isDefiniteRef) info.persistent b
 
 private def updateRefUsingCtorInfo (ctx : Context) (x : VarId) (c : CtorInfo) : Context :=
   let m := ctx.varMap
   { ctx with
     varMap := match m.get? x with
-    | some info => m.insert x { info with type := c.type }
-    | none      => m }
+    | some info =>
+      let isPossibleRef := c.type.isPossibleRef
+      let isDefiniteRef := c.type.isDefiniteRef
+      m.insert x { info with isPossibleRef, isDefiniteRef }
+    | none => m
+  }
 
 private def addDecForAlt (ctx : Context) (caseLiveVars altLiveVars : LiveVarSet) (b : FnBody) : FnBody :=
   caseLiveVars.foldl (init := b) fun b x =>
@@ -105,7 +110,7 @@ private def addIncBeforeAux (ctx : Context) (xs : Array Arg) (consumeParamPred :
     | .erased => b
     | .var x =>
       let info := getVarInfo ctx x
-      if !info.type.isPossibleRef || !isFirstOcc xs i then b
+      if !info.isPossibleRef || !isFirstOcc xs i then b
       else
         let numConsumptions := getNumConsumptions x xs consumeParamPred
         let numIncs :=
@@ -171,9 +176,13 @@ private def updateVarInfo (ctx : Context) (x : VarId) (t : IRType) (v : Expr) :
       | some info => info.inheritsBorrowFromParam
       | none => false
     | _ => false
+  let type := typeForScalarBoxedInTaggedPtr? v |>.getD t
+  let isPossibleRef := type.isPossibleRef
+  let isDefiniteRef := type.isDefiniteRef
   { ctx with
     varMap := ctx.varMap.insert x {
-        type := typeForScalarBoxedInTaggedPtr? v |>.getD t
+        isPossibleRef
+        isDefiniteRef
         persistent := isPersistent v,
         inheritsBorrowFromParam
     }
@@ -208,7 +217,11 @@ private def processVDecl (ctx : Context) (z : VarId) (t : IRType) (v : Expr) (b
 
 def updateVarInfoWithParams (ctx : Context) (ps : Array Param) : Context :=
   let m := ps.foldl (init := ctx.varMap) fun m p =>
-    m.insert p.x { type := p.ty, persistent := false, inheritsBorrowFromParam := p.borrow }
+    m.insert p.x {
+      isPossibleRef := p.ty.isPossibleRef
+      isDefiniteRef := p.ty.isDefiniteRef
+      persistent := false
+      inheritsBorrowFromParam := p.borrow }
   { ctx with varMap := m }
 
 partial def visitFnBody (b : FnBody) (ctx : Context) : FnBody × LiveVarSet :=
@@ -263,7 +276,7 @@ partial def visitFnBody (b : FnBody) (ctx : Context) : FnBody × LiveVarSet :=
     | .var x =>
       let info := getVarInfo ctx x
       let b :=
-        if info.type.isPossibleRef && info.inheritsBorrowFromParam then
+        if info.isPossibleRef && info.inheritsBorrowFromParam then
           addInc ctx x b
         else b
       ⟨b, mkLiveVarSet x⟩
@@ -275,7 +288,7 @@ partial def visitFnBody (b : FnBody) (ctx : Context) : FnBody × LiveVarSet :=
     let bLiveVars := collectLiveVars b ctx.jpLiveVarMap
     ⟨b, bLiveVars⟩
   | .unreachable => ⟨.unreachable, {}⟩
-  | _ => ⟨b, {}⟩ -- unreachable if well-formed
+  | .set .. | .setTag .. | .inc .. | .dec .. | .del .. => unreachable!
 
 partial def visitDecl (env : Environment) (decls : Array Decl) (d : Decl) : Decl :=
   match d with

src/Lean/Elab/Tactic/Do/VCGen/Basic.lean

@@ -62,6 +62,7 @@ structure Context where
   simpCtx : Simp.Context
   simprocs : Simp.SimprocsArray
   jps : FVarIdMap JumpSiteInfo := {}
+  initialCtxSize : Nat
 
 structure State where
   fuel : Fuel := .unlimited
@@ -88,9 +89,10 @@ def ifOutOfFuel (x : VCGenM α) (k : VCGenM α) : VCGenM α := do
   | _ => k
 
 def emitVC (subGoal : Expr) (name : Name) : VCGenM Expr := do
-  let m ← liftM <| mkFreshExprSyntheticOpaqueMVar subGoal (tag := name)
-  modify fun s => { s with vcs := s.vcs.push m.mvarId! }
-  return m
+  withFreshUserNamesSinceIdx (← read).initialCtxSize do
+    let m ← liftM <| mkFreshExprSyntheticOpaqueMVar subGoal (tag := name)
+    modify fun s => { s with vcs := s.vcs.push m.mvarId! }
+    return m
 
 def addSubGoalAsVC (goal : MVarId) : VCGenM PUnit := do
   modify fun s => { s with vcs := s.vcs.push goal }
@@ -239,4 +241,10 @@ def mkSpecContext (optConfig : Syntax) (lemmas : Syntax) (ignoreStarArg := false
           let thm ← mkSpecTheoremFromLocal fvar
           specThms := addSpecTheoremEntry specThms thm
         catch _ => continue
-  return { config, specThms, simpCtx := res.ctx, simprocs := res.simprocs }
+  return {
+    config,
+    specThms,
+    simpCtx := res.ctx,
+    simprocs := res.simprocs
+    initialCtxSize := (← getLCtx).numIndices
+  }

src/Lean/Meta/Basic.lean

@@ -1951,6 +1951,18 @@ def withErasedFVars [MonadLCtx n] [MonadLiftT MetaM n] (fvarIds : Array FVarId)
   let localInsts' := localInsts.filter (!fvarIds.contains ·.fvar.fvarId!)
   withLCtx lctx' localInsts' k
 
+/--
+Ensures that the user names of all local declarations after index `idx` have a macro scope.
+-/
+def withFreshUserNamesSinceIdx [MonadLCtx n] [MonadLiftT MetaM n] (idx : Nat) (k : n α) : n α := do
+  let mut lctx ← getLCtx
+  for i in [idx:lctx.numIndices] do
+    let some decl := lctx.decls[i]! | continue
+    let n := decl.userName
+    if !n.hasMacroScopes then
+      lctx := lctx.setUserName decl.fvarId (← liftMetaM <| mkFreshUserName n)
+  withLCtx' lctx k
+
 private def withMVarContextImp (mvarId : MVarId) (x : MetaM α) : MetaM α := do
   let mvarDecl ← mvarId.getDecl
   withLocalContextImp mvarDecl.lctx mvarDecl.localInstances x

src/Lean/Meta/CollectMVars.lean

@@ -50,39 +50,50 @@ def getMVarsAtDecl (d : Declaration) : MetaM (Array MVarId) := do
   let (_, s) ← (collectMVarsAtDecl d).run {}
   pure s.result
 
+end Lean.Meta
+
+open Lean Meta
+
+mutual
+
+/-- Auxiliary definition for `getMVarDependencies`. -/
+private partial def addMVars (e : Expr) (includeDelayed := false) : StateRefT (Std.HashSet MVarId) MetaM Unit := do
+  let mvars ← getMVars e
+  let mut s ← get
+  set ({} : Std.HashSet MVarId) -- Ensure that `s` is not shared.
+  for mvarId in mvars do
+    if ← pure includeDelayed <||> notM (mvarId.isDelayedAssigned) then
+      s := s.insert mvarId
+  set s
+  mvars.forM go
+
+/-- Auxiliary definition for `getMVarDependencies`. -/
+private partial def go (mvarId : MVarId) (includeDelayed := false) : StateRefT (Std.HashSet MVarId) MetaM Unit :=
+  withIncRecDepth do
+    let mdecl ← mvarId.getDecl
+    addMVars mdecl.type includeDelayed
+    for ldecl in mdecl.lctx do
+      addMVars ldecl.type includeDelayed
+      if let (some val) := ldecl.value? then
+        addMVars val includeDelayed
+    if let (some ass) ← getDelayedMVarAssignment? mvarId then
+      let pendingMVarId := ass.mvarIdPending
+      if ← notM pendingMVarId.isAssignedOrDelayedAssigned then
+        modify (·.insert pendingMVarId)
+      go pendingMVarId includeDelayed
+
+end
+
 /--
 Collect the metavariables which `mvarId` depends on. These are the metavariables
 which appear in the type and local context of `mvarId`, as well as the
 metavariables which *those* metavariables depend on, etc.
 -/
-partial def _root_.Lean.MVarId.getMVarDependencies (mvarId : MVarId) (includeDelayed := false) :
+def Lean.MVarId.getMVarDependencies (mvarId : MVarId) (includeDelayed := false) :
     MetaM (Std.HashSet MVarId) :=
-  (·.snd) <$> (go mvarId).run {}
-where
-  /-- Auxiliary definition for `getMVarDependencies`. -/
-  addMVars (e : Expr) : StateRefT (Std.HashSet MVarId) MetaM Unit := do
-    let mvars ← getMVars e
-    let mut s ← get
-    set ({} : Std.HashSet MVarId) -- Ensure that `s` is not shared.
-    for mvarId in mvars do
-      if ← pure includeDelayed <||> notM (mvarId.isDelayedAssigned) then
-        s := s.insert mvarId
-    set s
-    mvars.forM go
+  (·.snd) <$> (go mvarId includeDelayed).run {}
 
-  /-- Auxiliary definition for `getMVarDependencies`. -/
-  go (mvarId : MVarId) : StateRefT (Std.HashSet MVarId) MetaM Unit :=
-    withIncRecDepth do
-      let mdecl ← mvarId.getDecl
-      addMVars mdecl.type
-      for ldecl in mdecl.lctx do
-        addMVars ldecl.type
-        if let (some val) := ldecl.value? then
-          addMVars val
-      if let (some ass) ← getDelayedMVarAssignment? mvarId then
-        let pendingMVarId := ass.mvarIdPending
-        if ← notM pendingMVarId.isAssignedOrDelayedAssigned then
-          modify (·.insert pendingMVarId)
-        go pendingMVarId
-
-end Lean.Meta
+/-- Collect the metavariables appearing in the expression `e`,
+including metavariables in the type or local context of any such metavariables, etc. -/
+def Lean.Expr.getMVarDependencies (e : Expr) (includeDelayed := false) : MetaM (Std.HashSet MVarId) := do
+  (·.snd) <$> (addMVars e includeDelayed).run {}

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -62,13 +62,17 @@ def delabMVarAux (m : MVarId) : DelabM Term := do
   let mkMVar (n : Name) : DelabM Term := `(?$(mkIdent n))
   withTypeAscription (cond := ← getPPOption getPPMVarsWithType) do
     if ← getPPOption getPPMVars then
-      match (← m.getDecl).userName with
-      | .anonymous =>
-        if ← getPPOption getPPMVarsAnonymous then
-          mkMVar <| m.name.replacePrefix `_uniq `m
-        else
-          mkMVarPlaceholder
-      | n => mkMVar n
+      if let some decl ← m.findDecl? then
+        match decl.userName with
+        | .anonymous =>
+          if ← getPPOption getPPMVarsAnonymous then
+            mkMVar <| Name.num `m (decl.index + 1)
+          else
+            mkMVarPlaceholder
+        | n => mkMVar n
+      else
+        -- Undefined mvar, use internal name
+        mkMVar <| m.name.replacePrefix `_uniq `_mvar
     else
       mkMVarPlaceholder
 

src/Std/Do/PredTrans.lean

@@ -116,6 +116,10 @@ theorem bind_apply (x : PredTrans ps α) (f : α → PredTrans ps β) (Q : PostC
 theorem seq_apply (f : PredTrans ps (α → β)) (x : PredTrans ps α) (Q : PostCond β ps) :
   (f <*> x).apply Q = f.apply (fun g => x.apply (fun a => Q.1 (g a), Q.2), Q.2) := by rfl
 
+@[simp]
+theorem const_apply (p : Assertion ps) (Q : PostCond α ps) :
+  (PredTrans.const p : PredTrans ps α).apply Q = p := by rfl
+
 theorem bind_mono {x y : PredTrans ps α} {f : α → PredTrans ps β}
   (h : x ≤ y) : x >>= f ≤ y >>= f := by intro Q; exact (h (_, Q.2))
 

src/Std/Internal/Async/Basic.lean

@@ -681,22 +681,30 @@ instance : MonadLift BaseAsync (EAsync ε) where
 
 @[inline]
 protected partial def forIn
-    {β : Type} [i : Inhabited ε] (init : β)
+    {β : Type} (init : β)
     (f : Unit → β → EAsync ε (ForInStep β))
     (prio := Task.Priority.default) :
     EAsync ε β := do
+
+  have : Nonempty β := ⟨init⟩
   let promise ← IO.Promise.new
 
-  let rec @[specialize] loop (b : β) : EAsync ε (ETask ε Unit) := async (prio := prio) do
+  let rec @[specialize] loop (b : β) : BaseIO Unit := do
     match ← f () b with
-      | ForInStep.done b => promise.resolve (.ok b)
-      | ForInStep.yield b => discard <| (loop b)
+    | MaybeTask.pure result =>
+      match result with
+      | .error e => promise.resolve (.error e)
+      | .ok (.done b) => promise.resolve (.ok b)
+      | .ok (.yield b) => loop b
+    | MaybeTask.ofTask task => BaseIO.chainTask (prio := prio) task fun
+      | .error e => promise.resolve (.error e)
+      | .ok (.done b) => promise.resolve (.ok b)
+      | .ok (.yield b) => loop b
 
-  discard <| loop init
+  loop init
+  .mk <| EAsync.ofETask promise.result!
 
-  .mk <| BaseAsync.ofTask promise.result!
-
-instance [Inhabited ε] : ForIn (EAsync ε) Lean.Loop Unit where
+instance : ForIn (EAsync ε) Lean.Loop Unit where
   forIn _ := EAsync.forIn
 
 end EAsync
@@ -734,8 +742,8 @@ export MonadAwait (await)
 This function transforms the operation inside the monad `m` into a task and let it run in the background.
 -/
 @[inline, specialize]
-def background [Monad m] [MonadAsync t m] (prio := Task.Priority.default) : m α → m Unit :=
-  discard ∘ async (t := t) (prio := prio)
+def background [Monad m] [MonadAsync t m] (action : m α) (prio := Task.Priority.default) : m Unit :=
+  discard (async (t := t) (prio := prio) action)
 
 /--
 Runs two computations concurrently and returns both results as a pair.

tests/lean/815b.lean.expected.out

@@ -77,8 +77,7 @@
         Transformer
           fun redf a a => redf
   [Meta.synthInstance] ❌️ apply @comp to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
-    [Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g =>
-          f (g a✝) a ≟ IsSmooth fun a_1 => ?m a✝ a (?m a✝ a a_1)
+    [Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a_1 => ?m a✝ a (?m a✝ a a_1)
   [Meta.synthInstance] ✅️ apply @parm to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
     [Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a_1 => f (a_1 a✝) a
     [Meta.synthInstance.unusedArgs] ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a)
@@ -108,8 +107,7 @@
   [Meta.synthInstance] ❌️ apply inst✝ to ∀ (a : α), IsSmooth fun g => g a
     [Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => g a ≟ IsSmooth f
   [Meta.synthInstance] ❌️ apply @diag to ∀ (a : α), IsSmooth fun g => g a
-    [Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g =>
-          g a ≟ IsSmooth fun a_1 => ?m a (?m a a_1) (?m a a_1)
+    [Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => g a ≟ IsSmooth fun a_1 => ?m a (?m a a_1) (?m a a_1)
   [Meta.synthInstance] ❌️ apply @comp to ∀ (a : α), IsSmooth fun g => g a
     [Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => g a ≟ IsSmooth fun a_1 => ?m a (?m a a_1)
   [Meta.synthInstance] ✅️ apply @parm to ∀ (a : α), IsSmooth fun g => g a

tests/lean/interactive/autoBoundIssue.lean.expected.out

@@ -2,26 +2,22 @@
  "position": {"line": 13, "character": 21}}
 {"range":
  {"start": {"line": 13, "character": 21}, "end": {"line": 13, "character": 24}},
- "goal":
- "k : Fin ?m\nctx : Vector' Ty ?m\nty u : Ty\n⊢ Vector' Ty ?m"}
+ "goal": "k : Fin ?m\nctx : Vector' Ty ?m\nty u : Ty\n⊢ Vector' Ty ?m"}
 {"textDocument": {"uri": "file:///autoBoundIssue.lean"},
  "position": {"line": 16, "character": 26}}
 {"range":
  {"start": {"line": 16, "character": 26}, "end": {"line": 16, "character": 29}},
- "goal":
- "k : Fin ?m\nctx : Vector' Ty ?m\nty : Ty\n⊢ Vector' Ty ?m"}
+ "goal": "k : Fin ?m\nctx : Vector' Ty ?m\nty : Ty\n⊢ Vector' Ty ?m"}
 {"textDocument": {"uri": "file:///autoBoundIssue.lean"},
  "position": {"line": 19, "character": 20}}
 {"range":
  {"start": {"line": 19, "character": 20}, "end": {"line": 19, "character": 23}},
- "goal":
- "k : Fin ?m\nctx : Vector' Ty ?m\nty : Ty\n⊢ Vector' Ty ?m"}
+ "goal": "k : Fin ?m\nctx : Vector' Ty ?m\nty : Ty\n⊢ Vector' Ty ?m"}
 {"textDocument": {"uri": "file:///autoBoundIssue.lean"},
  "position": {"line": 24, "character": 18}}
 {"range":
  {"start": {"line": 24, "character": 18}, "end": {"line": 24, "character": 21}},
- "goal":
- "k : Fin ?m\nctx : Vector' Ty ?m\nty : Ty\n⊢ Vector' Ty ?m"}
+ "goal": "k : Fin ?m\nctx : Vector' Ty ?m\nty : Ty\n⊢ Vector' Ty ?m"}
 {"textDocument": {"uri": "file:///autoBoundIssue.lean"},
  "position": {"line": 26, "character": 18}}
 {"range":
@@ -32,5 +28,4 @@
  "position": {"line": 29, "character": 24}}
 {"range":
  {"start": {"line": 29, "character": 24}, "end": {"line": 29, "character": 27}},
- "goal":
- "k : Fin ?m\nctx : Vector' Ty ?m\nty : Ty\n⊢ Vector' Ty ?m"}
+ "goal": "k : Fin ?m\nctx : Vector' Ty ?m\nty : Ty\n⊢ Vector' Ty ?m"}

tests/lean/run/4144.lean

@@ -17,7 +17,7 @@ case refine'_4
 ⊢ ?refine'_1
 
 case refine'_5
-⊢ ¬(fun x => ?m.16) ?refine'_3 = (fun x => ?m.16) ?refine'_4
+⊢ ¬(fun x => ?m.9) ?refine'_3 = (fun x => ?m.9) ?refine'_4
 -/
 #guard_msgs in
 example : False := by

tests/lean/run/async.lean

@@ -20,7 +20,7 @@ def loop : Async Nat := do
   while res < 10 do
     res := res + 1
 
-  discard <| t
+  discard t
 
   pure res
 
@@ -29,3 +29,19 @@ info: 10
 -/
 #guard_msgs in
 #eval IO.println =<< ETask.block =<< loop.asTask
+
+def loopExcept : Async Nat := do
+  let mut res := 0
+
+  while res < 10 do
+    throw (.userError "some error")
+
+  discard t
+
+  pure res
+
+/--
+error: some error
+-/
+#guard_msgs in
+#eval IO.println =<< ETask.block =<< loopExcept.asTask

tests/lean/run/doLogicTests.lean

@@ -238,27 +238,6 @@ def fib_impl (n : Nat) : Id Nat := do
     b := a' + b
   return b
 
-abbrev fib_spec : Nat → Nat
-| 0 => 0
-| 1 => 1
-| n+2 => fib_spec n + fib_spec (n+1)
-
--- Finally investigate why we do not see the error here.
--- Seems to be related to not being able to display metavariables.
---theorem fib_triple : ⦃⌜True⌝⦄ fib_impl n ⦃⇓ r => r = fib_spec n⦄ := by
---  unfold fib_impl
---  dsimp
---  mintro _
---  if h : n = 0 then simp [h] else
---  simp only [h, reduceIte]
---  mspec
---  mspec_no_bind Spec.bind
---  set_option trace.Elab.Tactic.Do.spec true in
---  mspec_no_bind Spec.forIn_list ?inv ?step
---
---  case step => dsimp; intros; mintro _; simp_all
---  simp_all [Nat.sub_one_add_one]
-
 theorem fib_triple : ⦃⌜True⌝⦄ fib_impl n ⦃⇓ r => ⌜r = fib_spec n⌝⦄ := by
   unfold fib_impl
   dsimp
@@ -688,6 +667,12 @@ instance Result.instWPMonad : WPMonad Result (.except Error .pure) where
     ext Q
     cases x <;> simp [PredTrans.bind, PredTrans.const]
 
+theorem Result.by_wp {α} {x : Result α} (P : Result α → Prop) :
+  (⊢ₛ wp⟦x⟧ post⟨fun a => ⌜P (.ok a)⌝, fun e => ⌜P (.fail e)⌝⟩) → P x := by
+    intro hspec
+    simp only [instWP] at hspec
+    split at hspec <;> simp_all
+
 /-- Kinds of unsigned integers -/
 inductive UScalarTy where
 | Usize
@@ -940,14 +925,14 @@ theorem fast_expo_correct (x n : Nat) : fast_expo x n = x^n := by
   mvcgen
   case inv => exact ⇓⟨⟨e, x', y⟩, xs⟩ => ⌜x' ^ e * y = x ^ n ∧ e ≤ n - xs.pref.length⌝
   all_goals simp_all
-  case isFalse.isFalse b _ _ _ _ _ _ _ ih _ =>
+  case isFalse.isFalse b _ _ _ _ _ _ _ _ _ _ ih _ =>
     obtain ⟨e, y, x'⟩ := b
     simp at *
     constructor
     · rw [← Nat.pow_two, ← Nat.pow_mul]
       grind
     · grind
-  case isFalse.isTrue b _ _ _ _ _ _ _ ih _ =>
+  case isFalse.isTrue b _ _ _ _ _ _ _ _ _ _ ih _ =>
     obtain ⟨e, y, x'⟩ := b
     simp at *
     constructor
@@ -955,7 +940,7 @@ theorem fast_expo_correct (x n : Nat) : fast_expo x n = x^n := by
       have : e - 1 + 1 = e := by grind
       rw [this]
     · grind
-  case isTrue b _ _ _ _ _ _ _ ih =>
+  case isTrue b _ _ _ _ _ _ _ _ _ _ ih =>
     obtain ⟨e, y, x'⟩ := b
     subst_vars
     grind

tests/lean/run/haveTactic.lean

@@ -9,7 +9,7 @@ If the body of a `have` fails to elaborate, the tactic completes with a `sorry`
 error: Type mismatch
   False.elim
 has type
-  False → ?m.6
+  False → ?m.2
 but is expected to have type
   True
 ---

tests/lean/run/inferTypeFailure.lean

@@ -24,7 +24,7 @@ error: Failed to infer type of theorem `t`
 Note: All parameter types and holes (e.g., `_`) in the header of a theorem are resolved before the proof is processed; information from the proof cannot be used to infer what these values should be
 ---
 error: type of theorem 't' is not a proposition
-  ?m.65
+  ?m.1
 -/
 #guard_msgs in
 theorem t : _ := _

tests/lean/run/ppMVars.lean

@@ -19,6 +19,14 @@ example : (by_elab do return .sort (.mvar (.mk (.num `_uniq 1)))) := by
   trace_state
   sorry
 
+/-!
+No such mvar, pretty print using the mvarid rather than the index.
+-/
+/-- info: ?_mvar.222222 -/
+#guard_msgs in #eval do
+  let e := Expr.mvar (.mk (.num `_uniq 222222))
+  logInfo m!"{e}"
+
 /-!
 Turning off `pp.mvars`
 -/
@@ -54,14 +62,8 @@ set_option pp.mvars.levels false
 /-- info: ?a : Nat -/
 #guard_msgs in #check (?a : Nat)
 
-/-- info: ?m.222222222 : Nat -/
-#guard_msgs in #check by_elab do
-  -- Control the mvarId with something that's too big to happen naturally:
-  let mvarId : MVarId := .mk (.num `_uniq 222222222)
-  let lctx ← getLCtx
-  let type := mkConst ``Nat
-  Lean.MonadMCtx.modifyMCtx fun mctx => mctx.addExprMVarDecl mvarId .anonymous lctx {} type .natural 0
-  return .mvar mvarId
+/-- info: ?m.1 : Nat -/
+#guard_msgs in #check (_ : Nat)
 
 /-- trace: ⊢ Sort _ -/
 #guard_msgs (trace, drop all) in