chore: use backticks instead of single quotes for identifiers in messages

This PR standardizes the formatting of identifiers in error messages,
warnings, and diagnostics by using backticks instead of single quotes.
For example, `declaration uses 'sorry'` is now `declaration uses `sorry``.

This is a style improvement that makes code identifiers stand out better
in error messages and aligns with the convention used elsewhere in the
codebase where backticks are used for code formatting.

Author: alok

src/Lean/AddDecl.lean

@@ -68,7 +68,7 @@ def wasOriginallyTheorem (env : Environment) (declName : Name) : Bool :=
   getOriginalConstKind? env declName |>.map (· matches .thm) |>.getD false
 
 /-- If `warn.sorry` is set to true, then, so long as the message log does not already have any errors,
-declarations with `sorryAx` generate the "declaration uses 'sorry'" warning. -/
+declarations with `sorryAx` generate the "declaration uses `sorry`" warning. -/
 register_builtin_option warn.sorry : Bool := {
   defValue := true
   descr    := "warn about uses of `sorry` in declarations added to the environment"
@@ -91,10 +91,10 @@ def warnIfUsesSorry (decl : Declaration) : CoreM Unit := do
       -- These can appear without logged errors if `decl` is referring to declarations with elaboration errors;
       -- that's where a user should direct their focus.
       if let some (_, s) := sorries.find? (·.1) <|> sorries[0]? then
-        logWarning <| .tagged `hasSorry m!"declaration uses '{s}'"
+        logWarning <| .tagged `hasSorry m!"declaration uses `{s}`"
       else
         -- This case should not happen, but it ensures a warning will get logged no matter what.
-        logWarning <| .tagged `hasSorry m!"declaration uses 'sorry'"
+        logWarning <| .tagged `hasSorry m!"declaration uses `sorry`"
 
 builtin_initialize
   registerTraceClass `addDecl

src/Lean/Class.lean

@@ -159,7 +159,7 @@ def addClass (env : Environment) (clsName : Name) : Except MessageData Environme
   let some decl := env.find? clsName
     | throw m!"unknown declaration '{clsName}'"
   unless decl matches .inductInfo .. | .axiomInfo .. do
-    throw m!"invalid 'class', declaration '{.ofConstName clsName}' must be inductive datatype, structure, or constant"
+    throw m!"invalid `class`, declaration '{.ofConstName clsName}' must be inductive datatype, structure, or constant"
   let outParams ← checkOutParam 0 #[] #[] decl.type
   return classExtension.addEntry env { name := clsName, outParams }
 

src/Lean/Compiler/CSimpAttr.lean

@@ -50,7 +50,7 @@ def add (declName : Name) (kind : AttributeKind) : CoreM Unit := do
   if let some entry ← isConstantReplacement? declName then
     ext.add entry kind
   else
-    throwError "invalid 'csimp' theorem, only constant replacement theorems (e.g., `@f = @g`) are currently supported."
+    throwError "invalid `csimp` theorem, only constant replacement theorems (e.g., `@f = @g`) are currently supported."
 
 /--
 Tags compiler simplification theorems, which allow one value to be replaced by another equal value

src/Lean/Compiler/IR/Checker.lean

@@ -57,7 +57,7 @@ def markJP (j : JoinPointId) : M Unit :=
 def getDecl (c : Name) : M Decl := do
   let ctx ← read
   match findEnvDecl' (← getEnv) c ctx.decls with
-  | none   => throwCheckerError s!"depends on declaration '{c}', which has no executable code; consider marking definition as 'noncomputable'"
+  | none   => throwCheckerError s!"depends on declaration `{c}`, which has no executable code; consider marking definition as `noncomputable`"
   | some d => pure d
 
 def checkVar (x : VarId) : M Unit := do

src/Lean/Compiler/IR/EmitLLVM.lean

@@ -1067,7 +1067,7 @@ def emitSSet (builder : LLVM.Builder llvmctx) (x : VarId) (n : Nat) (offset : Na
   | IRType.uint16  => pure ("lean_ctor_set_uint16", ← LLVM.i16Type llvmctx)
   | IRType.uint32  => pure ("lean_ctor_set_uint32", ← LLVM.i32Type llvmctx)
   | IRType.uint64  => pure ("lean_ctor_set_uint64", ← LLVM.i64Type llvmctx)
-  | _              => throw s!"invalid type for 'lean_ctor_set': '{t}'"
+  | _              => throw s!"invalid type for `lean_ctor_set`: `{t}`"
   let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.unsignedType llvmctx, setty]
   let retty  ← LLVM.voidType llvmctx
   let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
@@ -1489,9 +1489,9 @@ def emitMainFn (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) : M
   let d ← getDecl `main
   let xs ← match d with
    | .fdecl (xs := xs) .. => pure xs
-   | _ =>  throw "Function declaration expected for 'main'"
+   | _ =>  throw "Function declaration expected for `main`"
 
-  unless xs.size == 2 || xs.size == 1 do throw s!"Invalid main function, main expected to have '2' or '1' arguments, found '{xs.size}' arguments"
+  unless xs.size == 2 || xs.size == 1 do throw s!"Invalid main function, main expected to have `2` or `1` arguments, found `{xs.size}` arguments"
   let env ← getEnv
   let usesLeanAPI := usesModuleFrom env `Lean
   let mainTy ← LLVM.functionType (← LLVM.i64Type llvmctx)

src/Lean/Compiler/LCNF/ToMono.lean

@@ -26,7 +26,7 @@ def Param.toMono (param : Param) : ToMonoM Param := do
   param.update (← toMonoType param.type)
 
 def throwNoncomputableError {α : Type} (declName : Name) : ToMonoM α :=
-  throwNamedError lean.dependsOnNoncomputable m!"failed to compile definition, consider marking it as 'noncomputable' because it depends on '{.ofConstName declName}', which is 'noncomputable'"
+  throwNamedError lean.dependsOnNoncomputable m!"failed to compile definition, consider marking it as `noncomputable` because it depends on '{.ofConstName declName}', which is `noncomputable`"
 
 def checkFVarUse (fvarId : FVarId) : ToMonoM Unit := do
   if let some declName := (← get).noncomputableVars.get? fvarId then

src/Lean/Data/Json/FromToJson/Basic.lean

@@ -191,7 +191,7 @@ protected def _root_.Float.fromJson? : Json → Except String Float
   | (Json.str "-Infinity") => Except.ok (-1.0 / 0.0)
   | (Json.str "NaN") => Except.ok (0.0 / 0.0)
   | (Json.num jn) => Except.ok jn.toFloat
-  | _ => Except.error "Expected a number or a string 'Infinity', '-Infinity', 'NaN'."
+  | _ => Except.error "Expected a number or a string `Infinity`, `-Infinity`, `NaN`."
 
 instance : FromJson Float where
   fromJson? := Float.fromJson?

src/Lean/DocString/Parser.lean

@@ -25,7 +25,7 @@ private partial def atLeastAux (n : Nat) (p : ParserFn) : ParserFn := fun c s =>
   if s.hasError then
     return if iniPos == s.pos && n == 0 then s.restore iniSz iniPos else s
   if iniPos == s.pos then
-    return s.mkUnexpectedError "invalid 'atLeast' parser combinator application, parser did not consume anything"
+    return s.mkUnexpectedError "invalid `atLeast` parser combinator application, parser did not consume anything"
   if s.stackSize > iniSz + 1 then
     s := s.mkNode nullKind iniSz
   atLeastAux (n - 1) p c s
@@ -64,7 +64,7 @@ private partial def atMostAux (n : Nat) (p : ParserFn) (msg : String) : ParserFn
     if s.hasError then
       return if iniPos == s.pos then s.restore iniSz iniPos else s
     if iniPos == s.pos then
-      return s.mkUnexpectedError "invalid 'atMost' parser combinator application, parser did not \
+      return s.mkUnexpectedError "invalid `atMost` parser combinator application, parser did not \
         consume anything"
     if s.stackSize > iniSz + 1 then
       s := s.mkNode nullKind iniSz

src/Lean/Elab/Binders.lean

@@ -854,7 +854,7 @@ def elabLetDeclAux (id : Syntax) (binders : Array Syntax) (typeStx : Syntax) (va
       let valResult ← elabTermEnsuringType valStx type
       let valResult ← mkLambdaFVars xs valResult (usedLetOnly := false)
       unless (← isDefEq val valResult) do
-        throwError "unexpected error when elaborating 'let'"
+        throwError "unexpected error when elaborating `let`"
   pure result
 
 structure LetIdDeclView where

src/Lean/Elab/BuiltinCommand.lean

@@ -286,7 +286,7 @@ private partial def elabChoiceAux (cmds : Array Syntax) (i : Nat) : CommandElabM
   let `(export $ns ($ids*)) := stx | throwUnsupportedSyntax
   let nss ← resolveNamespace ns
   let currNamespace ← getCurrNamespace
-  if nss == [currNamespace] then throwError "invalid 'export', self export"
+  if nss == [currNamespace] then throwError "invalid `export`, self export"
   let mut aliases := #[]
   for idStx in ids do
     let id := idStx.getId
@@ -515,7 +515,7 @@ open Lean.Parser.Command.InternalSyntax in
   | `($doc:docComment add_decl_doc $id) =>
     let declName ← liftCoreM <| realizeGlobalConstNoOverloadWithInfo id
     unless ((← getEnv).getModuleIdxFor? declName).isNone do
-      throwError "invalid 'add_decl_doc', declaration is in an imported module"
+      throwError "invalid `add_decl_doc`, declaration is in an imported module"
     if let .none ← findDeclarationRangesCore? declName then
       -- this is only relevant for declarations added without a declaration range
       -- in particular `Quot.mk` et al which are added by `init_quot`
@@ -532,7 +532,7 @@ open Lean.Parser.Command.InternalSyntax in
       if let some idx := vars.findIdx? (· == id.getId) then
         uids := uids.push sc.varUIds[idx]!
       else
-        throwError "invalid 'include', variable `{id}` has not been declared in the current scope"
+        throwError "invalid `include`, variable `{id}` has not been declared in the current scope"
     modifyScope fun sc => { sc with
       includedVars := sc.includedVars ++ uids.toList
       omittedVars := sc.omittedVars.filter (!uids.contains ·) }
@@ -571,7 +571,7 @@ open Lean.Parser.Command.InternalSyntax in
             omittedVars := omittedVars.push uid
             omitsUsed := omitsUsed.set! idx true
           else
-            throwError "invalid 'omit', `{ldecl.userName}` has not been declared in the current scope"
+            throwError "invalid `omit`, `{ldecl.userName}` has not been declared in the current scope"
       for o in omits, used in omitsUsed do
         unless used do
           throwError "`{o}` did not match any variables in the current scope"
@@ -592,10 +592,10 @@ open Lean.Parser.Command.InternalSyntax in
   logInfo m!"Lean {Lean.versionString}\nTarget: {target}{String.join platforms}"
 
 @[builtin_command_elab Parser.Command.exit] def elabExit : CommandElab := fun _ =>
-  logWarning "using 'exit' to interrupt Lean"
+  logWarning "using `exit` to interrupt Lean"
 
 @[builtin_command_elab Parser.Command.import] def elabImport : CommandElab := fun _ =>
-  throwError "invalid 'import' command, it must be used in the beginning of the file"
+  throwError "invalid `import` command, it must be used in the beginning of the file"
 
 @[builtin_command_elab Parser.Command.eoi] def elabEoi : CommandElab := fun _ =>
   return