chore: move to v4.9.0-rc1 (#46)

* chore: move to v4.9.0-rc1 * deprecations and test output
leanprover-community · Jun 7, 2024 · 7df77c0 · 7df77c0
1 parent 439687b
commit 7df77c0
Show file tree

Hide file tree

Showing 10 changed files with 28 additions and 24 deletions.
diff --git a/REPL/Frontend.lean b/REPL/Frontend.lean
@@ -20,7 +20,7 @@ def processCommandsWithInfoTrees
     (commandState : Command.State) : IO (Command.State × List Message × List InfoTree) := do
   let commandState := { commandState with infoState.enabled := true }
   let s ← IO.processCommands inputCtx parserState commandState <&> Frontend.State.commandState
-  let msgs := s.messages.msgs.toList.drop commandState.messages.msgs.size
+  let msgs := s.messages.toList.drop commandState.messages.toList.length
   let trees := s.infoState.trees.toList.drop commandState.infoState.trees.size
 
   pure (s, msgs, trees)

diff --git a/REPL/Main.lean b/REPL/Main.lean
@@ -208,7 +208,11 @@ 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, snap? := none } }
+      { fileName := "",
+        fileMap := default,
+        tacticCache? := none,
+        snap? := none,
+        cancelTk? := none } }
   let env ← recordCommandSnapshot cmdSnapshot
   let jsonTrees := match s.infotree with
   | some "full" => trees

diff --git a/REPL/Snapshots.lean b/REPL/Snapshots.lean
@@ -116,8 +116,8 @@ open Lean Elab Tactic
 /-- New messages in a `ProofSnapshot`, relative to an optional previous `ProofSnapshot`. -/
 def newMessages (new : ProofSnapshot) (old? : Option ProofSnapshot := none) : List Lean.Message :=
   match old? with
-  | none => new.coreState.messages.msgs.toList
-  | some old => new.coreState.messages.msgs.toList.drop (old.coreState.messages.msgs.size)
+  | none => new.coreState.messages.toList
+  | some old => new.coreState.messages.toList.drop (old.coreState.messages.toList.length)
 
 /-- New info trees in a `ProofSnapshot`, relative to an optional previous `ProofSnapshot`. -/
 def newInfoTrees (new : ProofSnapshot) (old? : Option ProofSnapshot := none) : List InfoTree :=

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.8.0
+leanprover/lean4:v4.9.0-rc1
diff --git a/test/Mathlib/lake-manifest.json b/test/Mathlib/lake-manifest.json
@@ -1,31 +1,31 @@
-{"version": 7,
+{"version": "1.0.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "551ff2d7dffd7af914cdbd01abbd449fe3e3d428",
+   "rev": "af2dda22771c59db026c48ac0aabc73b72b7a4de",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "nightly-testing",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "53156671405fbbd5402ed17a79bd129b961bd8d6",
+   "rev": "44f57616b0d9b8f9e5606f2c58d01df54840eba7",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "nightly-testing",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "53ba96ad7666d4a2515292974631629b5ea5dfee",
+   "rev": "f744aab6fc4e06553464e6ae66730a3b14b8e615",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "nightly-testing",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
@@ -49,7 +49,7 @@
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "rev": "77e081815b30b0d30707e1c5b0c6a6761f7a2404",
+   "rev": "7983e959f8f4a79313215720de3ef1eca2d6d474",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -58,10 +58,10 @@
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
-   "rev": "b5eba595428809e96f3ed113bc7ba776c5f801ac",
+   "rev": "bbf0d1e39b5faac9276413942ac15bd64de65c1e",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.8.0",
+   "inputRev": "master",
    "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.8.0"
+  require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "master"
 
 @[default_target]
 lean_lib «ReplMathlibTests» where

diff --git a/test/Mathlib/lean-toolchain b/test/Mathlib/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.8.0
+leanprover/lean4:v4.9.0-rc1
diff --git a/test/name_generator.expected.out b/test/name_generator.expected.out
@@ -24,13 +24,13 @@
  "goals": []}
 
 {"traces":
- ["[Meta.Tactic.simp.rewrite] @gt_iff_lt:1000, x > 0 ==> 0 < x",
+ ["[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] @gt_iff_lt:1000, x > 0 ==> 0 < x",
+ ["[Meta.Tactic.simp.rewrite] gt_iff_lt:1000, x > 0 ==> 0 < x",
   "[Meta.Tactic.simp.rewrite] h0:1000, 0 < x ==> True"],
  "proofState": 7,
  "goals": []}

diff --git a/test/no_goal_sorry.expected.out b/test/no_goal_sorry.expected.out
@@ -4,8 +4,8 @@
    "endPos": {"line": 2, "column": 18},
    "data": "type expected, got\n  (set Nat : ?m.8 PUnit)"},
   {"severity": "error",
-   "pos": {"line": 3, "column": 2},
-   "endPos": {"line": 3, "column": 7},
-   "data": "no goals to be solved"}],
+   "pos": {"line": 2, "column": 22},
+   "endPos": {"line": 2, "column": 24},
+   "data": "Case tag 'body' not found.\n\nThere are no cases to select."}],
  "env": 0}
 
diff --git a/test/trace_simp.expected.out b/test/trace_simp.expected.out
@@ -9,7 +9,7 @@
    "pos": {"line": 1, "column": 23},
    "endPos": {"line": 1, "column": 27},
    "data":
-   "[Meta.Tactic.simp.rewrite] f_def:1000, f ==> 37\n[Meta.Tactic.simp.rewrite] @eq_self:1000, 37 = 37 ==> True"}],
+   "[Meta.Tactic.simp.rewrite] f_def:1000, f ==> 37\n[Meta.Tactic.simp.rewrite] eq_self:1000, 37 = 37 ==> True"}],
  "env": 3}
 
 {"sorries":
@@ -28,7 +28,7 @@
 
 {"traces":
  ["[Meta.Tactic.simp.rewrite] f_def:1000, f ==> 37",
-  "[Meta.Tactic.simp.rewrite] @eq_self:1000, 37 = 37 ==> True"],
+  "[Meta.Tactic.simp.rewrite] eq_self:1000, 37 = 37 ==> True"],
  "proofState": 2,
  "goals": []}
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:v4.8.0
		leanprover/lean4:v4.9.0-rc1