Skip to content

Commit 5b7e0d4

Browse files
kim-emkim-em
committed
update for v4.3.0-rc2
1 parent 53aa3e5 commit 5b7e0d4

10 files changed

+114
-62
lines changed

‎.gitignore

+2
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,7 @@
11
/build
22
/lake-packages/*
33
/lakefile.olean
4+
/.lake
5+
/test/Mathlib/.lake
46
/test/*.olean
57
/test/*.olean.tmp

‎README.md

+5-5
Original file line numberDiff line numberDiff line change
@@ -64,13 +64,13 @@ and then using the `proofState` index returned for each `sorry`.
6464

6565
Example usage:
6666
```json
67-
{"cmd" : "def f : Nat := by sorry"}
67+
{"cmd" : "def f (x : Unit) : Nat := by sorry"}
6868

6969
{"sorries":
7070
[{"proofState": 0,
71-
"pos": {"line": 1, "column": 18},
72-
"goal": "⊢ Nat",
73-
"endPos": {"line": 1, "column": 23}}],
71+
"pos": {"line": 1, "column": 29},
72+
"goal": "x : Unit ⊢ Nat",
73+
"endPos": {"line": 1, "column": 34}}],
7474
"messages":
7575
[{"severity": "warning",
7676
"pos": {"line": 1, "column": 4},
@@ -80,7 +80,7 @@ Example usage:
8080

8181
{"tactic": "apply Int.natAbs", "proofState": 0}
8282

83-
{"proofState": 1, "goals": ["⊢ Int"]}
83+
{"proofState": 1, "goals": ["x : Unit\n⊢ Int"]}
8484

8585
{"tactic": "exact -37", "proofState": 1}
8686

‎lean-toolchain

+1-1
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
leanprover/lean4:v4.2.0-rc4
1+
leanprover/lean4:v4.3.0-rc2

‎test/Mathlib/lake-manifest.json

+58-51
Original file line numberDiff line numberDiff line change
@@ -1,52 +1,59 @@
1-
{"version": 6,
2-
"packagesDir": "lake-packages",
1+
{"version": 7,
2+
"packagesDir": ".lake/packages",
33
"packages":
4-
[{"git":
5-
{"url": "https://github.com/leanprover-community/mathlib4",
6-
"subDir?": null,
7-
"rev": "1a79f4b2854dea6dc7a133543f0a140d4138cc58",
8-
"opts": {},
9-
"name": "mathlib",
10-
"inputRev?": "master",
11-
"inherited": false}},
12-
{"git":
13-
{"url": "https://github.com/leanprover/std4",
14-
"subDir?": null,
15-
"rev": "fb56324020c8e4f3d451e8901b290dea82c072ae",
16-
"opts": {},
17-
"name": "std",
18-
"inputRev?": "main",
19-
"inherited": true}},
20-
{"git":
21-
{"url": "https://github.com/leanprover-community/quote4",
22-
"subDir?": null,
23-
"rev": "a387c0eb611857e2460cf97a8e861c944286e6b2",
24-
"opts": {},
25-
"name": "Qq",
26-
"inputRev?": "master",
27-
"inherited": true}},
28-
{"git":
29-
{"url": "https://github.com/leanprover-community/aesop",
30-
"subDir?": null,
31-
"rev": "9dc4a1097a690216eaa7cf2d2290efd447e60d7a",
32-
"opts": {},
33-
"name": "aesop",
34-
"inputRev?": "master",
35-
"inherited": true}},
36-
{"git":
37-
{"url": "https://github.com/leanprover/lean4-cli",
38-
"subDir?": null,
39-
"rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa",
40-
"opts": {},
41-
"name": "Cli",
42-
"inputRev?": "nightly",
43-
"inherited": true}},
44-
{"git":
45-
{"url": "https://github.com/leanprover-community/ProofWidgets4",
46-
"subDir?": null,
47-
"rev": "5382e38eca1e2537d75d4c4705a9e744424b0037",
48-
"opts": {},
49-
"name": "proofwidgets",
50-
"inputRev?": "v0.0.19",
51-
"inherited": true}}],
52-
"name": "«repl-mathlib-tests»"}
4+
[{"url": "https://github.com/leanprover/std4",
5+
"type": "git",
6+
"subDir": null,
7+
"rev": "e403f680f0beb8610c29e6f799132e8be880554e",
8+
"name": "std",
9+
"manifestFile": "lake-manifest.json",
10+
"inputRev": "main",
11+
"inherited": true,
12+
"configFile": "lakefile.lean"},
13+
{"url": "https://github.com/leanprover-community/quote4",
14+
"type": "git",
15+
"subDir": null,
16+
"rev": "d3a1d25f3eba0d93a58d5d3d027ffa78ece07755",
17+
"name": "Qq",
18+
"manifestFile": "lake-manifest.json",
19+
"inputRev": "master",
20+
"inherited": true,
21+
"configFile": "lakefile.lean"},
22+
{"url": "https://github.com/leanprover-community/aesop",
23+
"type": "git",
24+
"subDir": null,
25+
"rev": "bf5ab42a58e71de7ebad399ce3f90d29aae7fca9",
26+
"name": "aesop",
27+
"manifestFile": "lake-manifest.json",
28+
"inputRev": "master",
29+
"inherited": true,
30+
"configFile": "lakefile.lean"},
31+
{"url": "https://github.com/leanprover-community/ProofWidgets4",
32+
"type": "git",
33+
"subDir": null,
34+
"rev": "909febc72b4f64628f8d35cd0554f8a90b6e0749",
35+
"name": "proofwidgets",
36+
"manifestFile": "lake-manifest.json",
37+
"inputRev": "v0.0.23",
38+
"inherited": true,
39+
"configFile": "lakefile.lean"},
40+
{"url": "https://github.com/leanprover/lean4-cli",
41+
"type": "git",
42+
"subDir": null,
43+
"rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec",
44+
"name": "Cli",
45+
"manifestFile": "lake-manifest.json",
46+
"inputRev": "main",
47+
"inherited": true,
48+
"configFile": "lakefile.lean"},
49+
{"url": "https://github.com/leanprover-community/mathlib4",
50+
"type": "git",
51+
"subDir": null,
52+
"rev": "5be6ac521cc1dbd9c3f2b9424e1d09d8726764bb",
53+
"name": "mathlib",
54+
"manifestFile": "lake-manifest.json",
55+
"inputRev": "master",
56+
"inherited": false,
57+
"configFile": "lakefile.lean"}],
58+
"name": "«repl-mathlib-tests»",
59+
"lakeDir": ".lake"}

‎test/Mathlib/lean-toolchain

+1-1
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
leanprover/lean4:v4.2.0-rc4
1+
leanprover/lean4:v4.3.0-rc2

‎test/Mathlib/test.sh

+1-1
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ for infile in $IN_DIR/*.in; do
2323

2424
# Run the command and store its output in a temporary file
2525
tmpfile=$(mktemp)
26-
lake env ../../build/bin/repl < "$infile" > "$tmpfile" 2>&1
26+
lake env ../../.lake/build/bin/repl < "$infile" > "$tmpfile" 2>&1
2727

2828
# Compare the output with the expected output
2929
if diff "$tmpfile" "$expectedfile"; then

‎test/Mathlib/test/H20231020.in

+3-3
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
1-
{"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"}
1+
{"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"}
22

33
{"cmd": "theorem mathd_numbertheory_188 : Nat.gcd 180 168 = 12 := by norm_num", "env": 0}
44

5-
{"cmd": "theorem mathd_numbertheory_403 : ∑ k in (Nat.properDivisors 198), k = 270 := by simp", "env": 0}
5+
{"cmd": "theorem mathd_numbertheory_403 : ∑ k in (Nat.properDivisors 198), k = 270 := by simp (config := {decide := true})", "env": 0}
66

7-
{"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}
7+
{"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}
88

‎test/Mathlib/test/H20231020.lean

+22
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
import Mathlib.Algebra.BigOperators.Basic
2+
import Mathlib.Data.Real.Basic
3+
import Mathlib.Data.Complex.Basic
4+
import Mathlib.Data.Nat.Log
5+
import Mathlib.Data.Complex.Exponential
6+
import Mathlib.NumberTheory.Divisors
7+
import Mathlib.Data.ZMod.Defs
8+
import Mathlib.Data.ZMod.Basic
9+
import Mathlib.Topology.Basic
10+
import Mathlib.Data.Nat.Digits
11+
import Mathlib.Tactic.NormNum.GCD
12+
13+
open BigOperators
14+
open Real
15+
open Nat
16+
open Topology
17+
18+
theorem mathd_numbertheory_188 : Nat.gcd 180 168 = 12 := by norm_num
19+
20+
theorem mathd_numbertheory_403 : ∑ k in (Nat.properDivisors 198), k = 270 := by simp (config := {decide := true})
21+
22+
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

+16
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
{"sorries":
2+
[{"proofState": 0,
3+
"pos": {"line": 1, "column": 29},
4+
"goal": "x : Unit ⊢ Nat",
5+
"endPos": {"line": 1, "column": 34}}],
6+
"messages":
7+
[{"severity": "warning",
8+
"pos": {"line": 1, "column": 4},
9+
"endPos": {"line": 1, "column": 5},
10+
"data": "declaration uses 'sorry'"}],
11+
"env": 0}
12+
13+
{"proofState": 1, "goals": ["x : Unit\n⊢ Int"]}
14+
15+
{"proofState": 2, "goals": []}
16+

‎test/readme.in

+5
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
{"cmd" : "def f (x : Unit) : Nat := by sorry"}
2+
3+
{"tactic": "apply Int.natAbs", "proofState": 0}
4+
5+
{"tactic": "exact -37", "proofState": 1}

0 commit comments

Comments
 (0)