chore: move to v4.7.0-rc1 (leanprover-community#35)

* chore: move to v4.7.0-rc1

* fix imports and tests

* 'fix' tests

REPL/Frontend.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import Lean.Elab.Frontend
-import REPL.Util.TermUnsafe
 
 open Lean Elab
 

REPL/Main.lean

@@ -6,7 +6,6 @@ Authors: Scott Morrison
 import REPL.JSON
 import REPL.Frontend
 import REPL.Util.Path
-import REPL.Util.TermUnsafe
 import REPL.Lean.ContextInfo
 import REPL.Lean.Environment
 import REPL.Lean.InfoTree

REPL/Snapshots.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import Lean.Replay
+import Lean.Elab.Command
 import REPL.Util.Pickle
 
 open Lean Elab

REPL/Util/Pickle.lean

@@ -3,7 +3,7 @@ Copyright (c) 2023 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import REPL.Util.TermUnsafe
+import Lean.Environment
 
 /-!
 # Pickling and unpickling objects

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.6.0
+leanprover/lean4:v4.7.0-rc1

test/Mathlib/lake-manifest.json

@@ -4,10 +4,10 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "a7543d1a6934d52086971f510e482d743fe30cf3",
+   "rev": "ff9850c4726f6b9fb8d8e96980c3fcb2900be8bd",
    "name": "std",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.6.0",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/quote4",
@@ -22,19 +22,19 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "c51fa8ea4de8b203f64929cba19d139e555f9f6b",
+   "rev": "056ca0fa8f5585539d0b940f532d9750c3a2270f",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.6.0",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "16cae05860b208925f54e5581ec5fd264823440c",
+   "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.29",
+   "inputRev": "v0.0.30",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
@@ -58,10 +58,10 @@
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
-   "rev": "7ca43cbd6aa34058a1afad8e47190af3ec1f9bdb",
+   "rev": "fa48894a5d2780c6593a224003a660ca039e3e8f",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.6.0",
+   "inputRev": "v4.7.0-rc1",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "«repl-mathlib-tests»",

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.6.0"
+  require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.7.0-rc1"
 
 @[default_target]
 lean_lib «ReplMathlibTests» where

test/Mathlib/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.6.0
+leanprover/lean4:v4.7.0-rc1

test/Mathlib/test/20240209.expected.out

@@ -1,5 +1,3 @@
-{"env": 0}
-
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 1, "column": 22},
@@ -10,7 +8,7 @@
    "pos": {"line": 1, "column": 0},
    "endPos": {"line": 1, "column": 7},
    "data": "declaration uses 'sorry'"}],
- "env": 1}
+ "env": 0}
 
 {"proofState": 1,
  "messages":

test/Mathlib/test/20240209.in

@@ -1,5 +1,3 @@
-{"cmd": "import Std.Tactic.Simpa"}
-
-{"cmd": "example : False := by sorry", "env": 0}
+{"cmd": "example : False := by sorry"}
 
 {"tactic": "simpa using show False by done", "proofState": 0}

test/by_cases.expected.out

@@ -12,14 +12,14 @@
 
 {"proofState": 1,
  "goals":
- ["case inl\nx : Int\nh : x < 0\n⊢ x = x",
-  "case inr\nx : Int\nh : ¬x < 0\n⊢ x = x"]}
+ ["case pos\nx : Int\nh : x < 0\n⊢ x = x",
+  "case neg\nx : Int\nh : ¬x < 0\n⊢ x = x"]}
 
-{"proofState": 2, "goals": ["case inr\nx : Int\nh : ¬x < 0\n⊢ x = x"]}
+{"proofState": 2, "goals": ["case neg\nx : Int\nh : ¬x < 0\n⊢ x = x"]}
 
 {"sorries":
- [{"proofState": 3, "goal": "case inl\nx : Int\nh : x < 0\n⊢ x = x"},
-  {"proofState": 4, "goal": "case inr\nx : Int\nh : ¬x < 0\n⊢ x = x"}],
+ [{"proofState": 3, "goal": "case pos\nx : Int\nh : x < 0\n⊢ x = x"},
+  {"proofState": 4, "goal": "case neg\nx : Int\nh : ¬x < 0\n⊢ x = x"}],
  "proofState": 5,
  "goals": []}
 

test/by_cases.in

@@ -2,7 +2,7 @@
 
 {"proofState" : 0, "tactic": "by_cases h : x < 0"}
 
-{"proofState" : 1, "tactic": "case inl => rfl"}
+{"proofState" : 1, "tactic": "case pos => rfl"}
 
 {"proofState" : 1, "tactic": "all_goals sorry"}
 

test/name_generator.expected.out

@@ -23,11 +23,15 @@
  "proofState": 5,
  "goals": []}
 
-{"traces": ["[Meta.Tactic.simp.rewrite] h0:1000, x > 0 ==> True"],
+{"traces":
+ ["[Meta.Tactic.simp.rewrite] @gt_iff_lt:1000, x > 0 ==> 0 < x",
+  "[Meta.Tactic.simp.rewrite] h0:1000, 0 < x ==> True"],
  "proofState": 6,
  "goals": []}
 
-{"traces": ["[Meta.Tactic.simp.rewrite] h0:1000, x > 0 ==> True"],
+{"traces":
+ ["[Meta.Tactic.simp.rewrite] @gt_iff_lt:1000, x > 0 ==> 0 < x",
+  "[Meta.Tactic.simp.rewrite] h0:1000, 0 < x ==> True"],
  "proofState": 7,
  "goals": []}