chore: bump toolchain to v4.18.0-rc1 (#75)

* chore: bump toolchain to v4.18.0-rc1

* fix?

* chore: bump toolchain to v4.18.0-rc1

* fix tests

---------

Co-authored-by: Kim Morrison <kim@tqft.net>

Author: jcommelin

.gitignore

@@ -5,3 +5,4 @@
 /test/Mathlib/.lake
 /test/*.olean
 /test/*.olean.tmp
+/test/*.produced.out

REPL/Main.lean

@@ -212,7 +212,6 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do
     cmdContext := (cmdSnapshot?.map fun c => c.cmdContext).getD
       { fileName := "",
         fileMap := default,
-        tacticCache? := none,
         snap? := none,
         cancelTk? := none } }
   let env ← recordCommandSnapshot cmdSnapshot

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.17.0
+leanprover/lean4:v4.18.0-rc1

test.sh

@@ -34,8 +34,8 @@ for infile in $IN_DIR/*.in; do
         rm "$tmpfile"
     else
         echo "$base: FAILED"
-        # Remove the temporary file
-        rm "$tmpfile"
+        # Rename the temporary file instead of removing it
+        mv "$tmpfile" "${expectedfile/.expected.out/.produced.out}"
         exit 1
     fi
 

test/Mathlib/lake-manifest.json

@@ -5,17 +5,17 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "5269898d6a51d047931107c8d72d934d8d5d3753",
+   "rev": "6cecf71a82a22ea7c01598800e12f3e8eb66894b",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.17.0",
+   "inputRev": "v4.18.0-rc1",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c708be04267e3e995a14ac0d08b1530579c1525a",
+   "rev": "ebfb31672ab0a5b6d00a018ff67d2ec51ed66f3a",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "0447b0a7b7f41f0a1749010db3f222e4a96f9d30",
+   "rev": "08372f1ec11df288ff76621ead7b0b575cb29355",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,17 +45,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "799f6986de9f61b784ff7be8f6a8b101045b8ffd",
+   "rev": "a602d13aca2913724c7d47b2d7df0353620c4ee8",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.52",
+   "inputRev": "v0.0.53",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "56a2c80b209c253e0281ac4562a92122b457dcc0",
+   "rev": "ec060e0e10c685be8af65f288e23d026c9fde245",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "95561f7a5811fae6a309e4a1bbe22a0a4a98bf03",
+   "rev": "d892d7a88ad0ccf748fb8e651308ccd13426ba73",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "efcc7d9bd9936ecdc625baf0d033b60866565cd5",
+   "rev": "092b30de8e7ee78e96b24c235d99e26f2942d77e",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "e7fd1a415c80985ade02a021172834ca2139b0ca",
+   "rev": "dd423cf2b153b5b14cb017ee4beae788565a3925",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

test/Mathlib/lakefile.toml

@@ -4,7 +4,7 @@ defaultTargets = ["ReplMathlibTests"]
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4"
-rev = "v4.17.0"
+rev = "v4.18.0-rc1"
 
 [[lean_lib]]
 name = "ReplMathlibTests"

test/Mathlib/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.17.0
+leanprover/lean4:v4.18.0-rc1

test/enableInitializersExecution.expected.out

@@ -19,19 +19,19 @@
 {"proofState": 4, "goals": []}
 
 {"traces":
- ["[Meta.Tactic.simp.rewrite] of_eq_true (eq_true h0):1000, x > 0 ==> True"],
+ ["[Meta.Tactic.simp.rewrite] of_eq_true (eq_true h0):1000:\n      x > 0\n    ==>\n      True"],
  "proofState": 5,
  "goals": []}
 
 {"traces":
- ["[Meta.Tactic.simp.rewrite] gt_iff_lt:1000, x > 0 ==> 0 < x",
-  "[Meta.Tactic.simp.rewrite] h0:1000, 0 < x ==> True"],
+ ["[Meta.Tactic.simp.rewrite] gt_iff_lt:1000:\n      x > 0\n    ==>\n      0 < x",
+  "[Meta.Tactic.simp.rewrite] h0:1000:\n      0 < x\n    ==>\n      True"],
  "proofState": 6,
  "goals": []}
 
 {"traces":
- ["[Meta.Tactic.simp.rewrite] gt_iff_lt:1000, x > 0 ==> 0 < x",
-  "[Meta.Tactic.simp.rewrite] h0:1000, 0 < x ==> True"],
+ ["[Meta.Tactic.simp.rewrite] gt_iff_lt:1000:\n      x > 0\n    ==>\n      0 < x",
+  "[Meta.Tactic.simp.rewrite] h0:1000:\n      0 < x\n    ==>\n      True"],
  "proofState": 7,
  "goals": []}
 

test/enableInitializersExecution.in

@@ -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:\n      f\n    ==>\n      37\n[Meta.Tactic.simp.rewrite] eq_self:1000: 37 = 37 ==> True"}],
  "env": 3}
 
 {"sorries":
@@ -27,8 +27,8 @@
 {"traces": ["37"], "proofState": 1, "goals": ["⊢ f = 37"]}
 
 {"traces":
- ["[Meta.Tactic.simp.rewrite] f_def:1000, f ==> 37",
-  "[Meta.Tactic.simp.rewrite] eq_self:1000, 37 = 37 ==> True"],
+ ["[Meta.Tactic.simp.rewrite] f_def:1000:\n      f\n    ==>\n      37",
+  "[Meta.Tactic.simp.rewrite] eq_self:1000:\n      37 = 37\n    ==>\n      True"],
  "proofState": 2,
  "goals": []}