feat: simprocs for String and Char <, <=, >, >=

Fixes two output bugs with cloud releases: (1) the fetch as part of an
`extraDep` was not properly isolated in a job, and (2) the release job
would be shown even if the release had already been successfully
fetched.

Also includes some related touchups, including the addition of show all
jobs on `-v` which helps with debugging job counts.

RELEASES.md

@@ -22,6 +22,18 @@ v4.9.0 (development in progress)
   definition itself can be marked as `@[semireducible]` to get the previous
   behavor.
 
+* The `MessageData.ofPPFormat` constructor has been removed.
+  Its functionality has been split into two:
+
+  - for lazy structured messages, please use `MessageData.lazy`;
+  - for embedding `Format` or `FormatWithInfos`, use `MessageData.ofFormatWithInfos`.
+
+  An example migration can be found in [#3929](https://github.com/leanprover/lean4/pull/3929/files#diff-5910592ab7452a0e1b2616c62d22202d2291a9ebb463145f198685aed6299867L109).
+
+* The `MessageData.ofFormat` constructor has been turned into a function.
+  If you need to inspect `MessageData`,
+  you can pattern-match on `MessageData.ofFormatWithInfos`.
+
 v4.8.0
 ---------
 

src/Init/Data/String/Basic.lean

@@ -24,6 +24,14 @@ instance : LT String :=
 instance decLt (s₁ s₂ : @& String) : Decidable (s₁ < s₂) :=
   List.hasDecidableLt s₁.data s₂.data
 
+@[reducible] protected def le (a b : String) : Prop := ¬ b < a
+
+instance : LE String :=
+  ⟨String.le⟩
+
+instance decLE (s₁ s₂ : String) : Decidable (s₁ ≤ s₂) :=
+  inferInstanceAs (Decidable (Not _))
+
 /--
 Returns the length of a string in Unicode code points.
 

src/Init/Grind.lean

@@ -6,3 +6,4 @@ Authors: Leonardo de Moura
 prelude
 import Init.Grind.Norm
 import Init.Grind.Tactics
+import Init.Grind.Lemmas

src/Init/Grind/Lemmas.lean

@@ -0,0 +1,14 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Core
+
+namespace Lean.Grind
+
+theorem intro_with_eq (p p' q : Prop) (he : p = p') (h : p' → q) : p → q :=
+  fun hp => h (he.mp hp)
+
+end Lean.Grind

src/Init/NotationExtra.lean

@@ -87,6 +87,7 @@ macro:35 xs:bracketedExplicitBinders " × " b:term:35  : term => expandBrackedBi
 macro:35 xs:bracketedExplicitBinders " ×' " b:term:35 : term => expandBrackedBinders ``PSigma xs b
 end
 
+namespace Lean
 -- first step of a `calc` block
 syntax calcFirstStep := ppIndent(colGe term (" := " term)?)
 -- enforce indentation of calc steps so we know when to stop parsing them
@@ -136,6 +137,7 @@ syntax (name := calcTactic) "calc" calcSteps : tactic
 @[inherit_doc «calc»]
 macro tk:"calc" steps:calcSteps : conv =>
   `(conv| tactic => calc%$tk $steps)
+end Lean
 
 @[app_unexpander Unit.unit] def unexpandUnit : Lean.PrettyPrinter.Unexpander
   | `($(_)) => `(())
@@ -361,6 +363,7 @@ macro_rules
   | `(letI $_:ident $_* : $_ := $_; $_) => Lean.Macro.throwUnsupported -- handled by elab
 
 
+namespace Lean
 syntax cdotTk := patternIgnore("· " <|> ". ")
 /-- `· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. -/
 syntax (name := cdot) cdotTk tacticSeqIndentGt : tactic
@@ -368,12 +371,11 @@ syntax (name := cdot) cdotTk tacticSeqIndentGt : tactic
 /--
   Similar to `first`, but succeeds only if one the given tactics solves the current goal.
 -/
-syntax (name := solve) "solve" withPosition((ppDedent(ppLine) colGe "| " tacticSeq)+) : tactic
+syntax (name := solveTactic) "solve" withPosition((ppDedent(ppLine) colGe "| " tacticSeq)+) : tactic
 
 macro_rules
   | `(tactic| solve $[| $ts]* ) => `(tactic| focus first $[| ($ts); done]*)
 
-namespace Lean
 /-! # `repeat` and `while` notation -/
 
 inductive Loop where

src/Lean/CoreM.lean

@@ -332,7 +332,8 @@ export Core (CoreM mkFreshUserName checkSystem withCurrHeartbeats)
   We used a similar hack at `Exception.isMaxRecDepth` -/
 def Exception.isMaxHeartbeat (ex : Exception) : Bool :=
   match ex with
-  | Exception.error _ (MessageData.ofFormat (Std.Format.text msg)) => "(deterministic) timeout".isPrefixOf msg
+  | Exception.error _ (MessageData.ofFormatWithInfos ⟨Std.Format.text msg, _⟩) =>
+    "(deterministic) timeout".isPrefixOf msg
   | _ => false
 
 /-- Creates the expression `d → b` -/

src/Lean/Elab/Calc.lean

@@ -112,10 +112,12 @@ def elabCalcSteps (steps : TSyntax ``calcSteps) : TermElabM Expr := do
   return result?.get!.1
 
 /-- Elaborator for the `calc` term mode variant. -/
-@[builtin_term_elab «calc»]
+@[builtin_term_elab Lean.calc]
 def elabCalc : TermElab := fun stx expectedType? => do
   let steps : TSyntax ``calcSteps := ⟨stx[1]⟩
   let result ← elabCalcSteps steps
   synthesizeSyntheticMVarsUsingDefault
   let result ← ensureHasType expectedType? result
   return result
+
+end Lean.Elab.Term

src/Lean/Elab/Extra.lean

@@ -241,7 +241,10 @@ private def hasCoe (fromType toType : Expr) : TermElabM Bool := do
 
 private structure AnalyzeResult where
   max?            : Option Expr := none
-  hasUncomparable : Bool := false -- `true` if there are two types `α` and `β` where we don't have coercions in any direction.
+  /-- `true` if there are two types `α` and `β` where we don't have coercions in any direction. -/
+  hasUncomparable : Bool := false
+  /-- `true` if there are any leaf terms with an unknown type (according to `isUnknown`). -/
+  hasUnknown      : Bool := false
 
 private def isUnknown : Expr → Bool
   | .mvar ..        => true
@@ -255,7 +258,7 @@ private def analyze (t : Tree) (expectedType? : Option Expr) : TermElabM Analyze
     match expectedType? with
     | none => pure none
     | some expectedType =>
-      let expectedType ← instantiateMVars expectedType
+      let expectedType := (← instantiateMVars expectedType).cleanupAnnotations
       if isUnknown expectedType then pure none else pure (some expectedType)
   (go t *> get).run' { max? }
 where
@@ -268,8 +271,10 @@ where
        | .binop _ _ _ lhs rhs => go lhs; go rhs
        | .unop _ _ arg => go arg
        | .term _ _ val =>
-         let type ← instantiateMVars (← inferType val)
-         unless isUnknown type do
+         let type := (← instantiateMVars (← inferType val)).cleanupAnnotations
+         if isUnknown type then
+           modify fun s => { s with hasUnknown := true }
+         else
            match (← get).max? with
            | none     => modify fun s => { s with max? := type }
            | some max =>
@@ -430,7 +435,7 @@ mutual
       | .unop ref f arg =>
         return .unop ref f (← go arg none false false)
       | .term ref trees e =>
-        let type ← instantiateMVars (← inferType e)
+        let type := (← instantiateMVars (← inferType e)).cleanupAnnotations
         trace[Elab.binop] "visiting {e} : {type} =?= {maxType}"
         if isUnknown type then
           if let some f := f? then
@@ -448,12 +453,17 @@ mutual
 
   private partial def toExpr (tree : Tree) (expectedType? : Option Expr) : TermElabM Expr := do
     let r ← analyze tree expectedType?
-    trace[Elab.binop] "hasUncomparable: {r.hasUncomparable}, maxType: {r.max?}"
+    trace[Elab.binop] "hasUncomparable: {r.hasUncomparable}, hasUnknown: {r.hasUnknown}, maxType: {r.max?}"
     if r.hasUncomparable || r.max?.isNone then
       let result ← toExprCore tree
       ensureHasType expectedType? result
     else
       let result ← toExprCore (← applyCoe tree r.max?.get! (isPred := false))
+      unless r.hasUnknown do
+        -- Record the resulting maxType calculation.
+        -- We can do this when all the types are known, since in this case `hasUncomparable` is valid.
+        -- If they're not known, recording maxType like this can lead to heterogeneous operations failing to elaborate.
+        discard <| isDefEqGuarded (← inferType result) r.max?.get!
       trace[Elab.binop] "result: {result}"
       ensureHasType expectedType? result
 
@@ -519,7 +529,7 @@ def elabBinRelCore (noProp : Bool) (stx : Syntax) (expectedType? : Option Expr)
     let rhs ← withRef rhsStx <| toTree rhsStx
     let tree := .binop stx .regular f lhs rhs
     let r ← analyze tree none
-    trace[Elab.binrel] "hasUncomparable: {r.hasUncomparable}, maxType: {r.max?}"
+    trace[Elab.binrel] "hasUncomparable: {r.hasUncomparable}, hasUnknown: {r.hasUnknown}, maxType: {r.max?}"
     if r.hasUncomparable || r.max?.isNone then
       -- Use default elaboration strategy + `toBoolIfNecessary`
       let lhs ← toExprCore lhs

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -123,7 +123,7 @@ def evalSepByIndentTactic (stx : Syntax) : TacticM Unit := do
     withInfoContext (pure ()) initInfo
     evalSepByIndentTactic stx[1]
 
-@[builtin_tactic cdot] def evalTacticCDot : Tactic := fun stx => do
+@[builtin_tactic Lean.cdot] def evalTacticCDot : Tactic := fun stx => do
   -- adjusted copy of `evalTacticSeqBracketed`; we used to use the macro
   -- ``| `(tactic| $cdot:cdotTk $tacs) => `(tactic| {%$cdot ($tacs) }%$cdot)``
   -- but the token antiquotation does not copy trailing whitespace, leading to

src/Lean/Elab/Tactic/Calc.lean

@@ -11,7 +11,7 @@ namespace Lean.Elab.Tactic
 open Meta
 
 /-- Elaborator for the `calc` tactic mode variant. -/
-@[builtin_tactic calcTactic]
+@[builtin_tactic Lean.calcTactic]
 def evalCalc : Tactic := fun stx => withMainContext do
   let steps : TSyntax ``calcSteps := ⟨stx[1]⟩
   let (val, mvarIds) ← withCollectingNewGoalsFrom (tagSuffix := `calc) do
@@ -32,3 +32,5 @@ def evalCalc : Tactic := fun stx => withMainContext do
     return val
   (← getMainGoal).assign val
   replaceMainGoal mvarIds
+
+end Lean.Elab.Tactic

src/Lean/Elab/Tactic/Omega/OmegaM.lean

@@ -71,7 +71,7 @@ abbrev OmegaM := StateRefT Cache OmegaM'
 
 /-- Run a computation in the `OmegaM` monad, starting with no recorded atoms. -/
 def OmegaM.run (m : OmegaM α) (cfg : OmegaConfig) : MetaM α :=
-  m.run' HashMap.empty |>.run' {} { cfg } |>.run
+  m.run' HashMap.empty |>.run' {} { cfg } |>.run'
 
 /-- Retrieve the user-specified configuration options. -/
 def cfg : OmegaM OmegaConfig := do pure (← read).cfg

src/Lean/Exception.lean

@@ -130,7 +130,7 @@ been defined yet.
 -/
 def Exception.isMaxRecDepth (ex : Exception) : Bool :=
   match ex with
-  | error _ (MessageData.ofFormat (Std.Format.text msg)) => msg == maxRecDepthErrorMessage
+  | error _ (MessageData.ofFormatWithInfos ⟨Std.Format.text msg, _⟩) => msg == maxRecDepthErrorMessage
   | _ => false
 
 /--

src/Lean/Message.lean

@@ -39,13 +39,6 @@ structure NamingContext where
   currNamespace : Name
   openDecls : List OpenDecl
 
-/-- Lazily formatted text to be used in `MessageData`. -/
-structure PPFormat where
-  /-- Pretty-prints text using surrounding context, if any. -/
-  pp : Option PPContext → IO FormatWithInfos
-  /-- Searches for synthetic sorries in original input. Used to filter out certain messages. -/
-  hasSyntheticSorry : MetavarContext → Bool := fun _ => false
-
 structure TraceData where
   /-- Trace class, e.g. `Elab.step`. -/
   cls       : Name
@@ -60,10 +53,9 @@ structure TraceData where
 
 /-- Structured message data. We use it for reporting errors, trace messages, etc. -/
 inductive MessageData where
-  /-- Eagerly formatted text. We inspect this in various hacks, so it is not immediately subsumed by `ofPPFormat`. -/
-  | ofFormat          : Format → MessageData
-  /-- Lazily formatted text. -/
-  | ofPPFormat        : PPFormat → MessageData
+  /-- Eagerly formatted text with info annotations.
+  This constructor is inspected in various hacks. -/
+  | ofFormatWithInfos : FormatWithInfos → MessageData
   | ofGoal            : MVarId → MessageData
   /-- `withContext ctx d` specifies the pretty printing context `(env, mctx, lctx, opts)` for the nested expressions in `d`. -/
   | withContext       : MessageDataContext → MessageData → MessageData
@@ -78,12 +70,45 @@ inductive MessageData where
     Example: an inspector that tries to find "definitional equality failures" may look for the tag "DefEqFailure". -/
   | tagged            : Name → MessageData → MessageData
   | trace (data : TraceData) (msg : MessageData) (children : Array MessageData)
-  deriving Inhabited
+  /-- A lazy message.
+  The provided thunk will not be run until it is about to be displayed.
+  This can save computation in cases where the message may never be seen,
+  e.g. when nested inside a collapsed trace.
+
+  The `Dynamic` value is expected to be a `MessageData`,
+  which is a workaround for the positivity restriction.
+     
+  If the thunked message is produced for a term that contains a synthetic sorry,
+  `hasSyntheticSorry` should return `true`.
+  This is used to filter out certain messages. -/
+  | ofLazy (f : Option PPContext → IO Dynamic) (hasSyntheticSorry : MetavarContext → Bool)
+  deriving Inhabited, TypeName
 
 namespace MessageData
 
+/-- Eagerly formatted text. -/
+def ofFormat (fmt : Format) : MessageData := .ofFormatWithInfos ⟨fmt, .empty⟩
+
+/--
+Lazy message data production, with access to the context as given by
+a surrounding `MessageData.withContext` (which is expected to exist).
+-/
+def lazy (f : PPContext → IO MessageData)
+    (hasSyntheticSorry : MetavarContext → Bool := fun _ => false) : MessageData :=
+  .ofLazy (hasSyntheticSorry := hasSyntheticSorry) fun ctx? => do
+    let msg ← match ctx? with
+      | .none => pure (.ofFormat "(invalid MessageData.lazy, missing context)")
+      | .some ctx => f ctx
+    return Dynamic.mk msg
+
 variable (p : Name → Bool) in
-/-- Returns true when the message contains a `MessageData.tagged tag ..` constructor where `p tag` is true. -/
+/-- Returns true when the message contains a `MessageData.tagged tag ..` constructor where `p tag`
+is true.
+
+This does not descend into lazily generated subtress (`.ofLazy`); message tags
+of interest (like those added by `logLinter`) are expected to be near the root
+of the `MessageData`, and not hidden inside `.ofLazy`.
+-/
 partial def hasTag : MessageData → Bool
   | withContext _ msg       => hasTag msg
   | withNamingContext _ msg => hasTag msg
@@ -106,26 +131,14 @@ def mkPPContext (nCtx : NamingContext) (ctx : MessageDataContext) : PPContext :=
 def ofSyntax (stx : Syntax) : MessageData :=
   -- discard leading/trailing whitespace
   let stx := stx.copyHeadTailInfoFrom .missing
-  .ofPPFormat {
-    pp := fun
-      | some ctx => ppTerm ctx ⟨stx⟩  -- HACK: might not be a term
-      | none     => return stx.formatStx
-  }
+  .lazy fun ctx => ofFormat <$> ppTerm ctx ⟨stx⟩ -- HACK: might not be a term
 
 def ofExpr (e : Expr) : MessageData :=
-  .ofPPFormat {
-    pp := fun
-      | some ctx => ppExprWithInfos ctx e
-      | none     => return format (toString e)
-    hasSyntheticSorry := (instantiateMVarsCore · e |>.1.hasSyntheticSorry)
-  }
+  .lazy (fun ctx => ofFormatWithInfos <$> ppExprWithInfos ctx e)
+        (fun mctx => instantiateMVarsCore mctx e |>.1.hasSyntheticSorry)
 
 def ofLevel (l : Level) : MessageData :=
-  .ofPPFormat {
-    pp := fun
-      | some ctx => ppLevel ctx l
-      | none => return format l
-  }
+  .lazy fun ctx => ofFormat <$> ppLevel ctx l
 
 def ofName (n : Name) : MessageData := ofFormat (format n)
 
@@ -133,7 +146,7 @@ partial def hasSyntheticSorry (msg : MessageData) : Bool :=
   visit none msg
 where
   visit (mctx? : Option MetavarContext) : MessageData → Bool
-  | ofPPFormat f            => f.hasSyntheticSorry (mctx?.getD {})
+  | ofLazy _ f              => f (mctx?.getD {})
   | withContext ctx msg     => visit ctx.mctx msg
   | withNamingContext _ msg => visit mctx? msg
   | nest _ msg              => visit mctx? msg
@@ -144,8 +157,7 @@ where
   | _                       => false
 
 partial def formatAux : NamingContext → Option MessageDataContext → MessageData → IO Format
-  | _,    _,         ofFormat fmt             => return fmt
-  | nCtx, ctx?,      ofPPFormat f             => (·.fmt) <$> f.pp (ctx?.map (mkPPContext nCtx))
+  | _, _,            ofFormatWithInfos fmt    => return fmt.1
   | _,    none,      ofGoal mvarId            => return "goal " ++ format (mkMVar mvarId)
   | nCtx, some ctx,  ofGoal mvarId            => ppGoal (mkPPContext nCtx ctx) mvarId
   | nCtx, _,         withContext ctx d        => formatAux nCtx ctx d
@@ -161,6 +173,11 @@ partial def formatAux : NamingContext → Option MessageDataContext → MessageD
     msg := f!"{msg} {(← formatAux nCtx ctx header).nest 2}"
     let children ← children.mapM (formatAux nCtx ctx)
     return .nest 2 (.joinSep (msg::children.toList) "\n")
+  | nCtx, ctx?,      ofLazy pp _             => do
+    let dyn ← pp (ctx?.map (mkPPContext nCtx))
+    let some msg := dyn.get? MessageData
+      | panic! s!"MessageData.ofLazy: expected MessageData in Dynamic, got {dyn.typeName}"
+    formatAux nCtx ctx? msg
 
 protected def format (msgData : MessageData) : IO Format :=
   formatAux { currNamespace := Name.anonymous, openDecls := [] } none msgData

src/Lean/Meta/Basic.lean

@@ -720,15 +720,18 @@ def isReadOnlyExprMVar (mvarId : MVarId) : MetaM Bool := do
   mvarId.isReadOnly
 
 /--
-Return true if `mvarId.isReadOnly` return true or if `mvarId` is a synthetic opaque metavariable.
+Returns true if `mvarId.isReadOnly` returns true or if `mvarId` is a synthetic opaque metavariable.
 
 Recall `isDefEq` will not assign a value to `mvarId` if `mvarId.isReadOnlyOrSyntheticOpaque`.
 -/
 def _root_.Lean.MVarId.isReadOnlyOrSyntheticOpaque (mvarId : MVarId) : MetaM Bool := do
   let mvarDecl ← mvarId.getDecl
-  match mvarDecl.kind with
-  | MetavarKind.syntheticOpaque => return !(← getConfig).assignSyntheticOpaque
-  | _ => return mvarDecl.depth != (← getMCtx).depth
+  if mvarDecl.depth != (← getMCtx).depth then
+    return true
+  else
+    match mvarDecl.kind with
+    | MetavarKind.syntheticOpaque => return !(← getConfig).assignSyntheticOpaque
+    | _ => return false
 
 @[deprecated MVarId.isReadOnlyOrSyntheticOpaque (since := "2022-07-15")]
 def isReadOnlyOrSyntheticOpaqueExprMVar (mvarId : MVarId) : MetaM Bool := do
@@ -825,6 +828,17 @@ context. Fails if the given expression is not a fvar or if no such declaration e
 def getFVarLocalDecl (fvar : Expr) : MetaM LocalDecl :=
   fvar.fvarId!.getDecl
 
+/--
+Returns `true` if another local declaration in the local context depends on `fvarId`.
+-/
+def _root_.Lean.FVarId.hasForwardDeps (fvarId : FVarId) : MetaM Bool := do
+  let decl ← fvarId.getDecl
+  (← getLCtx).foldlM (init := false) (start := decl.index + 1) fun found other =>
+    if found then
+      return true
+    else
+      localDeclDependsOn other fvarId
+
 /--
 Given a user-facing name for a free variable, return its declaration in the current local context.
 Throw an exception if free variable is not declared.
@@ -1446,7 +1460,9 @@ def withLocalInstancesImp (decls : List LocalDecl) (k : MetaM α) : MetaM α :=
   for decl in decls do
     unless decl.isImplementationDetail do
       if let some className ← isClass? decl.type then
-        localInsts := localInsts.push { className, fvar := decl.toExpr }
+        -- Ensure we don't add the same local instance multiple times.
+        unless localInsts.any fun localInst => localInst.fvar.fvarId! == decl.fvarId do
+          localInsts := localInsts.push { className, fvar := decl.toExpr }
   if localInsts.size == size then
     k
   else

src/Lean/Meta/Canonicalizer.lean

@@ -63,8 +63,11 @@ abbrev CanonM := ReaderT TransparencyMode $ StateRefT State MetaM
 The definitionally equality tests are performed using the given transparency mode.
 We claim `TransparencyMode.instances` is a good setting for most applications.
 -/
-def CanonM.run (x : CanonM α) (transparency := TransparencyMode.instances) : MetaM α :=
-  StateRefT'.run' (x transparency) {}
+def CanonM.run' (x : CanonM α) (transparency := TransparencyMode.instances) (s : State := {}) : MetaM α :=
+  StateRefT'.run' (x transparency) s
+
+def CanonM.run (x : CanonM α) (transparency := TransparencyMode.instances) (s : State := {}) : MetaM (α × State) :=
+  StateRefT'.run (x transparency) s
 
 private partial def mkKey (e : Expr) : CanonM UInt64 := do
   if let some hash := unsafe (← get).cache.find? { e } then

src/Lean/Meta/ExprDefEq.lean

@@ -740,58 +740,59 @@ mutual
     if mvarId == ctx.mvarId then
       traceM `Meta.isDefEq.assign.occursCheck <| addAssignmentInfo "occurs check failed"
       throwCheckAssignmentFailure
-    else match (← getExprMVarAssignment? mvarId) with
-      | some v => check v
-      | none   =>
-        match (← mvarId.findDecl?) with
-        | none          => throwUnknownMVar mvarId
-        | some mvarDecl =>
-          if ctx.hasCtxLocals then
-            throwCheckAssignmentFailure -- It is not a pattern, then we fail and fall back to FO unification
-          else if mvarDecl.lctx.isSubPrefixOf ctx.mvarDecl.lctx ctx.fvars then
-            /- The local context of `mvar` - free variables being abstracted is a subprefix of the metavariable being assigned.
-               We "subtract" variables being abstracted because we use `elimMVarDeps` -/
-            pure mvar
-          else if mvarDecl.depth != (← getMCtx).depth || mvarDecl.kind.isSyntheticOpaque then
-            traceM `Meta.isDefEq.assign.readOnlyMVarWithBiggerLCtx <| addAssignmentInfo (mkMVar mvarId)
-            throwCheckAssignmentFailure
-          else
-            let ctxMeta ← readThe Meta.Context
-            if ctxMeta.config.ctxApprox && ctx.mvarDecl.lctx.isSubPrefixOf mvarDecl.lctx then
-              /- Create an auxiliary metavariable with a smaller context and "checked" type.
-                 Note that `mvarType` may be different from `mvarDecl.type`. Example: `mvarType` contains
-                 a metavariable that we also need to reduce the context.
+    if let some v ← getExprMVarAssignment? mvarId then
+      return (← check v)
+    let some mvarDecl ← mvarId.findDecl?
+      | throwUnknownMVar mvarId
+    if ctx.hasCtxLocals then
+      throwCheckAssignmentFailure -- It is not a pattern, then we fail and fall back to FO unification
+    if let some d ← getDelayedMVarAssignment? mvarId then
+      -- we must perform occurs-check at `d.mvarIdPending`
+      unless (← occursCheck ctx.mvarId (mkMVar d.mvarIdPending)) do
+        traceM `Meta.isDefEq.assign.occursCheck <| addAssignmentInfo "occurs check failed"
+        throwCheckAssignmentFailure
+    if mvarDecl.lctx.isSubPrefixOf ctx.mvarDecl.lctx ctx.fvars then
+      /- The local context of `mvar` - free variables being abstracted is a subprefix of the metavariable being assigned.
+         We "subtract" variables being abstracted because we use `elimMVarDeps` -/
+      return mvar
+    if mvarDecl.depth != (← getMCtx).depth || mvarDecl.kind.isSyntheticOpaque then
+      traceM `Meta.isDefEq.assign.readOnlyMVarWithBiggerLCtx <| addAssignmentInfo (mkMVar mvarId)
+      throwCheckAssignmentFailure
+    let ctxMeta ← readThe Meta.Context
+    unless ctxMeta.config.ctxApprox && ctx.mvarDecl.lctx.isSubPrefixOf mvarDecl.lctx do
+      traceM `Meta.isDefEq.assign.readOnlyMVarWithBiggerLCtx <| addAssignmentInfo (mkMVar mvarId)
+      throwCheckAssignmentFailure
+    /- Create an auxiliary metavariable with a smaller context and "checked" type.
+       Note that `mvarType` may be different from `mvarDecl.type`. Example: `mvarType` contains
+       a metavariable that we also need to reduce the context.
 
-                 We remove from `ctx.mvarDecl.lctx` any variable that is not in `mvarDecl.lctx`
-                 or in `ctx.fvars`. We don't need to remove the ones in `ctx.fvars` because
-                 `elimMVarDeps` will take care of them.
+       We remove from `ctx.mvarDecl.lctx` any variable that is not in `mvarDecl.lctx`
+       or in `ctx.fvars`. We don't need to remove the ones in `ctx.fvars` because
+       `elimMVarDeps` will take care of them.
 
-                 First, we collect `toErase` the variables that need to be erased.
-                 Notat that if a variable is `ctx.fvars`, but it depends on variable at `toErase`,
-                 we must also erase it.
-              -/
-              let toErase ← mvarDecl.lctx.foldlM (init := #[]) fun toErase localDecl => do
-                if ctx.mvarDecl.lctx.contains localDecl.fvarId then
-                  return toErase
-                else if ctx.fvars.any fun fvar => fvar.fvarId! == localDecl.fvarId then
-                  if (← findLocalDeclDependsOn localDecl fun fvarId => toErase.contains fvarId) then
-                    -- localDecl depends on a variable that will be erased. So, we must add it to `toErase` too
-                    return toErase.push localDecl.fvarId
-                  else
-                    return toErase
-                else
-                  return toErase.push localDecl.fvarId
-              let lctx := toErase.foldl (init := mvarDecl.lctx) fun lctx toEraseFVar =>
-                lctx.erase toEraseFVar
-              /- Compute new set of local instances. -/
-              let localInsts := mvarDecl.localInstances.filter fun localInst => !toErase.contains localInst.fvar.fvarId!
-              let mvarType ← check mvarDecl.type
-              let newMVar ← mkAuxMVar lctx localInsts mvarType mvarDecl.numScopeArgs
-              mvarId.assign newMVar
-              pure newMVar
-            else
-              traceM `Meta.isDefEq.assign.readOnlyMVarWithBiggerLCtx <| addAssignmentInfo (mkMVar mvarId)
-              throwCheckAssignmentFailure
+       First, we collect `toErase` the variables that need to be erased.
+       Notat that if a variable is `ctx.fvars`, but it depends on variable at `toErase`,
+       we must also erase it.
+    -/
+    let toErase ← mvarDecl.lctx.foldlM (init := #[]) fun toErase localDecl => do
+      if ctx.mvarDecl.lctx.contains localDecl.fvarId then
+        return toErase
+      else if ctx.fvars.any fun fvar => fvar.fvarId! == localDecl.fvarId then
+        if (← findLocalDeclDependsOn localDecl fun fvarId => toErase.contains fvarId) then
+          -- localDecl depends on a variable that will be erased. So, we must add it to `toErase` too
+          return toErase.push localDecl.fvarId
+        else
+          return toErase
+      else
+        return toErase.push localDecl.fvarId
+    let lctx := toErase.foldl (init := mvarDecl.lctx) fun lctx toEraseFVar =>
+      lctx.erase toEraseFVar
+    /- Compute new set of local instances. -/
+    let localInsts := mvarDecl.localInstances.filter fun localInst => !toErase.contains localInst.fvar.fvarId!
+    let mvarType ← check mvarDecl.type
+    let newMVar ← mkAuxMVar lctx localInsts mvarType mvarDecl.numScopeArgs
+    mvarId.assign newMVar
+    return newMVar
 
   /--
     Auxiliary function used to "fix" subterms of the form `?m x_1 ... x_n` where `x_i`s are free variables,
@@ -802,12 +803,10 @@ mutual
   partial def assignToConstFun (mvar : Expr) (numArgs : Nat) (newMVar : Expr) : MetaM Bool := do
     let mvarType ← inferType mvar
     forallBoundedTelescope mvarType numArgs fun xs _ => do
-      if xs.size != numArgs then pure false
-      else
-        let some v ← mkLambdaFVarsWithLetDeps xs newMVar | return false
-        match (← checkAssignmentAux mvar.mvarId! #[] false v) with
-        | some v => checkTypesAndAssign mvar v
-        | none   => return false
+      if xs.size != numArgs then return false
+      let some v ← mkLambdaFVarsWithLetDeps xs newMVar | return false
+      let some v ← checkAssignmentAux mvar.mvarId! #[] false v | return false
+      checkTypesAndAssign mvar v
 
   -- See checkAssignment
   partial def checkAssignmentAux (mvarId : MVarId) (fvars : Array Expr) (hasCtxLocals : Bool) (v : Expr) : MetaM (Option Expr) := do
@@ -825,19 +824,18 @@ mutual
           (fun ex => do
             if !f.isMVar then
               throw ex
-            else if (← f.mvarId!.isDelayedAssigned) then
+            if (← f.mvarId!.isDelayedAssigned) then
               throw ex
+            let eType ← inferType e
+            let mvarType ← check eType
+            /- Create an auxiliary metavariable with a smaller context and "checked" type, assign `?f := fun _ => ?newMVar`
+               Note that `mvarType` may be different from `eType`. -/
+            let ctx ← read
+            let newMVar ← mkAuxMVar ctx.mvarDecl.lctx ctx.mvarDecl.localInstances mvarType
+            if (← assignToConstFun f args.size newMVar) then
+              pure newMVar
             else
-              let eType ← inferType e
-              let mvarType ← check eType
-              /- Create an auxiliary metavariable with a smaller context and "checked" type, assign `?f := fun _ => ?newMVar`
-                    Note that `mvarType` may be different from `eType`. -/
-              let ctx ← read
-              let newMVar ← mkAuxMVar ctx.mvarDecl.lctx ctx.mvarDecl.localInstances mvarType
-              if (← assignToConstFun f args.size newMVar) then
-                pure newMVar
-              else
-                throw ex)
+              throw ex)
       else
         let f ← check f
         let args ← args.mapM check
@@ -900,38 +898,33 @@ namespace CheckAssignmentQuick
 partial def check
     (hasCtxLocals : Bool)
     (mctx : MetavarContext) (lctx : LocalContext) (mvarDecl : MetavarDecl) (mvarId : MVarId) (fvars : Array Expr) (e : Expr) : Bool :=
-  let rec visit (e : Expr) : Bool :=
+  let rec visit (e : Expr) : Bool := Id.run do
     if !e.hasExprMVar && !e.hasFVar then
-      true
-    else match e with
+      return true
+    match e with
     | .mdata _ b       => visit b
     | .proj _ _ s      => visit s
     | .app f a         => visit f && visit a
     | .lam _ d b _     => visit d && visit b
     | .forallE _ d b _ => visit d && visit b
     | .letE _ t v b _  => visit t && visit v && visit b
-    | .bvar ..         => true
-    | .sort ..         => true
-    | .const ..        => true
-    | .lit ..          => true
+    | .bvar .. | .sort .. | .const ..
+    | .lit .. => return true
     | .fvar fvarId ..  =>
-      if mvarDecl.lctx.contains fvarId then true
-      else match lctx.find? fvarId with
-        | some (LocalDecl.ldecl ..) => false -- need expensive CheckAssignment.check
-        | _ =>
-          if fvars.any fun x => x.fvarId! == fvarId then true
-          else false -- We could throw an exception here, but we would have to use ExceptM. So, we let CheckAssignment.check do it
+      if mvarDecl.lctx.contains fvarId then return true
+      if let some (LocalDecl.ldecl ..) := lctx.find? fvarId then
+        return false -- need expensive CheckAssignment.check
+      if fvars.any fun x => x.fvarId! == fvarId then
+        return true
+      return false -- We could throw an exception here, but we would have to use ExceptM. So, we let CheckAssignment.check do it
     | .mvar mvarId'    =>
-      match mctx.getExprAssignmentCore? mvarId' with
-      | some _ => false -- use CheckAssignment.check to instantiate
-      | none   =>
-        if mvarId' == mvarId then false -- occurs check failed, use CheckAssignment.check to throw exception
-        else match mctx.findDecl? mvarId' with
-          | none           => false
-          | some mvarDecl' =>
-            if hasCtxLocals then false -- use CheckAssignment.check
-            else if mvarDecl'.lctx.isSubPrefixOf mvarDecl.lctx fvars then true
-            else false -- use CheckAssignment.check
+      let none := mctx.getExprAssignmentCore? mvarId' | return false -- use CheckAssignment.check to instantiate
+      if mvarId' == mvarId then return false -- occurs check failed, use CheckAssignment.check to throw exception
+      let some mvarDecl' := mctx.findDecl? mvarId' | return false
+      if hasCtxLocals then return false -- use CheckAssignment.check
+      if !mvarDecl'.lctx.isSubPrefixOf mvarDecl.lctx fvars then return false -- use CheckAssignment.check
+      let none := mctx.getDelayedMVarAssignmentCore? mvarId' | return false -- use CheckAssignment.check
+      return true
   visit e
 
 end CheckAssignmentQuick

src/Lean/Meta/SynthInstance.lean

@@ -561,11 +561,17 @@ def generate : SynthM Unit := do
     if backward.synthInstance.canonInstances.get (← getOptions) then
       unless gNode.typeHasMVars do
         if let some entry := (← get).tableEntries.find? key then
-          unless entry.answers.isEmpty do
+          if entry.answers.any fun answer => answer.result.numMVars == 0 then
             /-
-            We already have an answer for this node, and since its type does not have metavariables,
-            we can skip other solutions because we assume instances are "morally canonical".
+            We already have an answer that:
+              1. its result does not have metavariables.
+              2. its types do not have metavariables.
+
+            Thus, we can skip other solutions because we assume instances are "morally canonical".
             We have added this optimization to address issue #3996.
+
+            Remark: Condition 1 is important since root nodes only take into account results
+            that do **not** contain metavariables. This extra check was added to address issue #4213.
             -/
             modify fun s => { s with generatorStack := s.generatorStack.pop }
             return

src/Lean/Meta/Tactic/Apply.lean

@@ -8,6 +8,7 @@ import Lean.Util.FindMVar
 import Lean.Meta.SynthInstance
 import Lean.Meta.CollectMVars
 import Lean.Meta.Tactic.Util
+import Lean.PrettyPrinter
 
 namespace Lean.Meta
 /-- Controls which new mvars are turned in to goals by the `apply` tactic.
@@ -50,8 +51,15 @@ def getExpectedNumArgs (e : Expr) : MetaM Nat := do
   let (numArgs, _) ← getExpectedNumArgsAux e
   pure numArgs
 
-private def throwApplyError {α} (mvarId : MVarId) (eType : Expr) (targetType : Expr) : MetaM α :=
-  throwTacticEx `apply mvarId m!"failed to unify{indentExpr eType}\nwith{indentExpr targetType}"
+private def throwApplyError {α} (mvarId : MVarId) (eType : Expr) (targetType : Expr) : MetaM α := do
+  let explanation := MessageData.lazy
+    (f := fun ppctxt => ppctxt.runMetaM do
+        let (eType, targetType) ← addPPExplicitToExposeDiff eType targetType
+        return m!"{indentExpr eType}\nwith{indentExpr targetType}")
+    (hasSyntheticSorry := fun mvarctxt =>
+      (instantiateMVarsCore mvarctxt eType |>.1.hasSyntheticSorry) ||
+      (instantiateMVarsCore mvarctxt targetType |>.1.hasSyntheticSorry))
+  throwTacticEx `apply mvarId m!"failed to unify{explanation}"
 
 def synthAppInstances (tacticName : Name) (mvarId : MVarId) (newMVars : Array Expr) (binderInfos : Array BinderInfo)
     (synthAssignedInstances : Bool) (allowSynthFailures : Bool) : MetaM Unit :=

src/Lean/Meta/Tactic/Grind.lean

@@ -6,6 +6,6 @@ Authors: Leonardo de Moura
 prelude
 import Lean.Meta.Tactic.Grind.Attr
 import Lean.Meta.Tactic.Grind.RevertAll
-import Lean.Meta.Tactic.Grind.EnsureNoMVar
 import Lean.Meta.Tactic.Grind.Types
 import Lean.Meta.Tactic.Grind.Preprocessor
+import Lean.Meta.Tactic.Grind.Util

src/Lean/Meta/Tactic/Grind/EnsureNoMVar.lean

@@ -1,19 +0,0 @@
-/-
-Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Lean.Meta.Tactic.Util
-
-namespace Lean.Meta.Grind
-
-/--
-Throws an exception if target of the given goal contains metavariables.
--/
-def _root_.Lean.MVarId.ensureNoMVar (mvarId : MVarId) : MetaM Unit := do
-  let type ← instantiateMVars (← mvarId.getType)
-  if type.hasExprMVar then
-    throwTacticEx `grind mvarId "goal contains metavariables"
-
-end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/Preprocessor.lean

@@ -4,14 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Init.Grind.Lemmas
 import Lean.Meta.Canonicalizer
 import Lean.Meta.Tactic.Util
 import Lean.Meta.Tactic.Intro
 import Lean.Meta.Tactic.Simp.Main
 import Lean.Meta.Tactic.Grind.Attr
 import Lean.Meta.Tactic.Grind.RevertAll
-import Lean.Meta.Tactic.Grind.EnsureNoMVar
 import Lean.Meta.Tactic.Grind.Types
+import Lean.Meta.Tactic.Grind.Util
 
 namespace Lean.Meta.Grind
 namespace Preprocessor
@@ -25,99 +26,113 @@ structure Context where
   deriving Inhabited
 
 structure State where
-  canon : Canonicalizer.State := {}
-  todo  : List Goal := []
-  goals : PArray Goal := {}
   simpStats : Simp.Stats := {}
   deriving Inhabited
 
-structure Result where
-  canon : Canonicalizer.State := {}
-  goals : PArray Goal := {}
-  deriving Inhabited
+abbrev PreM := ReaderT Context $ StateRefT State GrindM
 
-abbrev M := ReaderT Context $ StateRefT State MetaM
-
-def mkInitialState (mvarId : MVarId) : State :=
-  { todo := [ mkGoal mvarId ] }
-
-def M.run (x : M α) (mvarId : MVarId) : MetaM α := do
+def PreM.run (x : PreM α) : GrindM α := do
   let thms ← grindNormExt.getTheorems
   let simprocs := #[(← grindNormSimprocExt.getSimprocs)]
   let simp : Simp.Context := {
+    config := { arith := true }
     simpTheorems := #[thms]
     congrTheorems := (← getSimpCongrTheorems)
   }
-  x { simp, simprocs } |>.run' (mkInitialState mvarId)
+  x { simp, simprocs } |>.run' {}
 
-def simpHyp? (mvarId : MVarId) (fvarId : FVarId) : M (Option (FVarId × MVarId)) := do
+def simp (e : Expr) : PreM Simp.Result := do
+  let simpStats := (← get).simpStats
+  let (r, simpStats) ← Meta.simp e (← read).simp (← read).simprocs (stats := simpStats)
+  modify fun s => { s with simpStats }
+  return r
+
+def simpHyp? (mvarId : MVarId) (fvarId : FVarId) : PreM (Option (FVarId × MVarId)) := do
   let simpStats := (← get).simpStats
   let (result, simpStats) ← simpLocalDecl mvarId fvarId (← read).simp (← read).simprocs (stats := simpStats)
   modify fun s => { s with simpStats }
   return result
 
-def getNextGoal? : M (Option Goal) := do
-  match (← get).todo with
-  | [] => return none
-  | goal :: todo =>
-    modify fun s => { s with todo }
-    return some goal
-
 inductive IntroResult where
-  | done | closed
+  | done
   | newHyp (fvarId : FVarId) (goal : Goal)
   | newLocal (fvarId : FVarId) (goal : Goal)
 
-def introNext (goal : Goal) : M IntroResult := do
+def introNext (goal : Goal) : PreM IntroResult := do
   let target ← goal.mvarId.getType
   if target.isArrow then
-    let (fvarId, mvarId) ← goal.mvarId.intro1P
-    -- TODO: canonicalize subterms
-    mvarId.withContext do
-    if (← isProp (← fvarId.getType)) then
-      let some (fvarId, mvarId) ← simpHyp? mvarId fvarId | return .closed
-      return .newHyp fvarId { goal with mvarId }
-    else
-      return .newLocal fvarId { goal with mvarId }
+    goal.mvarId.withContext do
+      let p := target.bindingDomain!
+      if !(← isProp p) then
+        let (fvarId, mvarId) ← goal.mvarId.intro1P
+        return .newLocal fvarId { goal with mvarId }
+      else
+        let tag ← goal.mvarId.getTag
+        let q := target.bindingBody!
+        let r ← simp p
+        let p' := r.expr
+        let p' ← canon p'
+        let p' ← shareCommon p'
+        let fvarId ← mkFreshFVarId
+        let lctx := (← getLCtx).mkLocalDecl fvarId target.bindingName! p' target.bindingInfo!
+        let mvarNew ← mkFreshExprMVarAt lctx (← getLocalInstances) q .syntheticOpaque tag
+        let mvarIdNew := mvarNew.mvarId!
+        mvarIdNew.withContext do
+          let h ← mkLambdaFVars #[mkFVar fvarId] mvarNew
+          match r.proof? with
+          | some he =>
+            let hNew := mkAppN (mkConst ``Lean.Grind.intro_with_eq) #[p, p', q, he, h]
+            goal.mvarId.assign hNew
+            return .newHyp fvarId { goal with mvarId := mvarIdNew }
+          | none =>
+            -- `p` and `p'` are definitionally equal
+            goal.mvarId.assign h
+            return .newHyp fvarId { goal with mvarId := mvarIdNew }
   else if target.isLet || target.isForall then
-    -- TODO: canonicalize subterms
-    -- TODO: If forall is of the form `∀ h : <proposition>, A h`, generalize `h`.
     let (fvarId, mvarId) ← goal.mvarId.intro1P
-    return .newLocal fvarId { goal with mvarId }
+    mvarId.withContext do
+      let localDecl ← fvarId.getDecl
+      if (← isProp localDecl.type) then
+        -- Add a non-dependent copy
+        let mvarId ← mvarId.assert localDecl.userName localDecl.type (mkFVar fvarId)
+        return .newLocal fvarId { goal with mvarId }
+      else
+        return .newLocal fvarId { goal with mvarId }
   else
     return .done
 
-def pushTodo (goal : Goal) : M Unit :=
-  modify fun s => { s with todo := goal :: s.todo }
+def pushResult (goal : Goal) : PreM Unit :=
+  modifyThe Grind.State fun s => { s with goals := s.goals.push goal }
 
-def pushResult (goal : Goal) : M Unit :=
-  modify fun s => { s with goals := s.goals.push goal }
+partial def preprocess (goal : Goal) : PreM Unit := do
+  trace[Meta.debug] "{goal.mvarId}"
+  match (← introNext goal) with
+  | .done =>
+    if let some mvarId ← goal.mvarId.byContra? then
+      preprocess { goal with mvarId }
+    else
+      pushResult goal
+  | .newHyp fvarId goal =>
+    -- TODO: apply eliminators
+    let clause ← goal.mvarId.withContext do mkInputClause fvarId
+    preprocess { goal with clauses := goal.clauses.push clause }
+  | .newLocal _ goal =>
+    -- TODO: apply eliminators
+    preprocess goal
 
-partial def main (mvarId : MVarId) : MetaM Result := do
+end Preprocessor
+
+open Preprocessor
+
+partial def main (mvarId : MVarId) (mainDeclName : Name) : MetaM Grind.State := do
+  mvarId.ensureProp
   mvarId.ensureNoMVar
   let mvarId ← mvarId.revertAll
   mvarId.ensureNoMVar
-  let s ← (loop *> get) |>.run mvarId
-  return { s with }
-where
-  loop : M Unit := do
-    let some goal ← getNextGoal? | return ()
-    trace[Meta.debug] "{goal.mvarId}"
-    match (← introNext goal) with
-    | .closed => loop
-    | .done =>
-      -- TODO: apply `byContradiction`
-      pushResult goal
-      return ()
-    | .newHyp fvarId goal =>
-      -- TODO: apply eliminators
-      let clause ← goal.mvarId.withContext do mkInputClause fvarId
-      pushTodo { goal with clauses := goal.clauses.push clause }
-      loop
-    | .newLocal _ goal =>
-      -- TODO: apply eliminators
-      pushTodo goal
-      loop
+  let mvarId ← mvarId.abstractNestedProofs mainDeclName
+  let mvarId ← mvarId.unfoldReducible
+  let mvarId ← mvarId.betaReduce
+  let s ← (preprocess { mvarId } *> getThe Grind.State) |>.run |>.run mainDeclName
+  return s
 
-end Preprocessor
 end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/Types.lean

@@ -4,10 +4,46 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Lean.Util.ShareCommon
 import Lean.Meta.Basic
+import Lean.Meta.AbstractNestedProofs
+import Lean.Meta.Canonicalizer
 import Lean.Meta.Tactic.Util
 
 namespace Lean.Meta.Grind
+/--
+Stores information for a node in the egraph.
+Each internalized expression `e` has an `ENode` associated with it.
+-/
+structure ENode where
+  /-- Next element in the equivalence class. -/
+  next : Expr
+  /-- Root (aka canonical representative) of the equivalence class -/
+  root : Expr
+  /-- Root of the congruence class. This is field is a don't care if `e` is not an application. -/
+  cgRoot : Expr
+  /--
+  When `e` was added to this equivalence class because of an equality `h : e = target`,
+  then we store `target` here, and `h` at `proof?`.
+  -/
+  target? : Option Expr := none
+  proof? : Option Expr := none
+  /-- Proof has been flipped. -/
+  flipped : Bool := false
+  /-- Number of elements in the equivalence class, this field is meaningless if node is not the root. -/
+  size : Nat := 1
+  /-- `interpreted := true` if node should be viewed as an abstract value. -/
+  interpreted : Bool := false
+  /-- `ctor := true` if the head symbol is a constructor application. -/
+  ctor : Bool := false
+  /-- `hasLambdas := true` if equivalence class contains lambda expressions. -/
+  hasLambdas : Bool := false
+  /--
+  If `heqProofs := true`, then some proofs in the equivalence class are based
+  on heterogeneous equality.
+  -/
+  heqProofs : Bool := false
+  -- TODO: see Lean 3 implementation
 
 structure Clause where
   expr  : Expr
@@ -20,6 +56,8 @@ def mkInputClause (fvarId : FVarId) : MetaM Clause :=
 structure Goal where
   mvarId  : MVarId
   clauses : PArray Clause := {}
+  enodes  : PHashMap UInt64 ENode := {}
+  -- TODO: occurrences for propagation, etc
   deriving Inhabited
 
 def mkGoal (mvarId : MVarId) : Goal :=
@@ -28,4 +66,45 @@ def mkGoal (mvarId : MVarId) : Goal :=
 def Goal.admit (goal : Goal) : MetaM Unit :=
   goal.mvarId.admit
 
+structure Context where
+  mainDeclName : Name
+
+structure State where
+  canon      : Canonicalizer.State := {}
+  /-- `ShareCommon` (aka `Hashconsing`) state. -/
+  scState    : ShareCommon.State.{0} ShareCommon.objectFactory := ShareCommon.State.mk _
+  /-- Next index for creating auxiliary theorems. -/
+  nextThmIdx : Nat := 1
+  goals      : PArray Goal := {}
+
+abbrev GrindM := ReaderT Context $ StateRefT State MetaM
+
+def GrindM.run (x : GrindM α) (mainDeclName : Name) : MetaM α :=
+  x { mainDeclName } |>.run' {}
+
+def abstractNestedProofs (e : Expr) : GrindM Expr := do
+  let nextIdx := (← get).nextThmIdx
+  let (e, s') ← AbstractNestedProofs.visit e |>.run { baseName := (← read).mainDeclName } |>.run |>.run { nextIdx }
+  modify fun s => { s with nextThmIdx := s'.nextIdx }
+  return e
+
+def shareCommon (e : Expr) : GrindM Expr := do
+  modifyGet fun { canon, scState, nextThmIdx, goals } =>
+    let (e, scState) := ShareCommon.State.shareCommon scState e
+    (e, { canon, scState, nextThmIdx, goals })
+
+def canon (e : Expr) : GrindM Expr := do
+  let canonS ← modifyGet fun s => (s.canon, { s with canon := {} })
+  let (e, canonS) ← Canonicalizer.CanonM.run (canonRec e) (s := canonS)
+  modify fun s => { s with canon := canonS }
+  return e
+where
+  canonRec (e : Expr) : CanonM Expr := do
+    let post (e : Expr) : CanonM TransformStep := do
+      if e.isApp then
+        return .done (← Meta.canon e)
+      else
+        return .done e
+    transform e post
+
 end Lean.Meta.Grind

src/Lean/Meta/Tactic/Grind/Util.lean

@@ -0,0 +1,78 @@
+/-
+Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.AbstractNestedProofs
+import Lean.Meta.Tactic.Util
+
+namespace Lean.Meta.Grind
+/--
+Throws an exception if target of the given goal contains metavariables.
+-/
+def _root_.Lean.MVarId.ensureNoMVar (mvarId : MVarId) : MetaM Unit := do
+  let type ← instantiateMVars (← mvarId.getType)
+  if type.hasExprMVar then
+    throwTacticEx `grind mvarId "goal contains metavariables"
+
+/--
+Throws an exception if target is not a proposition.
+-/
+def _root_.Lean.MVarId.ensureProp (mvarId : MVarId) : MetaM Unit := do
+  let type ← mvarId.getType
+  unless (← isProp type) do
+    throwTacticEx `grind mvarId "goal is not a proposition"
+
+def _root_.Lean.MVarId.transformTarget (mvarId : MVarId) (f : Expr → MetaM Expr) : MetaM MVarId := mvarId.withContext do
+  mvarId.checkNotAssigned `grind
+  let tag ← mvarId.getTag
+  let type ← mvarId.getType
+  let typeNew ← f type
+  let mvarNew ← mkFreshExprSyntheticOpaqueMVar typeNew tag
+  mvarId.assign mvarNew
+  return mvarNew.mvarId!
+
+/--
+Unfold all `reducible` declarations occurring in `e`.
+-/
+def unfoldReducible (e : Expr) : MetaM Expr :=
+  let pre (e : Expr) : MetaM TransformStep := do
+    let .const declName _ := e.getAppFn | return .continue
+    unless (← isReducible declName) do return .continue
+    let some v ← unfoldDefinition? e | return .continue
+    return .visit v
+  Core.transform e (pre := pre)
+
+/--
+Unfold all `reducible` declarations occurring in the goal's target.
+-/
+def _root_.Lean.MVarId.unfoldReducible (mvarId : MVarId) : MetaM MVarId :=
+  mvarId.transformTarget Grind.unfoldReducible
+
+/--
+Abstract nested proofs occurring in the goal's target.
+-/
+def _root_.Lean.MVarId.abstractNestedProofs (mvarId : MVarId) (mainDeclName : Name) : MetaM MVarId :=
+  mvarId.transformTarget (Lean.Meta.abstractNestedProofs mainDeclName)
+
+/--
+Beta-reduce the goal's target.
+-/
+def _root_.Lean.MVarId.betaReduce (mvarId : MVarId) : MetaM MVarId :=
+  mvarId.transformTarget (Core.betaReduce ·)
+
+/--
+If the target is not `False`, apply `byContradiction`.
+-/
+def _root_.Lean.MVarId.byContra? (mvarId : MVarId) : MetaM (Option MVarId) := mvarId.withContext do
+  mvarId.checkNotAssigned `grind
+  let target ← mvarId.getType
+  if target.isFalse then return none
+  let targetNew ← mkArrow (mkNot target) (mkConst ``False)
+  let tag ← mvarId.getTag
+  let mvarNew ← mkFreshExprSyntheticOpaqueMVar targetNew tag
+  mvarId.assign <| mkApp2 (mkConst ``Classical.byContradiction) target mvarNew
+  return mvarNew.mvarId!
+
+end Lean.Meta.Grind

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Char.lean

@@ -45,6 +45,11 @@ builtin_dsimproc [simp, seval] reduceVal (Char.val _) := fun e => do
   let_expr Char.val arg ← e | return .continue
   let some c ← fromExpr? arg | return .continue
   return .done <| toExpr c.val
+
+builtin_simproc [simp, seval] reduceLT  (( _ : Char) < _)  := reduceBinPred ``LT.lt 4 (. < .)
+builtin_simproc [simp, seval] reduceLE  (( _ : Char) ≤ _)  := reduceBinPred ``LE.le 4 (. ≤ .)
+builtin_simproc [simp, seval] reduceGT  (( _ : Char) > _)  := reduceBinPred ``GT.gt 4 (. > .)
+builtin_simproc [simp, seval] reduceGE  (( _ : Char) ≥ _)  := reduceBinPred ``GE.ge 4 (. ≥ .)
 builtin_simproc [simp, seval] reduceEq  (( _ : Char) = _)  := reduceBinPred ``Eq 3 (. = .)
 builtin_simproc [simp, seval] reduceNe  (( _ : Char) ≠ _)  := reduceBinPred ``Ne 3 (. ≠ .)
 builtin_dsimproc [simp, seval] reduceBEq  (( _ : Char) == _)  := reduceBoolPred ``BEq.beq 4 (. == .)

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.lean

@@ -32,4 +32,25 @@ builtin_dsimproc [simp, seval] reduceMk (String.mk _) := fun e => do
   unless e.isAppOfArity ``String.mk 1 do return .continue
   reduceListChar e.appArg! ""
 
+@[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : String → String → Bool) (e : Expr) : SimpM Step := do
+  unless e.isAppOfArity declName arity do return .continue
+  let some n ← fromExpr? e.appFn!.appArg! | return .continue
+  let some m ← fromExpr? e.appArg! | return .continue
+  evalPropStep e (op n m)
+
+@[inline] def reduceBoolPred (declName : Name) (arity : Nat) (op : String → String → Bool) (e : Expr) : SimpM DStep := do
+  unless e.isAppOfArity declName arity do return .continue
+  let some n ← fromExpr? e.appFn!.appArg! | return .continue
+  let some m ← fromExpr? e.appArg! | return .continue
+  return .done <| toExpr (op n m)
+
+builtin_simproc [simp, seval] reduceLT  (( _ : String) < _)  := reduceBinPred ``LT.lt 4 (. < .)
+builtin_simproc [simp, seval] reduceLE  (( _ : String) ≤ _)  := reduceBinPred ``LE.le 4 (. ≤ .)
+builtin_simproc [simp, seval] reduceGT  (( _ : String) > _)  := reduceBinPred ``GT.gt 4 (. > .)
+builtin_simproc [simp, seval] reduceGE  (( _ : String) ≥ _)  := reduceBinPred ``GE.ge 4 (. ≥ .)
+builtin_simproc [simp, seval] reduceEq  (( _ : String) = _)  := reduceBinPred ``Eq 3 (. = .)
+builtin_simproc [simp, seval] reduceNe  (( _ : String) ≠ _)  := reduceBinPred ``Ne 3 (. ≠ .)
+builtin_dsimproc [simp, seval] reduceBEq  (( _ : String) == _)  := reduceBoolPred ``BEq.beq 4 (. == .)
+builtin_dsimproc [simp, seval] reduceBNe  (( _ : String) != _)  := reduceBoolPred ``bne 4 (. != .)
+
 end String

src/Lean/Meta/Tactic/Split.lean

@@ -320,10 +320,17 @@ def splitLocalDecl? (mvarId : MVarId) (fvarId : FVarId) : MetaM (Option (List MV
       if e.isIte || e.isDIte then
         return (← splitIfLocalDecl? mvarId fvarId).map fun (mvarId₁, mvarId₂) => [mvarId₁, mvarId₂]
       else
-        let (fvarIds, mvarId) ← mvarId.revert #[fvarId]
-        let num := fvarIds.size
+        let mut mvarId := mvarId
+        let localDecl ← fvarId.getDecl
+        if (← pure localDecl.isLet <||> exprDependsOn (← mvarId.getType) fvarId <||> fvarId.hasForwardDeps) then
+          -- If `fvarId` has dependencies or is a let-decl, we create a copy.
+          mvarId ← mvarId.assert localDecl.userName localDecl.type localDecl.toExpr
+        else
+          let (fvarIds, mvarId') ← mvarId.revert #[fvarId]
+          assert! fvarIds.size == 1 -- fvarId does not have forward dependencies
+          mvarId := mvarId'
         let mvarIds ← splitMatch mvarId e
-        let mvarIds ← mvarIds.mapM fun mvarId => return (← mvarId.introNP num).2
+        let mvarIds ← mvarIds.mapM fun mvarId => return (← mvarId.intro1P).2
         return some mvarIds
     else
       return none

src/Lean/MetavarContext.lean

@@ -360,8 +360,11 @@ def MetavarContext.getExprAssignmentCore? (m : MetavarContext) (mvarId : MVarId)
 def getExprMVarAssignment? [Monad m] [MonadMCtx m] (mvarId : MVarId) : m (Option Expr) :=
   return (← getMCtx).getExprAssignmentCore? mvarId
 
+def MetavarContext.getDelayedMVarAssignmentCore? (mctx : MetavarContext) (mvarId : MVarId) : Option DelayedMetavarAssignment :=
+  mctx.dAssignment.find? mvarId
+
 def getDelayedMVarAssignment? [Monad m] [MonadMCtx m] (mvarId : MVarId) : m (Option DelayedMetavarAssignment) :=
-  return (← getMCtx).dAssignment.find? mvarId
+  return (← getMCtx).getDelayedMVarAssignmentCore? mvarId
 
 /-- Given a sequence of delayed assignments
    ```

src/Lean/PrettyPrinter.lean

@@ -110,16 +110,14 @@ namespace MessageData
 open Lean PrettyPrinter Delaborator
 
 /--
-Turns a `MetaM FormatWithInfos` into a `MessageData` using `.ofPPFormat` and running the monadic value in the given context.
-Uses the `pp.tagAppFns` option to annotate constants with terminfo, which is necessary for seeing the type on mouse hover.
+Turns a `MetaM FormatWithInfos` into a `MessageData.lazy` which will run the monadic value.
+Uses the `pp.tagAppFns` option to annotate constants with terminfo,
+which is necessary for seeing the type on mouse hover.
 -/
-def ofFormatWithInfos
-    (fmt : MetaM FormatWithInfos)
-    (noContext : Unit → Format := fun _ => "<no context, could not generate MessageData>") : MessageData :=
-  .ofPPFormat
-  { pp := fun
-      | some ctx => ctx.runMetaM <| withOptions (pp.tagAppFns.set · true) fmt
-      | none => return noContext () }
+def ofFormatWithInfosM (fmt : MetaM FormatWithInfos) : MessageData :=
+  .lazy fun ctx => ctx.runMetaM <|
+    withOptions (pp.tagAppFns.set · true) <|
+      .ofFormatWithInfos <$> fmt
 
 /-- Pretty print a const expression using `delabConst` and generate terminfo.
 This function avoids inserting `@` if the constant is for a function whose first
@@ -127,13 +125,13 @@ argument is implicit, which is what the default `toMessageData` for `Expr` does.
 Panics if `e` is not a constant. -/
 def ofConst (e : Expr) : MessageData :=
   if e.isConst then
-    .ofFormatWithInfos (PrettyPrinter.ppExprWithInfos (delab := delabConst) e) fun _ => f!"{e}"
+    .ofFormatWithInfosM (PrettyPrinter.ppExprWithInfos (delab := delabConst) e)
   else
     panic! "not a constant"
 
 /-- Generates `MessageData` for a declaration `c` as `c.{<levels>} <params> : <type>`, with terminfo. -/
 def signature (c : Name) : MessageData :=
-  .ofFormatWithInfos (PrettyPrinter.ppSignature c) fun _ => f!"{c}"
+  .ofFormatWithInfosM (PrettyPrinter.ppSignature c)
 
 end MessageData
 

src/Lean/Util/PPExt.lean

@@ -40,6 +40,10 @@ structure PPContext where
   openDecls     : List OpenDecl := []
 
 abbrev PrettyPrinter.InfoPerPos := RBMap Nat Elab.Info compare
+/-- A format tree with `Elab.Info` annotations.
+Each `.tag n _` node is annotated with `infos[n]`.
+This is used to attach semantic data such as expressions
+to pretty-printer outputs. -/
 structure FormatWithInfos where
   fmt : Format
   infos : PrettyPrinter.InfoPerPos

src/Lean/Widget/InteractiveDiagnostic.lean

@@ -128,10 +128,8 @@ where
   }
 
   go (nCtx : NamingContext) : Option MessageDataContext → MessageData → MsgFmtM Format
-  | _,         ofFormat fmt             => withIgnoreTags fmt
-  | none,      ofPPFormat fmt           => (·.fmt) <$> fmt.pp none
-  | some ctx,  ofPPFormat fmt           => do
-    let ⟨fmt, infos⟩ ← fmt.pp (mkPPContext nCtx ctx)
+  | none,      ofFormatWithInfos ⟨fmt, _⟩ => withIgnoreTags fmt
+  | some ctx,  ofFormatWithInfos ⟨fmt, infos⟩ => do
     let t ← pushEmbed <| EmbedFmt.code (mkContextInfo nCtx ctx) infos
     return Format.tag t fmt
   | none,      ofGoal mvarId            => pure $ "goal " ++ format (mkMVar mvarId)
@@ -162,6 +160,11 @@ where
         pure (.strict (← children.mapM (go nCtx ctx)))
     let e := .trace data.cls header data.collapsed nodes
     return .tag (← pushEmbed e) ".\n"
+  | ctx?,     ofLazy f _          => do
+    let dyn ← f (ctx?.map (mkPPContext nCtx))
+    let some msg := dyn.get? MessageData
+      | throw <| IO.userError "MessageData.ofLazy: expected MessageData in Dynamic"
+    go nCtx ctx? msg
 
   /-- Recursively moves child nodes after the first `blockSize` into a new "more" node. -/
   chopUpChildren (cls : Name) (blockSize : Nat) (children : Subarray MessageData) :

src/lake/Lake/Build/Actions.lean

@@ -115,7 +115,7 @@ def download  (url : String) (file : FilePath) : LogIO PUnit := do
     createParentDirs file
   proc (quiet := true) {
     cmd := "curl"
-    args := #["-f", "-o", file.toString, "-L", url]
+    args := #["-s", "-S", "-f", "-o", file.toString, "-L", url]
   }
 
 /-- Unpack an archive `file` using `tar` into the directory `dir`. -/

src/lake/Lake/Build/Common.lean

@@ -71,8 +71,9 @@ of the `traceFile`. If rebuilt, save the new `depTrace` to the `tracefile`.
 @[inline] def buildUnlessUpToDate
   [CheckExists ι] [GetMTime ι] (info : ι)
   (depTrace : BuildTrace) (traceFile : FilePath) (build : JobM PUnit)
+  (action : JobAction := .build) (oldTrace := depTrace)
 : JobM PUnit := do
-  discard <| buildUnlessUpToDate? info depTrace traceFile build
+  discard <| buildUnlessUpToDate? info depTrace traceFile build action oldTrace
 
 /-- Fetch the trace of a file that may have its hash already cached in a `.hash` file. -/
 def fetchFileTrace (file : FilePath) : JobM BuildTrace := do

src/lake/Lake/Build/Package.lean

@@ -35,10 +35,12 @@ def Package.recBuildExtraDepTargets (self : Package) : FetchM (BuildJob Unit) :=
     job := job.mix <| ← dep.extraDep.fetch
   -- Fetch pre-built release if desired and this package is a dependency
   if self.name ≠ (← getWorkspace).root.name ∧ self.preferReleaseBuild then
-    job := job.add <| ← (← self.optRelease.fetch).bindSync fun success t => do
-      unless success do
-        logWarning "failed to fetch cloud release; falling back to local build"
-      return ((), t)
+    job := job.add <| ←
+      withRegisterJob s!"{self.name}:optRelease" do
+        (← self.optRelease.fetch).bindSync fun success t => do
+          unless success do
+            logWarning "failed to fetch cloud release; falling back to local build"
+          return ((), t)
   -- Build this package's extra dep targets
   for target in self.extraDepTargets do
     job := job.mix <| ← self.fetchTargetJob target
@@ -50,26 +52,26 @@ def Package.extraDepFacetConfig : PackageFacetConfig extraDepFacet :=
 
 /-- Download and unpack the package's prebuilt release archive (from GitHub). -/
 def Package.fetchOptRelease (self : Package) : FetchM (BuildJob Bool) := Job.async do
-  updateAction .fetch
   let repo := GitRepo.mk self.dir
   let repoUrl? := self.releaseRepo? <|> self.remoteUrl?
   let some repoUrl := repoUrl? <|> (← repo.getFilteredRemoteUrl?)
     | logInfo s!"{self.name}: wanted prebuilt release, \
-        but package's repository URL was not known; it may need to set 'releaseRepo'"
+        but repository URL not known; the package may need to set 'releaseRepo'"
+      updateAction .fetch
       return (false, .nil)
   let some tag ← repo.findTag?
-    | logInfo s!"{self.name}: wanted prebuilt release, \
-        but could not find an associated tag for the package's revision"
+    | logInfo s!"{self.name}: wanted prebuilt release, but no tag found for revision"
+      updateAction .fetch
       return (false, .nil)
   let url := s!"{repoUrl}/releases/download/{tag}/{self.buildArchive}"
-  let logName := s!"{self.name}/{tag}/{self.buildArchive}"
   let depTrace := Hash.ofString url
   let traceFile := FilePath.mk <| self.buildArchiveFile.toString ++ ".trace"
   let upToDate ← buildUnlessUpToDate? (action := .fetch) self.buildArchiveFile depTrace traceFile do
-    logVerbose s!"downloading {logName}"
+    logVerbose s!"downloading {url}"
     download url self.buildArchiveFile
   unless upToDate && (← self.buildDir.pathExists) do
-    logVerbose s!"unpacking {logName}"
+    updateAction .fetch
+    logVerbose s!"unpacking {self.name}/{tag}/{self.buildArchive}"
     untar self.buildArchiveFile self.buildDir
   return (true, .nil)
 

src/lake/Lake/Build/Run.lean

@@ -31,8 +31,9 @@ structure MonitorContext where
   out : IO.FS.Stream
   outLv : LogLevel
   failLv : LogLevel
-  showProgress : Bool
+  minAction : JobAction
   useAnsi : Bool
+  showProgress : Bool
   /-- How often to poll jobs (in milliseconds). -/
   updateFrequency : Nat := 100
 
@@ -83,19 +84,19 @@ def renderProgress : MonitorM PUnit := do
     if h : 0 < jobs.size then
       let caption := jobs[0]'h |>.caption
       let resetCtrl ← modifyGet fun s => (s.resetCtrl, {s with resetCtrl := Ansi.resetLine})
-      print s!"{resetCtrl}[{jobNo}/{totalJobs}] Checking {caption}"
+      print s!"{resetCtrl}[{jobNo}/{totalJobs}] Running {caption}"
       flush
 
 def reportJob (job : Job Unit) : MonitorM PUnit := do
   let {jobNo, ..} ← get
-  let {totalJobs, failLv, outLv, out, useAnsi, showProgress, ..} ← read
+  let {totalJobs, failLv, outLv, out, useAnsi, showProgress, minAction, ..} ← read
   let {log, action, ..} := job.task.get.state
   let maxLv := log.maxLv
   let failed := log.hasEntries ∧ maxLv ≥ failLv
   if failed then
     modify fun s => {s with failures := s.failures.push job.caption}
   let hasOutput := failed ∨ (log.hasEntries ∧ maxLv ≥ outLv)
-  if hasOutput ∨ (showProgress ∧ action ≥ .fetch) then
+  if hasOutput ∨ (showProgress ∧ (action ≥ minAction)) then
     let verb := action.verb failed
     let icon := if hasOutput then maxLv.icon else '✔'
     let caption := s!"{icon} [{jobNo}/{totalJobs}] {verb} {job.caption}"
@@ -151,6 +152,7 @@ def monitorJobs
   (jobs : Array (Job Unit))
   (out : IO.FS.Stream)
   (failLv outLv : LogLevel)
+  (minAction : JobAction)
   (useAnsi showProgress : Bool)
   (resetCtrl : String := "")
   (initFailures : Array String := #[])
@@ -158,7 +160,7 @@ def monitorJobs
   (updateFrequency := 100)
 : BaseIO (Array String) := do
   let ctx := {
-    totalJobs, out, failLv, outLv,
+    totalJobs, out, failLv, outLv, minAction
     useAnsi, showProgress, updateFrequency
   }
   let s := {
@@ -211,7 +213,8 @@ def Workspace.runFetchM
   -- Job Monitor
   let jobs ← ctx.registeredJobs.get
   let resetCtrl := if showAnsiProgress then Ansi.resetLine else ""
-  let failures ← monitorJobs jobs out failLv outLv useAnsi showProgress
+  let minAction := if cfg.verbosity = .verbose then .unknown else .fetch
+  let failures ← monitorJobs jobs out failLv outLv minAction useAnsi showProgress
     (resetCtrl := resetCtrl) (initFailures := failures)
   -- Failure Report
   if failures.isEmpty then

src/lake/Lake/CLI/Init.lean

@@ -148,6 +148,8 @@ git = \"https://github.com/leanprover-community/mathlib4.git\"
 name = {repr libRoot}
 "
 
+def readmeFileContents (pkgName : String) := s!"# {pkgName}"
+
 def mathToolchainUrl : String :=
   "https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain"
 
@@ -267,6 +269,11 @@ def initPkg (dir : FilePath) (name : String) (tmp : InitTemplate) (lang : Config
     else
       logWarning "failed to initialize git repository"
 
+  -- Initialize a README.md file if none exists.
+  let readmeFile := dir / "README.md"
+  unless (← readmeFile.pathExists) do
+    IO.FS.writeFile readmeFile (readmeFileContents name)
+
 def validatePkgName (pkgName : String) : LogIO PUnit := do
   if pkgName.isEmpty || pkgName.all (· == '.') || pkgName.any (· ∈ ['/', '\\']) then
     error s!"illegal package name '{pkgName}'"

src/lake/tests/noRelease/clean.sh

@@ -1 +1 @@
-rm -rf .lake lake-manifest.json
+rm -rf .lake lake-manifest.json dep/.lake dep/.git

src/lake/tests/noRelease/dep/lakefile.lean

@@ -4,3 +4,4 @@ open Lake DSL
 package dep where
   preferReleaseBuild := true
   releaseRepo := "https://example.com"
+  buildArchive := "release.tgz"

src/lake/tests/noRelease/lakefile.lean

@@ -3,3 +3,5 @@ open Lake DSL
 
 package test
 require dep from "dep"
+
+lean_lib Test

src/lake/tests/noRelease/test.sh

@@ -12,7 +12,7 @@ LAKE=${LAKE:-../../.lake/build/bin/lake}
 # Test that a direct invocation fo `lake build *:release` fails
 ($LAKE build dep:release && exit 1 || true) | diff -u --strip-trailing-cr <(cat << 'EOF'
 ✖ [1/1] Fetching dep:release
-info: dep: wanted prebuilt release, but could not find an associated tag for the package's revision
+info: dep: wanted prebuilt release, but no tag found for revision
 error: failed to fetch cloud release
 Some builds logged failures:
 - dep:release
@@ -20,10 +20,50 @@ EOF
 ) -
 
 # Test that an indirect fetch on the release does not cause the build to fail
-$LAKE build -v test:extraDep | diff -u --strip-trailing-cr <(cat << 'EOF'
-⚠ [1/1] Fetched test:extraDep
-info: dep: wanted prebuilt release, but could not find an associated tag for the package's revision
+$LAKE build Test | diff -u --strip-trailing-cr <(cat << 'EOF'
+⚠ [1/3] Fetched dep:optRelease
+info: dep: wanted prebuilt release, but no tag found for revision
 warning: failed to fetch cloud release; falling back to local build
+✔ [2/3] Built Test
 Build completed successfully.
 EOF
 ) -
+
+# Since committing a Git repository to a Git repository is not well-supported,
+# We reinitialize the bar repository on each test. This requires updating the
+# locked manifest to the new hash to ensure things work properly.
+pushd dep
+git init
+git checkout -b master
+git config user.name test
+git config user.email test@example.com
+git add --all
+git commit -m "initial commit"
+git tag release
+popd
+
+# Test download failure
+($LAKE build dep:release && exit 1 || true) | grep --color "downloading"
+
+# Test unpacking
+mkdir -p dep/.lake/build
+tar -cz -f dep/.lake/release.tgz -C dep/.lake/build .
+echo 4225503363911572621 > dep/.lake/release.tgz.trace
+rmdir dep/.lake/build
+$LAKE build dep:release -v | grep --color "unpacking"
+test -d dep/.lake/build
+
+# Test that the job prints nothing if the archive is already fetched and unpacked
+$LAKE build dep:release | diff -u --strip-trailing-cr <(cat << 'EOF'
+Build completed successfully.
+EOF
+) -
+
+# Test that releases do not contaminate downstream jobs
+$LAKE build Test | diff -u --strip-trailing-cr <(cat << 'EOF'
+Build completed successfully.
+EOF
+) -
+
+# Cleanup git repo
+rm -rf dep/.git