diff --git a/lean-toolchain b/lean-toolchain
index 5249182c..4bafde20 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.27.0
+leanprover/lean4:v4.28.0-rc1
diff --git a/test/Mathlib/lake-manifest.json b/test/Mathlib/lake-manifest.json
index 1105821d..6605beba 100644
--- a/test/Mathlib/lake-manifest.json
+++ b/test/Mathlib/lake-manifest.json
@@ -5,17 +5,17 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "a3a10db0e9d66acbebf76c5e6a135066525ac900",
+   "rev": "5352afccd6866369be9de43f5b7ec47203555f44",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.27.0",
+   "inputRev": "v4.28.0-rc1",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "009dc1e6f2feb2c96c081537d80a0905b2c6498f",
+   "rev": "7311586e1a56af887b1081d05e80c11b6c41d212",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8f497d55985a189cea8020d9dc51260af1e41ad2",
+   "rev": "875ad9d88ed684e39c16bdea260e6ecfa15afd60",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,17 +45,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c04225ee7c0585effbd933662b3151f01b600e40",
+   "rev": "6d65c6e0a25b8a52c13c3adeb63ecde3bfbb6294",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.85",
+   "inputRev": "v0.0.86",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "cb837cc26236ada03c81837bebe0acd9c70ced7d",
+   "rev": "f08e838d4f9aea519f3cde06260cfb686fd4bab0",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "bd58c9efe2086d56ca361807014141a860ddbf8c",
+   "rev": "23324752757bf28124a518ec284044c8db79fee5",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b25b36a7caf8e237e7d1e6121543078a06777c8a",
+   "rev": "cabbb5a025bfbbc50af9184ed2dfdde6ea4f53a7",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,10 +85,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "55c37290ff6186e2e965d68cf853a57c0702db82",
+   "rev": "28e0856d4424863a85b18f38868c5420c55f9bae",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.27.0",
+   "inputRev": "v4.28.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "«repl-mathlib-tests»",
diff --git a/test/Mathlib/lakefile.toml b/test/Mathlib/lakefile.toml
index f97faa28..f67bbae9 100644
--- a/test/Mathlib/lakefile.toml
+++ b/test/Mathlib/lakefile.toml
@@ -4,7 +4,7 @@ defaultTargets = ["ReplMathlibTests"]
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4"
-rev = "v4.27.0"
+rev = "v4.28.0-rc1"
 
 [[lean_lib]]
 name = "ReplMathlibTests"
diff --git a/test/Mathlib/lean-toolchain b/test/Mathlib/lean-toolchain
index 5249182c..4bafde20 100644
--- a/test/Mathlib/lean-toolchain
+++ b/test/Mathlib/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.27.0
+leanprover/lean4:v4.28.0-rc1
diff --git a/test/Mathlib/test/20240209.expected.out b/test/Mathlib/test/20240209.expected.out
index b7cfc2da..7053ba92 100644
--- a/test/Mathlib/test/20240209.expected.out
+++ b/test/Mathlib/test/20240209.expected.out
@@ -7,7 +7,7 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 0},
    "endPos": {"line": 1, "column": 7},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 0}
 
 {"proofStatus": "Incomplete: contains sorry",
diff --git a/test/Mathlib/test/H20231115.expected.out b/test/Mathlib/test/H20231115.expected.out
index e283b375..88908ebd 100644
--- a/test/Mathlib/test/H20231115.expected.out
+++ b/test/Mathlib/test/H20231115.expected.out
@@ -9,7 +9,7 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 0},
    "endPos": {"line": 1, "column": 7},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 1}
 
 {"proofStatus": "Incomplete: open goals remain",
diff --git a/test/Mathlib/test/H20231115_2.expected.out b/test/Mathlib/test/H20231115_2.expected.out
index 3c19b57e..f60c784f 100644
--- a/test/Mathlib/test/H20231115_2.expected.out
+++ b/test/Mathlib/test/H20231115_2.expected.out
@@ -13,6 +13,6 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 0},
    "endPos": {"line": 1, "column": 7},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 1}
 
diff --git a/test/Mathlib/test/H20231215_2.expected.out b/test/Mathlib/test/H20231215_2.expected.out
index 1a83bcff..a69a6b44 100644
--- a/test/Mathlib/test/H20231215_2.expected.out
+++ b/test/Mathlib/test/H20231215_2.expected.out
@@ -9,6 +9,6 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 8},
    "endPos": {"line": 1, "column": 30},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 1}
 
diff --git a/test/Mathlib/test/exact.expected.out b/test/Mathlib/test/exact.expected.out
index 005f1158..c74a47c8 100644
--- a/test/Mathlib/test/exact.expected.out
+++ b/test/Mathlib/test/exact.expected.out
@@ -9,7 +9,7 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 8},
    "endPos": {"line": 1, "column": 12},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 1}
 
 {"proofStatus": "Completed",
@@ -30,7 +30,7 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 8},
    "endPos": {"line": 1, "column": 12},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 2}
 
 {"message":
diff --git a/test/Mathlib/test/file_env.expected.out b/test/Mathlib/test/file_env.expected.out
index b2293847..9cf0d19e 100644
--- a/test/Mathlib/test/file_env.expected.out
+++ b/test/Mathlib/test/file_env.expected.out
@@ -9,7 +9,7 @@
  [{"severity": "warning",
    "pos": {"line": 3, "column": 8},
    "endPos": {"line": 3, "column": 12},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 1}
 
 {"messages":
diff --git a/test/Mathlib/test/induction.expected.out b/test/Mathlib/test/induction.expected.out
index 7f80087a..2ed01f8c 100644
--- a/test/Mathlib/test/induction.expected.out
+++ b/test/Mathlib/test/induction.expected.out
@@ -9,7 +9,7 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 8},
    "endPos": {"line": 1, "column": 11},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 1}
 
 {"proofStatus": "Incomplete: open goals remain",
diff --git a/test/Mathlib/test/line_breaks.expected.out b/test/Mathlib/test/line_breaks.expected.out
index 8c4bd32e..d0ce3af7 100644
--- a/test/Mathlib/test/line_breaks.expected.out
+++ b/test/Mathlib/test/line_breaks.expected.out
@@ -9,6 +9,6 @@
  [{"severity": "warning",
    "pos": {"line": 3, "column": 8},
    "endPos": {"line": 3, "column": 12},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 1}
 
diff --git a/test/Mathlib/test/on_goal.expected.out b/test/Mathlib/test/on_goal.expected.out
index 510cfe1b..3ee4801d 100644
--- a/test/Mathlib/test/on_goal.expected.out
+++ b/test/Mathlib/test/on_goal.expected.out
@@ -9,7 +9,7 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 0},
    "endPos": {"line": 1, "column": 7},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 1}
 
 {"sorries":
diff --git a/test/Mathlib/test/pickle.expected.out b/test/Mathlib/test/pickle.expected.out
index e3d1c163..65e435d8 100644
--- a/test/Mathlib/test/pickle.expected.out
+++ b/test/Mathlib/test/pickle.expected.out
@@ -9,7 +9,7 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 8},
    "endPos": {"line": 1, "column": 25},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 1}
 
 {"proofStatus": "Incomplete: open goals remain",
diff --git a/test/Mathlib/test/placeholder_synthesis.expected.out b/test/Mathlib/test/placeholder_synthesis.expected.out
index ad26358f..16239500 100644
--- a/test/Mathlib/test/placeholder_synthesis.expected.out
+++ b/test/Mathlib/test/placeholder_synthesis.expected.out
@@ -17,7 +17,7 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 0},
    "endPos": {"line": 1, "column": 7},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 2}
 
 {"proofStatus": "Incomplete: open goals remain",
diff --git a/test/app_type_mismatch.expected.out b/test/app_type_mismatch.expected.out
index 317d655e..faa7da51 100644
--- a/test/app_type_mismatch.expected.out
+++ b/test/app_type_mismatch.expected.out
@@ -14,7 +14,7 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 0},
    "endPos": {"line": 1, "column": 7},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 1}
 
 {"proofStatus": "Incomplete: open goals remain",
diff --git a/test/app_type_mismatch2.expected.out b/test/app_type_mismatch2.expected.out
index 37d6afe7..e85665fe 100644
--- a/test/app_type_mismatch2.expected.out
+++ b/test/app_type_mismatch2.expected.out
@@ -15,7 +15,7 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 0},
    "endPos": {"line": 1, "column": 7},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 1}
 
 {"proofStatus": "Incomplete: open goals remain",
diff --git a/test/assumption_proof.expected.out b/test/assumption_proof.expected.out
index 0c253350..063ca364 100644
--- a/test/assumption_proof.expected.out
+++ b/test/assumption_proof.expected.out
@@ -7,7 +7,7 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 8},
    "endPos": {"line": 1, "column": 10},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 0}
 
 {"proofStatus": "Completed", "proofState": 1, "goals": []}
diff --git a/test/by_cases.expected.out b/test/by_cases.expected.out
index 978df508..66f1da80 100644
--- a/test/by_cases.expected.out
+++ b/test/by_cases.expected.out
@@ -7,7 +7,7 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 8},
    "endPos": {"line": 1, "column": 11},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 0}
 
 {"proofStatus": "Incomplete: open goals remain",
diff --git a/test/calc.expected.out b/test/calc.expected.out
index 8db4c61b..61fe31c1 100644
--- a/test/calc.expected.out
+++ b/test/calc.expected.out
@@ -68,6 +68,6 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 0},
    "endPos": {"line": 1, "column": 7},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 0}
 
diff --git a/test/dup_sorries.expected.out b/test/dup_sorries.expected.out
index d01dd9b0..faa2cb61 100644
--- a/test/dup_sorries.expected.out
+++ b/test/dup_sorries.expected.out
@@ -7,7 +7,7 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 8},
    "endPos": {"line": 1, "column": 12},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 0}
 
 {"sorries":
@@ -19,6 +19,6 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 8},
    "endPos": {"line": 1, "column": 12},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 1}
 
diff --git a/test/have_by_sorry.expected.out b/test/have_by_sorry.expected.out
index 03c79017..9aa73517 100644
--- a/test/have_by_sorry.expected.out
+++ b/test/have_by_sorry.expected.out
@@ -19,7 +19,7 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 8},
    "endPos": {"line": 1, "column": 11},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 1}
 
 {"sorries": [{"proofState": 2, "goal": "x : Int\n⊢ x = 1"}],
diff --git a/test/invalid_tactic.expected.out b/test/invalid_tactic.expected.out
index 375164b7..252b13e5 100644
--- a/test/invalid_tactic.expected.out
+++ b/test/invalid_tactic.expected.out
@@ -7,7 +7,7 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 8},
    "endPos": {"line": 1, "column": 18},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 0}
 
 {"proofStatus": "Incomplete: contains sorry",
diff --git a/test/line_breaks.expected.out b/test/line_breaks.expected.out
index d6e980af..5a185261 100644
--- a/test/line_breaks.expected.out
+++ b/test/line_breaks.expected.out
@@ -7,7 +7,7 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 8},
    "endPos": {"line": 1, "column": 11},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 0}
 
 {"env": 1}
diff --git a/test/name_generator.expected.out b/test/name_generator.expected.out
index 987d0593..e3e88205 100644
--- a/test/name_generator.expected.out
+++ b/test/name_generator.expected.out
@@ -7,7 +7,7 @@
  [{"severity": "warning",
    "pos": {"line": 2, "column": 0},
    "endPos": {"line": 2, "column": 7},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 0}
 
 {"sorries": [{"proofState": 1, "goal": "x : Int\nh0 : x > 0\n⊢ x > 0"}],
diff --git a/test/pickle_open_scoped.expected.out b/test/pickle_open_scoped.expected.out
index df23507a..69bc7f51 100644
--- a/test/pickle_open_scoped.expected.out
+++ b/test/pickle_open_scoped.expected.out
@@ -11,7 +11,7 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 7},
    "endPos": {"line": 1, "column": 14},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 2}
 
 {"env": 1}
diff --git a/test/pickle_open_scoped_2.expected.out b/test/pickle_open_scoped_2.expected.out
index f21692d2..cbe6da59 100644
--- a/test/pickle_open_scoped_2.expected.out
+++ b/test/pickle_open_scoped_2.expected.out
@@ -9,6 +9,6 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 7},
    "endPos": {"line": 1, "column": 14},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 1}
 
diff --git a/test/pickle_proof_state_1.expected.out b/test/pickle_proof_state_1.expected.out
index 238b74c9..933d86a9 100644
--- a/test/pickle_proof_state_1.expected.out
+++ b/test/pickle_proof_state_1.expected.out
@@ -9,7 +9,7 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 4},
    "endPos": {"line": 1, "column": 5},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 1}
 
 {"proofStatus": "Incomplete: open goals remain",
diff --git a/test/pickle_proof_state_env.expected.out b/test/pickle_proof_state_env.expected.out
index 238b74c9..933d86a9 100644
--- a/test/pickle_proof_state_env.expected.out
+++ b/test/pickle_proof_state_env.expected.out
@@ -9,7 +9,7 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 4},
    "endPos": {"line": 1, "column": 5},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 1}
 
 {"proofStatus": "Incomplete: open goals remain",
diff --git a/test/proof_branching.expected.out b/test/proof_branching.expected.out
index bfea811d..537f0697 100644
--- a/test/proof_branching.expected.out
+++ b/test/proof_branching.expected.out
@@ -7,7 +7,7 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 8},
    "endPos": {"line": 1, "column": 19},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 0}
 
 {"proofStatus": "Incomplete: open goals remain",
diff --git a/test/proof_branching2.expected.out b/test/proof_branching2.expected.out
index 1bcd8e1e..8e59e256 100644
--- a/test/proof_branching2.expected.out
+++ b/test/proof_branching2.expected.out
@@ -7,7 +7,7 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 0},
    "endPos": {"line": 1, "column": 7},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 0}
 
 {"proofStatus": "Incomplete: open goals remain",
diff --git a/test/proof_step.expected.out b/test/proof_step.expected.out
index 013889b6..e751b9ff 100644
--- a/test/proof_step.expected.out
+++ b/test/proof_step.expected.out
@@ -7,7 +7,7 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 4},
    "endPos": {"line": 1, "column": 5},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 0}
 
 {"proofStatus": "Incomplete: open goals remain",
diff --git a/test/proof_transitivity.expected.out b/test/proof_transitivity.expected.out
index 45f4b082..b5de1caa 100644
--- a/test/proof_transitivity.expected.out
+++ b/test/proof_transitivity.expected.out
@@ -7,7 +7,7 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 0},
    "endPos": {"line": 1, "column": 7},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 0}
 
 {"proofStatus": "Completed", "proofState": 1, "goals": []}
@@ -21,7 +21,7 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 0},
    "endPos": {"line": 1, "column": 7},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 1}
 
 {"proofStatus": "Completed", "proofState": 3, "goals": []}
diff --git a/test/readme.expected.out b/test/readme.expected.out
index 7ffa1109..c69e0fe2 100644
--- a/test/readme.expected.out
+++ b/test/readme.expected.out
@@ -7,7 +7,7 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 4},
    "endPos": {"line": 1, "column": 5},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 0}
 
 {"proofStatus": "Incomplete: open goals remain",
diff --git a/test/self_proof_apply_check.expected.out b/test/self_proof_apply_check.expected.out
index 1de871f2..3a36e6d7 100644
--- a/test/self_proof_apply_check.expected.out
+++ b/test/self_proof_apply_check.expected.out
@@ -15,7 +15,7 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 8},
    "endPos": {"line": 1, "column": 10},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 1}
 
 {"proofStatus":
diff --git a/test/self_proof_check.expected.out b/test/self_proof_check.expected.out
index 48253d70..d0ea48aa 100644
--- a/test/self_proof_check.expected.out
+++ b/test/self_proof_check.expected.out
@@ -15,7 +15,7 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 8},
    "endPos": {"line": 1, "column": 10},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 1}
 
 {"message":
@@ -30,7 +30,7 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 8},
    "endPos": {"line": 1, "column": 10},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 2}
 
 {"message":
@@ -62,7 +62,7 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 8},
    "endPos": {"line": 1, "column": 10},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 3}
 
 {"message":
@@ -81,7 +81,7 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 8},
    "endPos": {"line": 1, "column": 10},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 4}
 
 {"message":
diff --git a/test/self_proof_exact_check.expected.out b/test/self_proof_exact_check.expected.out
index 1de871f2..3a36e6d7 100644
--- a/test/self_proof_exact_check.expected.out
+++ b/test/self_proof_exact_check.expected.out
@@ -15,7 +15,7 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 8},
    "endPos": {"line": 1, "column": 10},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 1}
 
 {"proofStatus":
diff --git a/test/self_proof_rw.expected.out b/test/self_proof_rw.expected.out
index c49bba92..bdb17e36 100644
--- a/test/self_proof_rw.expected.out
+++ b/test/self_proof_rw.expected.out
@@ -15,7 +15,7 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 8},
    "endPos": {"line": 1, "column": 24},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 1}
 
 {"proofStatus":
diff --git a/test/sorry_hypotheses.expected.out b/test/sorry_hypotheses.expected.out
index d59e9b1e..8162c9f6 100644
--- a/test/sorry_hypotheses.expected.out
+++ b/test/sorry_hypotheses.expected.out
@@ -7,7 +7,7 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 8},
    "endPos": {"line": 1, "column": 11},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 0}
 
 {"sorries": [{"proofState": 1, "goal": "x : Int\n⊢ x = 1"}],
diff --git a/test/tactic_mode_sorry.expected.out b/test/tactic_mode_sorry.expected.out
index 15c007e6..827d5696 100644
--- a/test/tactic_mode_sorry.expected.out
+++ b/test/tactic_mode_sorry.expected.out
@@ -7,7 +7,7 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 4},
    "endPos": {"line": 1, "column": 5},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 0}
 
 {"sorries": [{"proofState": 1, "goal": "⊢ Nat"}],
diff --git a/test/tactic_sorry.expected.out b/test/tactic_sorry.expected.out
index 0394d4f8..d93bc9e7 100644
--- a/test/tactic_sorry.expected.out
+++ b/test/tactic_sorry.expected.out
@@ -7,6 +7,6 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 4},
    "endPos": {"line": 1, "column": 5},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 0}
 
diff --git a/test/term_sorry.expected.out b/test/term_sorry.expected.out
index ab332e35..a178f8fd 100644
--- a/test/term_sorry.expected.out
+++ b/test/term_sorry.expected.out
@@ -7,6 +7,6 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 4},
    "endPos": {"line": 1, "column": 5},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 0}
 
diff --git a/test/trace_simp.expected.out b/test/trace_simp.expected.out
index 0f3bbba7..dd8bc6be 100644
--- a/test/trace_simp.expected.out
+++ b/test/trace_simp.expected.out
@@ -21,7 +21,7 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 0},
    "endPos": {"line": 1, "column": 7},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 4}
 
 {"traces": ["37"],
diff --git a/test/unknown_proof_state.expected.out b/test/unknown_proof_state.expected.out
index ee52464f..edaf1585 100644
--- a/test/unknown_proof_state.expected.out
+++ b/test/unknown_proof_state.expected.out
@@ -7,7 +7,7 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 4},
    "endPos": {"line": 1, "column": 5},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 0}
 
 {"message": "Unknown proof state."}
diff --git a/test/unknown_tactic.expected.out b/test/unknown_tactic.expected.out
index 7e55103b..1c1dc8ee 100644
--- a/test/unknown_tactic.expected.out
+++ b/test/unknown_tactic.expected.out
@@ -7,7 +7,7 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 4},
    "endPos": {"line": 1, "column": 5},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 0}
 
 {"message": "Lean error:\n<input>:1:1: unknown tactic"}
diff --git a/test/variables.expected.out b/test/variables.expected.out
index d67e84bd..4e99fc49 100644
--- a/test/variables.expected.out
+++ b/test/variables.expected.out
@@ -18,6 +18,6 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 8},
    "endPos": {"line": 1, "column": 15},
-   "data": "declaration uses 'sorry'"}],
+   "data": "declaration uses `sorry`"}],
  "env": 2}