chore: for #8914 after stage0 update, part 2 (#8931)

This PR finishes post-stage0-cleanup after #8914 and #8929. Also:
- adds configuration options for `haveI` and `letI` terms.
- adds `letConfig` parser alias

src/Lean/Elab/Binders.lean

@@ -856,11 +856,12 @@ def expandLetEqnsDecl (letDecl : Syntax) (useExplicit := true) : MacroM Syntax :
   return mkNode `Lean.Parser.Term.letIdDecl #[letDecl[0], letDecl[1], letDecl[2], mkAtomFrom ref " := ", val]
 
 def elabLetDeclCore (stx : Syntax) (expectedType? : Option Expr) (initConfig : LetConfig) : TermElabM Expr := do
-  let declIdx := stx.getNumArgs - 3
-  let letConfig := stx[1]
-  let config    ← mkLetConfig letConfig initConfig
+  let (config, declIdx) ← if stx[1].isOfKind ``Parser.Term.letConfig then
+    pure (← mkLetConfig stx[1] initConfig, 2)
+  else
+    pure (initConfig, 1)
   let letDecl   := stx[declIdx][0]
-  let body      := stx[stx.getNumArgs - 1]
+  let body      := stx[declIdx + 2]
   if letDecl.getKind == ``Lean.Parser.Term.letIdDecl then
     let { id, binders, type, value } := mkLetIdDeclView letDecl
     let id ← if id.isIdent then pure id else mkFreshIdent id (canonical := true)

src/Lean/Elab/BuiltinNotation.lean

@@ -117,7 +117,7 @@ open Meta
     ```
     -/
     let thisId := mkIdentFrom stx `this
-    let valNew ← `(let_fun $thisId:ident : $(← exprToSyntax type) := $val; $thisId)
+    let valNew ← `(have $thisId:ident : $(← exprToSyntax type) := $val; $thisId)
     elabTerm valNew expectedType?
   | _ => throwUnsupportedSyntax
 

src/Lean/Elab/Do.lean

@@ -651,10 +651,7 @@ def concat (terminal : CodeBlock) (kRef : Syntax) (y? : Option Var) (k : CodeBlo
 def getLetIdVars (letId : Syntax) : Array Var :=
   assert! letId.isOfKind ``Parser.Term.letId
   -- def letId := leading_parser binderIdent <|> hygieneInfo
-  if letId.isIdent then
-    -- TODO(kmill): Remove this case after stage0 update
-    #[letId]
-  else if letId[0].isIdent then
+  if letId[0].isIdent then
     #[letId[0]]
   else if letId[0].isOfKind hygieneInfoKind then
     #[HygieneInfo.mkIdent letId[0] `this (canonical := true)]
@@ -1084,22 +1081,12 @@ def declToTerm (decl : Syntax) (k : Syntax) : M Syntax := withRef decl <| withFr
     Macro.throwErrorAt decl "unexpected kind of `do` declaration"
 
 def reassignToTerm (reassign : Syntax) (k : Syntax) : MacroM Syntax := withRef reassign <| withFreshMacroScope do
-  -- TODO(kmill) Restore after stage0 update
-    if reassign.isOfKind ``Parser.Term.doReassign then
-      if reassign[0].isOfKind ``Parser.Term.letIdDecl then
-        let letId := reassign[0][0]
-        let x := if letId.isIdent then letId else letId[0]
-        if x.isIdent then
-          let rhs := reassign[0][4]
-          return ← `(let $x:ident := ensure_type_of% $x $(quote "invalid reassignment, value") $rhs; $k)
-      if let `(doElem| $e:term := $rhs) := reassign then
-        return ← `(let $e:term  := ensure_type_of% $e $(quote "invalid reassignment, value") $rhs; $k)
-  -- match reassign with
-  -- | `(doElem| $x:ident := $rhs) => `(let $x:ident := ensure_type_of% $x $(quote "invalid reassignment, value") $rhs; $k)
-  -- | `(doElem| $e:term  := $rhs) => `(let $e:term  := ensure_type_of% $e $(quote "invalid reassignment, value") $rhs; $k)
-  -- | _ =>
+  match reassign with
+  | `(doElem| $x:ident := $rhs) => `(let $x:ident := ensure_type_of% $x $(quote "invalid reassignment, value") $rhs; $k)
+  | `(doElem| $e:term  := $rhs) => `(let $e:term  := ensure_type_of% $e $(quote "invalid reassignment, value") $rhs; $k)
+  | _ =>
     -- Note that `doReassignArrow` is expanded by `doReassignArrowToCode
-    Macro.throwErrorAt reassign s!"unexpected kind of `do` reassignment {reassign}"
+    Macro.throwErrorAt reassign "unexpected kind of `do` reassignment"
 
 def mkIte (optIdent : Syntax) (cond : Syntax) (thenBranch : Syntax) (elseBranch : Syntax) : MacroM Syntax := do
   if optIdent.isNone then

src/Lean/Parser/Term.lean

@@ -650,7 +650,7 @@ def letNegOpt := leading_parser (withAnonymousAntiquot := false)
 @[builtin_doc] def letOptEq := leading_parser (withAnonymousAntiquot := false)
   atomic (" (" >> nonReservedSymbol "eq" >> " := ") >> binderIdent >> ")"
 def letConfigItem := letPosOpt <|> letNegOpt <|> letOptEq
-/-- Configuration options for tactics. -/
+/-- Configuration options for `let` tactics. -/
 def letConfig := leading_parser (withAnonymousAntiquot := false)
   many letConfigItem
 /--
@@ -704,12 +704,12 @@ It is often used when building macros.
 -/
 @[builtin_term_parser] def «let_tmp» := leading_parser:leadPrec
   withPosition ("let_tmp " >> letDecl) >> optSemicolon termParser
-/-- `haveI` behaves like `have`, but inlines the value instead of producing a `let_fun` term. -/
+/-- `haveI` behaves like `have`, but inlines the value instead of producing a `have` term. -/
 @[builtin_term_parser] def «haveI» := leading_parser
-  withPosition ("haveI " >> letDecl) >> optSemicolon termParser
-/-- `letI` behaves like `let`, but inlines the value instead of producing a `let_fun` term. -/
+  withPosition ("haveI " >> letConfig >> letDecl) >> optSemicolon termParser
+/-- `letI` behaves like `let`, but inlines the value instead of producing a `let` term. -/
 @[builtin_term_parser] def «letI» := leading_parser
-  withPosition ("letI " >> letDecl) >> optSemicolon termParser
+  withPosition ("letI " >> letConfig >> letDecl) >> optSemicolon termParser
 
 def «scoped» := leading_parser "scoped "
 def «local»  := leading_parser "local "
@@ -1196,6 +1196,7 @@ end Term
 open Term in
 builtin_initialize
   register_parser_alias letDecl
+  register_parser_alias letConfig
   register_parser_alias sufficesDecl
   register_parser_alias letRecDecls
   register_parser_alias hole

tests/lean/noTabs.lean

@@ -1,4 +1,3 @@
-#guard_msgs (drop error) in -- TODO(kmill) remove #guard_msgs after stage0 update
 #check
   let a := 1
 	let b := 2

tests/lean/noTabs.lean.expected.out

@@ -1 +1,3 @@
-noTabs.lean:4:0: error: tabs are not allowed; please configure your editor to expand them
+noTabs.lean:3:0: error: tabs are not allowed; please configure your editor to expand them
+let a := 1;
+sorry : ?m

tests/lean/unknownTactic.lean.expected.out

@@ -5,5 +5,11 @@ a✝ : x = x
 ⊢ x = x
 ---
 unknownTactic.lean:8:22: error: unknown tactic
+unknownTactic.lean:8:18-8:24: error: unsolved goals
+x : Nat
+⊢ x = x
 ---
 unknownTactic.lean:14:22: error: unknown tactic
+unknownTactic.lean:14:18-14:24: error: unsolved goals
+x : Nat
+⊢ x = x