Update tests

Author: nomeata

tests/lean/1038.lean.expected.out

@@ -1 +1 @@
-1038.lean:1:7-1:21: error(lean.unknownIdentifier): Unknown constant `IO.FS.realpath`
+1038.lean:1:10-1:12: error(lean.unknownIdentifier): Unknown constant `IO.FS.realpath`

tests/lean/346.lean.expected.out

@@ -1,5 +1,5 @@
-346.lean:10:6-10:16: error(lean.unknownIdentifier): Unknown constant `SomeType.b`
-346.lean:13:2-13:5: error: Invalid field `z`: The environment does not contain `Nat.z`
+346.lean:10:15-10:16: error(lean.unknownIdentifier): Unknown constant `SomeType.b`
+346.lean:13:4-13:5: error: Invalid field `z`: The environment does not contain `Nat.z`
   x
 has type
   Nat

tests/lean/funind_errors.lean.expected.out

@@ -1,5 +1,5 @@
 funind_errors.lean:4:7-4:26: error(lean.unknownIdentifier): Unknown identifier `doesNotExist.induct`
-funind_errors.lean:22:7-22:23: error(lean.unknownIdentifier): Unknown constant `takeWhile.induct`
+funind_errors.lean:22:17-22:23: error(lean.unknownIdentifier): Unknown constant `takeWhile.induct`
 takeWhile.foo.induct.{u_1} {α : Type u_1} (p : α → Bool) (as : Array α) (motive : Nat → Array α → Prop)
   (case1 :
     ∀ (i : Nat) (r : Array α) (h : i < as.size),
@@ -10,5 +10,5 @@ takeWhile.foo.induct.{u_1} {α : Type u_1} (p : α → Bool) (as : Array α) (mo
       have a := as[i];
       ¬p a = true → motive i r)
   (case3 : ∀ (i : Nat) (r : Array α), ¬i < as.size → motive i r) (i : Nat) (r : Array α) : motive i r
-funind_errors.lean:38:7-38:20: error(lean.unknownIdentifier): Unknown constant `idEven.induct`
-funind_errors.lean:45:7-45:19: error(lean.unknownIdentifier): Unknown constant `idAcc.induct`
+funind_errors.lean:38:14-38:20: error(lean.unknownIdentifier): Unknown constant `idEven.induct`
+funind_errors.lean:45:13-45:19: error(lean.unknownIdentifier): Unknown constant `idAcc.induct`

tests/lean/run/issue10821.lean

@@ -1,3 +1,5 @@
+set_option linter.deprecated true
+
 /-!
 Checks that deprecated names in projection notation cause just
 the name to be marked, not the whole expression.