chore: bump to v4.8.0-rc1 (leanprover-community#39)

m4lvin · May 6, 2024 · 6d5b2c3 · 6d5b2c3
1 parent 683fa0c
commit 6d5b2c3
Show file tree

Hide file tree

Showing 14 changed files with 40 additions and 31 deletions.
diff --git a/REPL/Main.lean b/REPL/Main.lean
@@ -208,18 +208,18 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do
   let cmdSnapshot :=
   { cmdState
     cmdContext := (cmdSnapshot?.map fun c => c.cmdContext).getD
-      { fileName := "", fileMap := default, tacticCache? := none } }
+      { fileName := "", fileMap := default, tacticCache? := none, snap? := none } }
   let env ← recordCommandSnapshot cmdSnapshot
   let jsonTrees := match s.infotree with
   | some "full" => trees
   | some "tactics" => trees.bind InfoTree.retainTacticInfo
   | some "original" => trees.bind InfoTree.retainTacticInfo |>.bind InfoTree.retainOriginal
   | some "substantive" => trees.bind InfoTree.retainTacticInfo |>.bind InfoTree.retainSubstantive
   | _ => []
-  let infotree := if jsonTrees.isEmpty then
-    none
+  let infotree ← if jsonTrees.isEmpty then
+    pure none
   else
-    some <| Json.arr (← jsonTrees.toArray.mapM fun t => t.toJson none)
+    pure <| some <| Json.arr (← jsonTrees.toArray.mapM fun t => t.toJson none)
   return .inl
     { env,
       messages,

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.7.0
+leanprover/lean4:v4.8.0-rc1
diff --git a/test/Mathlib/lake-manifest.json b/test/Mathlib/lake-manifest.json
@@ -4,7 +4,7 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "32983874c1b897d78f20d620fe92fc8fd3f06c3a",
+   "rev": "3025cb124492b423070f20cf0a70636f757d117f",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "5fefb40a7c9038a7150e7edd92e43b1b94c49e79",
+   "rev": "0a21a48c286c4a4703c0be6ad2045f601f31b1d0",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -31,16 +31,16 @@
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8",
+   "rev": "fe1eff53bd0838c657aa6126fe4dd75ad9939d9a",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.30",
+   "inputRev": "v0.0.35",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5",
+   "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -49,7 +49,7 @@
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "rev": "61a79185b6582573d23bf7e17f2137cd49e7e662",
+   "rev": "188eb34fcf1125e89d651ad462d02598219718ca",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -58,10 +58,10 @@
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
-   "rev": "a45ae63747140c1b2cbad9d46f518015c047047a",
+   "rev": "db651742f2c631e5b8525e9aabcf3d61ed094a4a",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.7.0",
+   "inputRev": "v4.8.0-rc1",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "«repl-mathlib-tests»",

diff --git a/test/Mathlib/lakefile.lean b/test/Mathlib/lakefile.lean
@@ -3,7 +3,7 @@ open Lake DSL
 
 package «repl-mathlib-tests» where
   -- add package configuration options here
-  require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.7.0"
+  require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.8.0-rc1"
 
 @[default_target]
 lean_lib «ReplMathlibTests» where

diff --git a/test/Mathlib/lean-toolchain b/test/Mathlib/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.7.0
+leanprover/lean4:v4.8.0-rc1
diff --git a/test/Mathlib/test/H20231115.expected.out b/test/Mathlib/test/H20231115.expected.out
@@ -14,6 +14,6 @@
 
 {"proofState": 1,
  "goals":
- ["case zero\n⊢ Nat.zero + 1 > Nat.zero",
-  "case succ\nx : Nat\nhx : x + 1 > x\n⊢ Nat.succ x + 1 > Nat.succ x"]}
+ ["case zero\n⊢ 0 + 1 > 0",
+  "case succ\nx : Nat\nhx : x + 1 > x\n⊢ x + 1 + 1 > x + 1"]}
 
diff --git a/test/Mathlib/test/H20231115_2.expected.out b/test/Mathlib/test/H20231115_2.expected.out
@@ -3,11 +3,11 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 3, "column": 12},
-   "goal": "case zero\n⊢ Nat.zero + 1 > Nat.zero",
+   "goal": "case zero\n⊢ 0 + 1 > 0",
    "endPos": {"line": 3, "column": 17}},
   {"proofState": 1,
    "pos": {"line": 3, "column": 12},
-   "goal": "case succ\nx : Nat\nhx : x + 1 > x\n⊢ Nat.succ x + 1 > Nat.succ x",
+   "goal": "case succ\nx : Nat\nhx : x + 1 > x\n⊢ x + 1 + 1 > x + 1",
    "endPos": {"line": 3, "column": 17}}],
  "messages":
  [{"severity": "warning",

diff --git a/test/Mathlib/test/H20231115_3.expected.out b/test/Mathlib/test/H20231115_3.expected.out
@@ -5,6 +5,6 @@
    "pos": {"line": 1, "column": 33},
    "endPos": {"line": 2, "column": 24},
    "data":
-   "unsolved goals\ncase zero\n⊢ Nat.zero + 1 > Nat.zero\n\ncase succ\nx : Nat\nhx : x + 1 > x\n⊢ Nat.succ x + 1 > Nat.succ x"}],
+   "unsolved goals\ncase zero\n⊢ 0 + 1 > 0\n\ncase succ\nx : Nat\nhx : x + 1 > x\n⊢ x + 1 + 1 > x + 1"}],
  "env": 1}
 
diff --git a/test/Mathlib/test/H20231214.lean b/test/Mathlib/test/H20231214.lean
@@ -12,6 +12,14 @@ but is expected to have type
   p x = 6 / x * p x : Prop
 ---
 error: unsolved goals
+case calc.step
+p q : ℝ → ℝ
+h₀ : ∀ (x : ℝ), p x = 2 - x ^ 2
+h₁ : ∀ (x : ℝ), x ≠ 0 → q x = 6 / x
+x : ℝ
+⊢ 6 / 2 * 6 / x * (6 / x) = 6 / x
+---
+error: unsolved goals
 p q : ℝ → ℝ
 h₀ : ∀ (x : ℝ), p x = 2 - x ^ 2
 h₁ : ∀ (x : ℝ), x ≠ 0 → q x = 6 / x

diff --git a/test/Mathlib/test/exact.expected.out b/test/Mathlib/test/exact.expected.out
@@ -17,7 +17,7 @@
  [{"severity": "info",
    "pos": {"line": 0, "column": 0},
    "endPos": {"line": 0, "column": 0},
-   "data": "Try this: exact Nat.zero_lt_one"}],
+   "data": "Try this: exact Nat.one_pos"}],
  "goals": []}
 
 {"sorries":

diff --git a/test/Mathlib/test/exact.in b/test/Mathlib/test/exact.in
@@ -1,4 +1,4 @@
-{"cmd": "import Mathlib\n\nset_option maxHeartbeats 500000"}
+{"cmd": "import Mathlib"}
 
 {"cmd": "theorem test : 0 < 1 := by sorry", "env": 0}
 

diff --git a/test/Mathlib/test/induction.expected.out b/test/Mathlib/test/induction.expected.out
@@ -14,16 +14,14 @@
 
 {"proofState": 1,
  "goals":
- ["case zero\n⊢ Nat.zero = Nat.zero",
-  "case succ\nn✝ : ℕ\nn_ih✝ : n✝ = n✝\n⊢ Nat.succ n✝ = Nat.succ n✝"]}
+ ["case zero\n⊢ 0 = 0", "case succ\nn✝ : ℕ\na✝ : n✝ = n✝\n⊢ n✝ + 1 = n✝ + 1"]}
 
 {"proofState": 2,
- "goals": ["case succ\nn✝ : ℕ\nn_ih✝ : n✝ = n✝\n⊢ Nat.succ n✝ = Nat.succ n✝"]}
+ "goals": ["case succ\nn✝ : ℕ\na✝ : n✝ = n✝\n⊢ n✝ + 1 = n✝ + 1"]}
 
 {"sorries":
- [{"proofState": 3, "goal": "case zero\n⊢ Nat.zero = Nat.zero"},
-  {"proofState": 4,
-   "goal": "case succ\nx : ℕ\nn_ih✝ : x = x\n⊢ Nat.succ x = Nat.succ x"}],
+ [{"proofState": 3, "goal": "case zero\n⊢ 0 = 0"},
+  {"proofState": 4, "goal": "case succ\nx : ℕ\na✝ : x = x\n⊢ x + 1 = x + 1"}],
  "proofState": 5,
  "goals": []}
 
diff --git a/test/infotree.expected.out b/test/infotree.expected.out
@@ -2,7 +2,8 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 7},
    "endPos": {"line": 1, "column": 8},
-   "data": "unused variable `h` [linter.unusedVariables]"}],
+   "data":
+   "unused variable `h`\nnote: this linter can be disabled with `set_option linter.unusedVariables false`"}],
  "infotree":
  [{"node":
    {"stx":

diff --git a/test/variables.expected.out b/test/variables.expected.out
@@ -4,7 +4,8 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 12},
    "endPos": {"line": 1, "column": 13},
-   "data": "unused variable `y` [linter.unusedVariables]"}],
+   "data":
+   "unused variable `y`\nnote: this linter can be disabled with `set_option linter.unusedVariables false`"}],
  "env": 1}
 
 {"sorries":
@@ -17,7 +18,8 @@
  [{"severity": "warning",
    "pos": {"line": 1, "column": 12},
    "endPos": {"line": 1, "column": 13},
-   "data": "unused variable `y` [linter.unusedVariables]"},
+   "data":
+   "unused variable `y`\nnote: this linter can be disabled with `set_option linter.unusedVariables false`"},
   {"severity": "warning",
    "pos": {"line": 1, "column": 8},
    "endPos": {"line": 1, "column": 15},
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:v4.7.0
		leanprover/lean4:v4.8.0-rc1