update for v4.3.0-rc2

.gitignore

@@ -1,5 +1,7 @@
 /build
 /lake-packages/*
 /lakefile.olean
+/.lake
+/test/Mathlib/.lake
 /test/*.olean
 /test/*.olean.tmp

README.md

@@ -64,13 +64,13 @@ and then using the `proofState` index returned for each `sorry`.
 
 Example usage:
 ```json
-{"cmd" : "def f : Nat := by sorry"}
+{"cmd" : "def f (x : Unit) : Nat := by sorry"}
 
 {"sorries":
  [{"proofState": 0,
-   "pos": {"line": 1, "column": 18},
-   "goal": "⊢ Nat",
-   "endPos": {"line": 1, "column": 23}}],
+   "pos": {"line": 1, "column": 29},
+   "goal": "x : Unit ⊢ Nat",
+   "endPos": {"line": 1, "column": 34}}],
  "messages":
  [{"severity": "warning",
    "pos": {"line": 1, "column": 4},
@@ -80,7 +80,7 @@ Example usage:
 
 {"tactic": "apply Int.natAbs", "proofState": 0}
 
-{"proofState": 1, "goals": ["⊢ Int"]}
+{"proofState": 1, "goals": ["x : Unit\n⊢ Int"]}
 
 {"tactic": "exact -37", "proofState": 1}
 

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.2.0-rc4
+leanprover/lean4:v4.3.0-rc2

test/Mathlib/lake-manifest.json

@@ -1,52 +1,59 @@
-{"version": 6,
- "packagesDir": "lake-packages",
+{"version": 7,
+ "packagesDir": ".lake/packages",
  "packages":
- [{"git":
-   {"url": "https://github.com/leanprover-community/mathlib4",
-    "subDir?": null,
-    "rev": "1a79f4b2854dea6dc7a133543f0a140d4138cc58",
-    "opts": {},
-    "name": "mathlib",
-    "inputRev?": "master",
-    "inherited": false}},
-  {"git":
-   {"url": "https://github.com/leanprover/std4",
-    "subDir?": null,
-    "rev": "fb56324020c8e4f3d451e8901b290dea82c072ae",
-    "opts": {},
-    "name": "std",
-    "inputRev?": "main",
-    "inherited": true}},
-  {"git":
-   {"url": "https://github.com/leanprover-community/quote4",
-    "subDir?": null,
-    "rev": "a387c0eb611857e2460cf97a8e861c944286e6b2",
-    "opts": {},
-    "name": "Qq",
-    "inputRev?": "master",
-    "inherited": true}},
-  {"git":
-   {"url": "https://github.com/leanprover-community/aesop",
-    "subDir?": null,
-    "rev": "9dc4a1097a690216eaa7cf2d2290efd447e60d7a",
-    "opts": {},
-    "name": "aesop",
-    "inputRev?": "master",
-    "inherited": true}},
-  {"git":
-   {"url": "https://github.com/leanprover/lean4-cli",
-    "subDir?": null,
-    "rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa",
-    "opts": {},
-    "name": "Cli",
-    "inputRev?": "nightly",
-    "inherited": true}},
-  {"git":
-   {"url": "https://github.com/leanprover-community/ProofWidgets4",
-    "subDir?": null,
-    "rev": "5382e38eca1e2537d75d4c4705a9e744424b0037",
-    "opts": {},
-    "name": "proofwidgets",
-    "inputRev?": "v0.0.19",
-    "inherited": true}}],
- "name": "«repl-mathlib-tests»"}
+ [{"url": "https://github.com/leanprover/std4",
+   "type": "git",
+   "subDir": null,
+   "rev": "e403f680f0beb8610c29e6f799132e8be880554e",
+   "name": "std",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "rev": "d3a1d25f3eba0d93a58d5d3d027ffa78ece07755",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "rev": "bf5ab42a58e71de7ebad399ce3f90d29aae7fca9",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "rev": "909febc72b4f64628f8d35cd0554f8a90b6e0749",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.23",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/mathlib4",
+   "type": "git",
+   "subDir": null,
+   "rev": "5be6ac521cc1dbd9c3f2b9424e1d09d8726764bb",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
+ "name": "«repl-mathlib-tests»",
+ "lakeDir": ".lake"}

test/Mathlib/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.2.0-rc4
+leanprover/lean4:v4.3.0-rc2

test/Mathlib/test.sh

@@ -23,7 +23,7 @@ for infile in $IN_DIR/*.in; do
 
     # Run the command and store its output in a temporary file
     tmpfile=$(mktemp)
-    lake env ../../build/bin/repl < "$infile" > "$tmpfile" 2>&1
+    lake env ../../.lake/build/bin/repl < "$infile" > "$tmpfile" 2>&1
 
     # Compare the output with the expected output
     if diff "$tmpfile" "$expectedfile"; then

test/Mathlib/test/H20231020.in

@@ -1,8 +1,8 @@
-{"cmd": "import Mathlib.Algebra.BigOperators.Basic\nimport Mathlib.Data.Real.Basic\nimport Mathlib.Data.Complex.Basic\nimport Mathlib.Data.Nat.Log\nimport Mathlib.Data.Complex.Exponential\nimport Mathlib.NumberTheory.Divisors\nimport Mathlib.Data.ZMod.Defs\nimport Mathlib.Data.ZMod.Basic\nimport Mathlib.Topology.Basic\nimport Mathlib.Data.Nat.Digits\nopen BigOperators\nopen Real\nopen Nat\nopen Topology"}
+{"cmd": "import Mathlib.Algebra.BigOperators.Basic\nimport Mathlib.Data.Real.Basic\nimport Mathlib.Data.Complex.Basic\nimport Mathlib.Data.Nat.Log\nimport Mathlib.Data.Complex.Exponential\nimport Mathlib.NumberTheory.Divisors\nimport Mathlib.Data.ZMod.Defs\nimport Mathlib.Data.ZMod.Basic\nimport Mathlib.Topology.Basic\nimport Mathlib.Data.Nat.Digits\nimport Mathlib.Tactic.NormNum.GCD\nopen BigOperators\nopen Real\nopen Nat\nopen Topology"}
 
 {"cmd": "theorem mathd_numbertheory_188 : Nat.gcd 180 168 = 12 := by norm_num", "env": 0}
 
-{"cmd": "theorem mathd_numbertheory_403 : ∑ k in (Nat.properDivisors 198), k = 270 := by simp", "env": 0}
+{"cmd": "theorem mathd_numbertheory_403 : ∑ k in (Nat.properDivisors 198), k = 270 := by simp (config := {decide := true})", "env": 0}
 
-{"cmd": "theorem mathd_numbertheory_109 (v : ℕ → ℕ) (h₀ : ∀ n, v n = 2 * n - 1) : (∑ k in Finset.Icc 1 100, v k) % 7 = 4 := by simp_rw [h₀]", "env": 0}
+{"cmd": "theorem mathd_numbertheory_109 (v : ℕ → ℕ) (h₀ : ∀ n, v n = 2 * n - 1) : (∑ k in Finset.Icc 1 100, v k) % 7 = 4 := by simp_rw (config := {decide := true}) [h₀]", "env": 0}
 

test/Mathlib/test/H20231020.lean

@@ -0,0 +1,22 @@
+import Mathlib.Algebra.BigOperators.Basic
+import Mathlib.Data.Real.Basic
+import Mathlib.Data.Complex.Basic
+import Mathlib.Data.Nat.Log
+import Mathlib.Data.Complex.Exponential
+import Mathlib.NumberTheory.Divisors
+import Mathlib.Data.ZMod.Defs
+import Mathlib.Data.ZMod.Basic
+import Mathlib.Topology.Basic
+import Mathlib.Data.Nat.Digits
+import Mathlib.Tactic.NormNum.GCD
+
+open BigOperators
+open Real
+open Nat
+open Topology
+
+theorem mathd_numbertheory_188 : Nat.gcd 180 168 = 12 := by norm_num
+
+theorem mathd_numbertheory_403 : ∑ k in (Nat.properDivisors 198), k = 270 := by simp (config := {decide := true})
+
+theorem mathd_numbertheory_109 (v : ℕ → ℕ) (h₀ : ∀ n, v n = 2 * n - 1) : (∑ k in Finset.Icc 1 100, v k) % 7 = 4 := by simp_rw (config := {decide := true}) [h₀]

test/readme.expected.out

@@ -0,0 +1,16 @@
+{"sorries":
+ [{"proofState": 0,
+   "pos": {"line": 1, "column": 29},
+   "goal": "x : Unit ⊢ Nat",
+   "endPos": {"line": 1, "column": 34}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 4},
+   "endPos": {"line": 1, "column": 5},
+   "data": "declaration uses 'sorry'"}],
+ "env": 0}
+
+{"proofState": 1, "goals": ["x : Unit\n⊢ Int"]}
+
+{"proofState": 2, "goals": []}
+

test/readme.in

@@ -0,0 +1,5 @@
+{"cmd" : "def f (x : Unit) : Nat := by sorry"}
+
+{"tactic": "apply Int.natAbs", "proofState": 0}
+
+{"tactic": "exact -37", "proofState": 1}