diff --git a/REPL/Main.lean b/REPL/Main.lean index 0ef81ee..9cd2be5 100644 --- a/REPL/Main.lean +++ b/REPL/Main.lean @@ -208,7 +208,7 @@ 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 @@ -216,10 +216,10 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do | 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 index 9ad3040..d8a6d7e 100644 --- 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 index 52f878d..742d1c6 100644 --- 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 index 23a10ca..82bd628 100644 --- 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 index 9ad3040..d8a6d7e 100644 --- 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 index f386cb7..2efb1d8 100644 --- 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 index 39d6142..3c19b57 100644 --- 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 index 45b397f..3b72d40 100644 --- 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 index 24f3f20..fc8ad1c 100644 --- 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 index 1c1a057..86cd1c6 100644 --- 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 index 5764c0f..72b4c50 100644 --- 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 index 8e19362..7ef34d3 100644 --- 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 index 236e1ba..cb76c20 100644 --- 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 index 7643187..d6e4bdd 100644 --- 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},