Leanのバージョンを v4.28.0-rc1 に更新する

Author: Seasawher

LeanByExample/Declarative/Opaque.lean

@@ -67,10 +67,10 @@ structure Something where
 
 -- Inhabited インスタンスがないのでエラーになる
 /-⋆-//--
-error: failed to synthesize
-  Inhabited Something
+error: failed to synthesize 'Inhabited' or 'Nonempty' instance for
+  Something
 
-Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+If this type is defined using the 'structure' or 'inductive' command, you can try adding a 'deriving Nonempty' clause to it.
 -/
 #guard_msgs in --#
 opaque something : Something

LeanByExample/Modifier/DocComment/ParseError.lean

@@ -8,7 +8,7 @@ def parse (cat : Name) (s : String) : MetaM Syntax := do
 
 -- ドキュメントコメントで `namespace` を修飾しようとすると構文エラーになる
 /-⋆-//--
-error: <input>:1:21: expected '#guard_msgs', 'abbrev', 'add_decl_doc', 'axiom', 'binder_predicate', 'builtin_dsimproc', 'builtin_dsimproc_decl', 'builtin_grind_propagator', 'builtin_initialize', 'builtin_simproc', 'builtin_simproc_decl', 'class', 'coinductive', 'declare_command_config_elab', 'declare_config_elab', 'declare_config_getter', 'declare_simp_like_tactic', 'declare_syntax_cat', 'def', 'dsimproc', 'dsimproc_decl', 'elab', 'elab_rules', 'example', 'grind_propagator', 'inductive', 'infix', 'infixl', 'infixr', 'initialize', 'instance', 'macro', 'macro_rules', 'notation', 'opaque', 'postfix', 'prefix', 'recommended_spelling', 'register_builtin_option', 'register_error_explanation', 'register_label_attr', 'register_linter_set', 'register_option', 'register_simp_attr', 'register_tactic_tag', 'register_try?_tactic', 'simproc', 'simproc_decl', 'structure', 'syntax', 'tactic_extension', 'theorem' or 'unif_hint'
+error: <input>:1:21: expected '#guard_msgs', 'abbrev', 'add_decl_doc', 'axiom', 'binder_predicate', 'builtin_dsimproc', 'builtin_dsimproc_decl', 'builtin_grind_propagator', 'builtin_initialize', 'builtin_simproc', 'builtin_simproc_decl', 'class', 'coinductive', 'declare_command_config_elab', 'declare_config_elab', 'declare_config_getter', 'declare_simp_like_tactic', 'declare_syntax_cat', 'def', 'dsimproc', 'dsimproc_decl', 'elab', 'elab_rules', 'example', 'grind_propagator', 'inductive', 'infix', 'infixl', 'infixr', 'initialize', 'instance', 'macro', 'macro_rules', 'notation', 'opaque', 'postfix', 'prefix', 'recommended_spelling', 'register_builtin_option', 'register_error_explanation', 'register_grind_attr', 'register_label_attr', 'register_linter_set', 'register_option', 'register_simp_attr', 'register_tactic_tag', 'register_try?_tactic', 'simproc', 'simproc_decl', 'structure', 'syntax', 'tactic_extension', 'theorem' or 'unif_hint'
 -/
 #guard_msgs in --#
 #eval parse `command "/-- これはドキュメントコメント -/ namespace Foo"

LeanByExample/Tactic/Hint.lean

@@ -46,14 +46,14 @@ def getRegisteredTactics : CoreM Unit := do
     IO.println arr[0]!
 
 /-⋆-//--
-info: "noncomm_ring"
-"group"
-"finiteness"
-"field"
-"field_simp"
+info: "group"
 "compute_degree"
+"noncomm_ring"
+"finiteness"
 "ring"
 "linarith"
+"field"
+"field_simp"
 "positivity"
 "bound"
 "abel"

LeanByExample/Tactic/Sorry.lean

@@ -7,7 +7,7 @@ import Lean --#
 def FermatLastTheorem :=
   ∀ x y z n : Nat, n > 2 ∧ x * y * z ≠ 0 → x ^ n + y ^ n ≠ z ^ n
 
-/-⋆-//-- warning: declaration uses 'sorry' -/
+/-⋆-//-- warning: declaration uses `sorry` -/
 #guard_msgs (warning) in --#
 theorem flt : FermatLastTheorem :=
   sorry

LeanByExample/Tactic/TryQuestion.lean

@@ -17,10 +17,6 @@ example (as : List α) : (reverse as).head? = as.last? := by
   -- grind 単体では証明ができない
   fail_if_success grind
 
-  -- 帰納法を適当に使ってみてもダメ
-  fail_if_success induction as with grind
-  fail_if_success fun_induction last? <;> grind
-
   -- try? なら証明を見つけることができる
   try?
 

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "64c76eabb64d58848cd5a272f58dfa31f3d1e3ea",
+   "rev": "946b120add760bbddb7b89608957d12b0fb16230",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "8e0524310148337b54602f6f1b30578ee2910106",
+   "rev": "2cd9b4f8b6f88bb12cfb08c7480131161c9bfe08",
    "name": "mdgen",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "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": "5ce7f0a355f522a952a3d678d696bd563bb4fd28",
+   "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8f497d55985a189cea8020d9dc51260af1e41ad2",
+   "rev": "b5908dbac486279f1133cb937648c63c30b455af",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,17 +55,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",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "bd58c9efe2086d56ca361807014141a860ddbf8c",
+   "rev": "23324752757bf28124a518ec284044c8db79fee5",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "45926c76c3e0d876e39b3e9e5e77080fef0b10ba",
+   "rev": "8fda52e157c840eb11716f8410f3ca2096d325f0",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,10 +95,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": "«Lean by Example»",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.27.0
+leanprover/lean4:v4.28.0-rc1