chore: use string gaps (#9193)

For error messages that span multiple lines, now we can use the new "string gap" escape sequence (a `\` at the end of the line, which causes all the whitespace at the beginning of the next line ignored), rather than using append operations or hacks involving `{` and `}` for `s!` and `m!` strings.

Style-wise, we suggest for long messages that the body of the message start on the next line if possible, by starting the message with a string gap sequence. This eliminates needing to decide whether to indent continuing lines at the `"` or at the next column. For example:
```lean
    logError m!"\
      Tactic 'more_magic' cannot \
      apply expression{indentD e}\n\
      due to some reason or another."
```
Note that to get whitespace to appear between one line and the next, you include it before the `\`.

Cache/Requests.lean

@@ -47,8 +47,8 @@ def mkGetConfigContent (hashMap : IO.HashMap) : IO String := do
 
     -- Note we append a '.part' to the filenames here,
     -- which `downloadFiles` then removes when the download is successful.
-    pure $ acc ++ s!"url = {← mkFileURL fileName none}\n-o {
-      (IO.CACHEDIR / (fileName ++ ".part")).toString.quote}\n"
+    pure $ acc ++ s!"url = {← mkFileURL fileName none}\n\
+      -o {(IO.CACHEDIR / (fileName ++ ".part")).toString.quote}\n"
 
 /-- Calls `curl` to download a single file from the server to `CACHEDIR` (`.cache`) -/
 def downloadFile (hash : UInt64) : IO Bool := do

ImportGraph/Main.lean

@@ -78,9 +78,9 @@ def importGraphCLI (args : Cli.Parsed) : IO UInt32 := do
 /-- Setting up command line options and help text for `lake exe graph`. -/
 def graph : Cmd := `[Cli|
   graph VIA importGraphCLI; ["0.0.1"]
-  "Generate representations of a Lean import graph." ++
-  "By default generates the import graph up to `Mathlib`." ++
-  "If you are working in a downstream project, use `lake exe graph --to MyProject`."
+  "Generate representations of a Lean import graph. \
+   By default generates the import graph up to `Mathlib`. \
+   If you are working in a downstream project, use `lake exe graph --to MyProject`."
 
   FLAGS:
     reduce;               "Remove transitively redundant edges."
@@ -90,11 +90,11 @@ def graph : Cmd := `[Cli|
     "include-deps";       "Include used files from other projects (e.g. lake packages)"
 
   ARGS:
-    ...outputs : String;  "Filename(s) for the output. " ++
-      "If none are specified, generates `import_graph.dot`. " ++
-      "Automatically chooses the format based on the file extension. " ++
-      "Currently `.dot` is supported, " ++
-      "and if you have `graphviz` installed then any supported output format is allowed."
+    ...outputs : String;  "Filename(s) for the output. \
+      If none are specified, generates `import_graph.dot`. \
+      Automatically chooses the format based on the file extension. \
+      Currently `.dot` is supported, \
+      and if you have `graphviz` installed then any supported output format is allowed."
 ]
 
 /-- `lake exe graph` -/

Mathlib/Data/Matrix/Notation.lean

@@ -103,9 +103,9 @@ macro_rules
     let n := if h : 0 < m then rows[0].size else 0
     let rowVecs ← rows.mapM fun row : Array Term => do
       unless row.size = n do
-        Macro.throwErrorAt (mkNullNode row)
-          s!"Rows must be of equal length; this row has {row.size} items, the previous rows {"
-          "}have {n}"
+        Macro.throwErrorAt (mkNullNode row) s!"\
+          Rows must be of equal length; this row has {row.size} items, \
+          the previous rows have {n}"
       `(![$row,*])
     `(@Matrix.of (Fin $(quote m)) (Fin $(quote n)) _ ![$rowVecs,*])
   | `(!![$[;%$semicolons]*]) => do

Mathlib/Data/PNat/Xgcd.lean

@@ -70,9 +70,9 @@ instance : SizeOf XgcdType :=
  reflects the matrix/vector interpretation as above. -/
 instance : Repr XgcdType where
   reprPrec
-  | g, _ => s!"[[[ {repr (g.wp + 1)}, {(repr g.x)} ], [" ++
-            s!"{repr g.y}, {repr (g.zp + 1)}]], [" ++
-            s!"{repr (g.ap + 1)}, {repr (g.bp + 1)}]]"
+  | g, _ => s!"[[[{repr (g.wp + 1)}, {repr g.x}], \
+                 [{repr g.y}, {repr (g.zp + 1)}]], \
+                [{repr (g.ap + 1)}, {repr (g.bp + 1)}]]"
 
 /-- Another `mk` using ℕ and ℕ+ -/
 def mk' (w : ℕ+) (x : ℕ) (y : ℕ) (z : ℕ+) (a : ℕ+) (b : ℕ+) : XgcdType :=

Mathlib/Lean/Expr/Basic.lean

@@ -422,8 +422,8 @@ def reduceProjStruct? (e : Expr) : MetaM (Option Expr) := do
     if hs : sidx < sfields.size then
       return some (sfields[sidx]'hs)
     else
-      throwError m!"ill-formed expression, {cname} is the {pinfo.i + 1}-th projection function {
-          ""}but {sarg} does not have enough arguments"
+      throwError m!"ill-formed expression, {cname} is the {pinfo.i + 1}-th projection function \
+        but {sarg} does not have enough arguments"
   else
     return none
 

Mathlib/Mathport/Notation.lean

@@ -590,13 +590,14 @@ elab (name := notation3) doc:(docComment)? attrs?:(Parser.Term.attributes)? attr
         elabCommand <|
           ← `(command| attribute [$attrKind delab $(mkIdent key)] $(Lean.mkIdent delabName))
     else
-      logWarning s!"Was not able to generate a pretty printer for this notation.{
-        ""} If you do not expect it to be pretty printable, then you can use{
-        ""} `notation3 (prettyPrint := false)`.{
-        ""} If the notation expansion refers to section variables, be sure to do `local notation3`.{
-        ""} Otherwise, you might be able to adjust the notation expansion to make it matchable;{
-        ""} pretty printing relies on deriving an expression matcher from the expansion.{
-        ""} (Use `set_option trace.notation3 true` to get some debug information.)"
+      logWarning s!"\
+        Was not able to generate a pretty printer for this notation. \
+        If you do not expect it to be pretty printable, then you can use \
+        `notation3 (prettyPrint := false)`. \
+        If the notation expansion refers to section variables, be sure to do `local notation3`. \
+        Otherwise, you might be able to adjust the notation expansion to make it matchable; \
+        pretty printing relies on deriving an expression matcher from the expansion. \
+        (Use `set_option trace.notation3 true` to get some debug information.)"
 
 initialize Std.Linter.UnreachableTactic.addIgnoreTacticKind ``«notation3»
 

Mathlib/Mathport/Rename.lean

@@ -160,17 +160,17 @@ def suspiciousLean3Name (s : String) : Bool := Id.run do
         let note := "(add `set_option align.precheck false` to suppress this message)"
         let inner := match ← try some <$> resolveGlobalConstWithInfos id4 catch _ => pure none with
         | none => m!""
-        | some cs => m!" Did you mean:\n\n{
-            ("\n":MessageData).joinSep (cs.map fun c' => m!"  #align {id3} {c'}")
-          }\n\n#align inputs have to be fully qualified.{""
-          } (Double check the lean 3 name too, we can't check that!)"
+        | some cs => m!" Did you mean:\n\n\
+              {("\n":MessageData).joinSep (cs.map fun c' => m!"  #align {id3} {c'}")}\n\n\
+            #align inputs have to be fully qualified. \
+            (Double check the lean 3 name too, we can't check that!)"
         throwErrorAt id4 "Declaration {c} not found.{inner}\n{note}"
       if Linter.getLinterValue linter.uppercaseLean3 (← getOptions) then
         if id3.getId.anyS suspiciousLean3Name then
-          Linter.logLint linter.uppercaseLean3 id3 $
-            "Lean 3 names are usually lowercase. This might be a typo.\n" ++
-            "If the Lean 3 name is correct, then above this line, add:\n" ++
-            "set_option linter.uppercaseLean3 false in\n"
+          Linter.logLint linter.uppercaseLean3 id3
+            "Lean 3 names are usually lowercase. This might be a typo.\n\
+             If the Lean 3 name is correct, then above this line, add:\n\
+             set_option linter.uppercaseLean3 false in\n"
     withRef id3 <| ensureUnused id3.getId
     liftCoreM <| addNameAlignment id3.getId id4.getId
   | _ => throwUnsupportedSyntax

Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

@@ -243,11 +243,11 @@ def borelToRefl (e : Expr) (i : FVarId) : TacticM Unit := do
     liftMetaTactic fun m => return [← subst m i]
   catch _ =>
     let et ← synthInstance (← mkAppOptM ``TopologicalSpace #[e])
-    throwError
-      (m!"`‹TopologicalSpace {e}› := {et}" ++ MessageData.ofFormat Format.line ++
-        m!"depends on" ++ MessageData.ofFormat Format.line ++
-        m!"{Expr.fvar i} : MeasurableSpace {e}`" ++ MessageData.ofFormat Format.line ++
-        "so `borelize` isn't avaliable")
+    throwError m!"\
+      `‹TopologicalSpace {e}› := {et}\n\
+      depends on\n\
+      {Expr.fvar i} : MeasurableSpace {e}`\n\
+      so `borelize` isn't avaliable"
   evalTactic <| ← `(tactic|
     refine_lift
       letI : MeasurableSpace $te := borel $te

Mathlib/Tactic/Cases.lean

@@ -75,11 +75,11 @@ elab (name := induction') "induction' " tgts:(Parser.Tactic.casesTarget,+)
       let mut s ← getFVarSetToGeneralize targets forbidden
       for v in genArgs do
         if forbidden.contains v then
-          throwError "variable cannot be generalized {""
-            }because target depends on it{indentExpr (mkFVar v)}"
+          throwError "variable cannot be generalized \
+            because target depends on it{indentExpr (mkFVar v)}"
         if s.contains v then
-          throwError "unnecessary 'generalizing' argument, {""
-            }variable '{mkFVar v}' is generalized automatically"
+          throwError "unnecessary 'generalizing' argument, \
+            variable '{mkFVar v}' is generalized automatically"
         s := s.insert v
       let (fvarIds, g) ← g.revert (← sortFVarIds s.toArray)
       g.withContext do

Mathlib/Tactic/CategoryTheory/Coherence.lean

@@ -329,8 +329,8 @@ def coherence_loop (maxSteps := 37) : TacticM Unit :=
     -- Otherwise, rearrange so we have a maximal prefix of each side
     -- that is built out of unitors and associators:
     evalTactic (← `(tactic| liftable_prefixes)) <|>
-      exception' ("Something went wrong in the `coherence` tactic: " ++
-        "is the target an equation in a monoidal category?")
+      exception' "Something went wrong in the `coherence` tactic: \
+        is the target an equation in a monoidal category?"
     -- The goal should now look like `f₀ ≫ f₁ = g₀ ≫ g₁`,
     liftMetaTactic MVarId.congrCore
     -- and now we have two goals `f₀ = g₀` and `f₁ = g₁`.

Mathlib/Tactic/CategoryTheory/Elementwise.lean

@@ -84,19 +84,19 @@ def elementwiseExpr (src : Name) (type pf : Expr) (simpSides := true) :
       -- First simplify using elementwise-specific lemmas
       let mut eqPf' ← simpType (simpOnlyNames elementwiseThms (config := { decide := false })) eqPf
       if (← inferType eqPf') == .const ``True [] then
-        throwError "elementwise lemma for {src} is trivial after applying ConcreteCategory {""
-          }lemmas, which can be caused by how applications are unfolded. {""
-          }Using elementwise is unnecessary."
+        throwError "elementwise lemma for {src} is trivial after applying ConcreteCategory \
+          lemmas, which can be caused by how applications are unfolded. \
+          Using elementwise is unnecessary."
       if simpSides then
         let ctx := { ← Simp.Context.mkDefault with config.decide := false }
         let (ty', eqPf'') ← simpEq (fun e => return (← simp e ctx).1) (← inferType eqPf') eqPf'
         -- check that it's not a simp-trivial equality:
         forallTelescope ty' fun _ ty' => do
           if let some (_, lhs, rhs) := ty'.eq? then
             if ← Std.Tactic.Lint.isSimpEq lhs rhs then
-              throwError "applying simp to both sides reduces elementwise lemma for {src} {""
-                }to the trivial equality {ty'}. {""
-                }Either add `nosimp` or remove the `elementwise` attribute."
+              throwError "applying simp to both sides reduces elementwise lemma for {src} \
+                to the trivial equality {ty'}. \
+                Either add `nosimp` or remove the `elementwise` attribute."
         eqPf' ← mkExpectedTypeHint eqPf'' ty'
       if let some (w, instConcr) := instConcr? then
         return (← Meta.mkLambdaFVars (fvars.push instConcr) eqPf', w)

Mathlib/Tactic/Change.lean

@@ -39,8 +39,9 @@ elab_rules : tactic
     | some sop => do
       let tgt ← getMainTarget
       let ex ← withRef sop <| elabTermEnsuringType sop (← inferType tgt)
-      if !(← isDefEq ex tgt) then throwErrorAt sop "The term{indentD ex}\nis not defeq to the goal:{
-        indentD tgt}"
+      if !(← isDefEq ex tgt) then throwErrorAt sop "\
+        The term{indentD ex}\n\
+        is not defeq to the goal:{indentD tgt}"
       instantiateMVars ex
   let dstx ← delabToRefinableSyntax expr
   addSuggestion tk (← `(tactic| change $dstx)) (origSpan? := stx)

Mathlib/Tactic/ComputeDegree.lean

@@ -445,11 +445,10 @@ elab_rules : tactic | `(tactic| compute_degree $[!%$bang]?) => focus <| withMain
     | _ => none
   let twoH := twoHeadsArgs gt
   match twoH with
-    | (_, .anonymous, _) => throwError
-        (m!"'compute_degree' inapplicable. The goal{indentD gt}\nis expected to be '≤' or '='.")
-    | (.anonymous, _, _) => throwError
-        (m!"'compute_degree' inapplicable. The LHS must be an application of {
-          ""}'natDegree', 'degree', or 'coeff'.")
+    | (_, .anonymous, _) => throwError m!"'compute_degree' inapplicable. \
+        The goal{indentD gt}\nis expected to be '≤' or '='."
+    | (.anonymous, _, _) => throwError m!"'compute_degree' inapplicable. \
+        The LHS must be an application of 'natDegree', 'degree', or 'coeff'."
     | _ =>
       let lem := dispatchLemma twoH
       trace[Tactic.compute_degree] f!"'compute_degree' first applies lemma '{lem.getString}'"

Mathlib/Tactic/Core.lean

@@ -251,8 +251,8 @@ def getPackageDir (pkg : String) : IO System.FilePath := do
   let root? ← sp.findM? fun p =>
     (p / pkg).isDir <||> ((p / pkg).withExtension "lean").pathExists
   if let some root := root? then return root
-  throw <| IO.userError s!"Could not find {pkg} directory. {
-    ""}Make sure the LEAN_SRC_PATH environment variable is set correctly."
+  throw <| IO.userError s!"Could not find {pkg} directory. \
+    Make sure the LEAN_SRC_PATH environment variable is set correctly."
 
 /-- Returns the mathlib root directory. -/
 def getMathlibDir := getPackageDir "Mathlib"

Mathlib/Tactic/DeriveFintype.lean

@@ -133,8 +133,8 @@ def mkFintypeEnum (declName : Name) : CommandElabM Unit := do
           type := listType
           value := enumList }
       setProtected enumListName
-      addDocString enumListName s!"A list enumerating every element of the type, {
-        ""}which are all zero-argument constructors. (Generated by the `Fintype` deriving handler.)"
+      addDocString enumListName s!"A list enumerating every element of the type, \
+        which are all zero-argument constructors. (Generated by the `Fintype` deriving handler.)"
     do -- Prove that this list is in `toCtorIdx` order
       trace[Elab.Deriving.fintype] "proving {toCtorThmName}"
       let goalStx ← `(term| ∀ (x : $(← Term.exprToSyntax <| mkConst declName levels)),

Mathlib/Tactic/Eqns.lean

@@ -38,8 +38,8 @@ initialize eqnsAttribute : NameMapExtension (Array Name) ←
     add   := fun
     | declName, `(attr| eqns $[$names]*) => do
       if let some _ := Meta.eqnsExt.getState (← getEnv) |>.map.find? declName then
-        throwError "There already exist stored eqns for '{declName}' registering new equations{
-            "\n"}will not have the desired effect."
+        throwError "There already exist stored eqns for '{declName}'; registering new equations \
+          will not have the desired effect."
       names.mapM resolveGlobalConstNoOverloadWithInfo
     | _, _ => Lean.Elab.throwUnsupportedSyntax }
 

Mathlib/Tactic/FinCases.lean

@@ -30,8 +30,8 @@ def getMemType {m : Type → Type} [Monad m] [MonadError m] (e : Expr) : m (Opti
     | (``List, #[α])     => return α
     | (``Multiset, #[α]) => return α
     | (``Finset, #[α])   => return α
-    | _ => throwError ("Hypothesis must be of type `x ∈ (A : List α)`, `x ∈ (A : Finset α)`,"
-        ++ " or `x ∈ (A : Multiset α)`")
+    | _ => throwError "Hypothesis must be of type `x ∈ (A : List α)`, `x ∈ (A : Finset α)`, \
+                       or `x ∈ (A : Multiset α)`"
   | _ => return none
 
 /--

Mathlib/Tactic/GCongr/Core.lean

@@ -155,9 +155,9 @@ initialize registerBuiltinAttribute {
   add := fun decl _ kind ↦ MetaM.run' do
     let declTy := (← getConstInfo decl).type
     withReducible <| forallTelescopeReducing declTy fun xs targetTy => do
-    let fail := throwError
-      "@[gcongr] attribute only applies to lemmas proving {
-      ""}x₁ ~₁ x₁' → ... xₙ ~ₙ xₙ' → f x₁ ... xₙ ∼ f x₁' ... xₙ', got {declTy}"
+    let fail := throwError "\
+      @[gcongr] attribute only applies to lemmas proving \
+      x₁ ~₁ x₁' → ... xₙ ~ₙ xₙ' → f x₁ ... xₙ ∼ f x₁' ... xₙ', got {declTy}"
     -- verify that conclusion of the lemma is of the form `rel (head x₁ ... xₙ) (head y₁ ... yₙ)`
     let .app (.app rel lhs) rhs ← whnf targetTy | fail
     let some relName := rel.getAppFn.constName? | fail
@@ -404,8 +404,8 @@ partial def _root_.Lean.MVarId.gcongr
   let some (sErr, e) := ex?
     -- B. If there is a template, and there was no `@[gcongr]` lemma which matched the template,
     -- fail.
-    | throwError "gcongr failed, no @[gcongr] lemma applies for the template portion {""
-        }{template} and the relation {rel}"
+    | throwError "gcongr failed, no @[gcongr] lemma applies for the template portion \
+        {template} and the relation {rel}"
   -- B. If there is a template, and there was a `@[gcongr]` lemma which matched the template, but
   -- it was not possible to `apply` that lemma, then report the error message from `apply`-ing that
   -- lemma.
@@ -512,5 +512,5 @@ elab_rules : tactic
     | unsolvedGoalStates => do
       let unsolvedGoals ← @List.mapM MetaM _ _ _ MVarId.getType unsolvedGoalStates
       let g := Lean.MessageData.joinSep (unsolvedGoals.map Lean.MessageData.ofExpr) Format.line
-      throwError "rel failed, cannot prove goal by 'substituting' the listed relationships. {""
-        }The steps which could not be automatically justified were: \n{g}"
+      throwError "rel failed, cannot prove goal by 'substituting' the listed relationships. \
+        The steps which could not be automatically justified were:\n{g}"

Mathlib/Tactic/LibrarySearch.lean

@@ -275,8 +275,8 @@ elab_rules : tactic | `(tactic| apply? $[using $[$required],*]?) => do
   exact? (← getRef) required false
 
 elab tk:"library_search" : tactic => do
-  logWarning ("`library_search` has been renamed to `apply?`" ++
-    " (or `exact?` if you only want solutions closing the goal)")
+  logWarning "`library_search` has been renamed to `apply?` \
+    (or `exact?` if you only want solutions closing the goal)"
   exact? tk none false
 
 open Elab Term in

Mathlib/Tactic/MoveAdd.lean

@@ -388,8 +388,9 @@ def unifyMovements (data : Array (Expr × Bool × Syntax)) (tgt : Expr) :
   let atoms := (ops.map Prod.fst).flatten.toList.filter (!isBVar ·)
   -- `instr` are the unified user-provided terms, `neverMatched` are non-unified ones
   let (instr, neverMatched) ← pairUp data.toList atoms
-  let dbgMsg := #[m!"Matching of input variables:\n* pre-match:  {
-    data.map (Prod.snd ∘ Prod.snd)}\n* post-match: {instr}",
+  let dbgMsg := #[m!"Matching of input variables:\n\
+    * pre-match:  {data.map (Prod.snd ∘ Prod.snd)}\n\
+    * post-match: {instr}",
     m!"\nMaximum number of iterations: {ops.size}"]
   -- if there are `neverMatched` terms, return the parsed terms and the syntax
   let errMsg := neverMatched.map fun (t, a, stx) => (if a then m!"← {t}" else m!"{t}", stx)

Mathlib/Tactic/Nontriviality/Core.lean

@@ -109,8 +109,8 @@ syntax (name := nontriviality) "nontriviality" (ppSpace colGt term)?
       if let some (α, _) := tgt.eq? then return α
       if let some (α, _) := tgt.app4? ``LE.le then return α
       if let some (α, _) := tgt.app4? ``LT.lt then return α
-      throwError "The goal is not an (in)equality, so you'll need to specify the desired {""
-        }`Nontrivial α` instance by invoking `nontriviality α`.")
+      throwError "The goal is not an (in)equality, so you'll need to specify the desired \
+        `Nontrivial α` instance by invoking `nontriviality α`.")
     let .sort u ← whnf (← inferType α) | unreachable!
     let some v := u.dec | throwError "not a type{indentExpr α}"
     let α : Q(Type v) := α