Skip to content

Commit 7f7dc97

Browse files
mfornetclaude
mfornet
and
claude
committed
chore: upgrade Lean toolchain to v4.32.0
Bump the pinned Lean toolchain from v4.31.0 to v4.32.0 and move Mathlib to its matching v4.32.0 tag. All packages (interpreter, codelib, programs, verifier) build clean with no proof or API changes required; regenerated lake manifests accordingly. Also bump doc-gen4 to its v4.32.0-compatible commit and update the README Lean badge. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
1 parent 2eba201 commit 7f7dc97

14 files changed

Lines changed: 113 additions & 113 deletions

‎README.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
# Talos
22

3-
[![Lean](https://img.shields.io/badge/Lean-v4.31.0-blue?logo=lean)](lean-toolchain)
3+
[![Lean](https://img.shields.io/badge/Lean-v4.32.0-blue?logo=lean)](lean-toolchain)
44
[![Telegram](https://img.shields.io/badge/Telegram-Join%20the%20discussion-2CA5E0?logo=telegram&logoColor=white)](https://t.me/TalosDev)
55

66
**Talos** is a WebAssembly interpreter written in Lean 4, named after the bronze giant of Greek mythology who guarded Crete — a mechanical guardian, built to enforce rules.

‎codelib/lake-manifest.json‎

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -12,17 +12,17 @@
1212
"type": "git",
1313
"subDir": null,
1414
"scope": "leanprover-community",
15-
"rev": "fabf563a7c95a166b8d7b6efca11c8b4dc9d911f",
15+
"rev": "81a5d257c8e410db227a6665ed08f64fea08e997",
1616
"name": "mathlib",
1717
"manifestFile": "lake-manifest.json",
18-
"inputRev": "v4.31.0",
18+
"inputRev": "v4.32.0",
1919
"inherited": true,
2020
"configFile": "lakefile.lean"},
2121
{"url": "https://github.com/leanprover-community/plausible",
2222
"type": "git",
2323
"subDir": null,
2424
"scope": "leanprover-community",
25-
"rev": "63045536fe95024e6c18fc7b48e03f506701c5bc",
25+
"rev": "e12c1910fe855cbfc38803cd4e55543906d5fa62",
2626
"name": "plausible",
2727
"manifestFile": "lake-manifest.json",
2828
"inputRev": "main",
@@ -42,7 +42,7 @@
4242
"type": "git",
4343
"subDir": null,
4444
"scope": "leanprover-community",
45-
"rev": "5c7542ed018c78194f1e2b903eaf6a792b74c03d",
45+
"rev": "7e9612bf0b9ee66db3cb5b9988a35afc706f5a12",
4646
"name": "importGraph",
4747
"manifestFile": "lake-manifest.json",
4848
"inputRev": "main",
@@ -52,7 +52,7 @@
5252
"type": "git",
5353
"subDir": null,
5454
"scope": "leanprover-community",
55-
"rev": "24b0d9dc081c5423f8eec7e866c441e5184f29d9",
55+
"rev": "6e311e2a844da9b2cc3971187df2fe0066947b93",
5656
"name": "proofwidgets",
5757
"manifestFile": "lake-manifest.json",
5858
"inputRev": "main",
@@ -62,7 +62,7 @@
6262
"type": "git",
6363
"subDir": null,
6464
"scope": "leanprover-community",
65-
"rev": "e3cb2f741431ce31bf73549fb52316a57368b06f",
65+
"rev": "a7dbf0c63b694e47f425f3dcddbc0e178bb432d3",
6666
"name": "aesop",
6767
"manifestFile": "lake-manifest.json",
6868
"inputRev": "master",
@@ -72,7 +72,7 @@
7272
"type": "git",
7373
"subDir": null,
7474
"scope": "leanprover-community",
75-
"rev": "f46324995fca5f0483b742e4eb4daec7f4ee50d2",
75+
"rev": "38d591e778f100aec9762bb582f9c7f55f50e9dc",
7676
"name": "Qq",
7777
"manifestFile": "lake-manifest.json",
7878
"inputRev": "master",
@@ -82,7 +82,7 @@
8282
"type": "git",
8383
"subDir": null,
8484
"scope": "leanprover-community",
85-
"rev": "fa08db58b30eb033edcdab331bba000827f9f785",
85+
"rev": "023ce7d62a0531e22a5331e20b587817a80d49ff",
8686
"name": "batteries",
8787
"manifestFile": "lake-manifest.json",
8888
"inputRev": "main",
@@ -92,10 +92,10 @@
9292
"type": "git",
9393
"subDir": null,
9494
"scope": "leanprover",
95-
"rev": "92564e5770e4d09f2d86dfbf8ada1e9c715b384c",
95+
"rev": "88679d088c9720c27ebdf2ba4dafe17341747f94",
9696
"name": "Cli",
9797
"manifestFile": "lake-manifest.json",
98-
"inputRev": "v4.31.0",
98+
"inputRev": "v4.32.0",
9999
"inherited": true,
100100
"configFile": "lakefile.toml"}],
101101
"name": "CodeLib",

‎codelib/lean-toolchain‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
leanprover/lean4:v4.31.0
1+
leanprover/lean4:v4.32.0

‎docbuild/lake-manifest.json‎

Lines changed: 64 additions & 64 deletions
Original file line numberDiff line numberDiff line change
@@ -12,10 +12,10 @@
1212
"type": "git",
1313
"subDir": null,
1414
"scope": "leanprover",
15-
"rev": "689fdeecf45e08cc048214680d40cfe2491be78b",
15+
"rev": "092d6318789e7bb9160ade1e85bdbcc0abfd7f6e",
1616
"name": "«doc-gen4»",
1717
"manifestFile": "lake-manifest.json",
18-
"inputRev": "689fdeecf45e08cc048214680d40cfe2491be78b",
18+
"inputRev": "092d6318789e7bb9160ade1e85bdbcc0abfd7f6e",
1919
"inherited": false,
2020
"configFile": "lakefile.lean"},
2121
{"type": "path",
@@ -25,6 +25,56 @@
2525
"inherited": true,
2626
"dir": "../programs/lean/../../codelib",
2727
"configFile": "lakefile.toml"},
28+
{"url": "https://github.com/leanprover/leansqlite",
29+
"type": "git",
30+
"subDir": null,
31+
"scope": "",
32+
"rev": "b2e8105c3507d81adaa531fda5990d14b631528f",
33+
"name": "leansqlite",
34+
"manifestFile": "lake-manifest.json",
35+
"inputRev": "main",
36+
"inherited": true,
37+
"configFile": "lakefile.lean"},
38+
{"url": "https://github.com/leanprover/lean4-cli",
39+
"type": "git",
40+
"subDir": null,
41+
"scope": "leanprover",
42+
"rev": "88679d088c9720c27ebdf2ba4dafe17341747f94",
43+
"name": "Cli",
44+
"manifestFile": "lake-manifest.json",
45+
"inputRev": "v4.32.0",
46+
"inherited": true,
47+
"configFile": "lakefile.toml"},
48+
{"url": "https://github.com/fgdorais/lean4-unicode-basic",
49+
"type": "git",
50+
"subDir": null,
51+
"scope": "",
52+
"rev": "947120c17904da8fc89abe3616d57e1c3e13aa9c",
53+
"name": "UnicodeBasic",
54+
"manifestFile": "lake-manifest.json",
55+
"inputRev": "main",
56+
"inherited": true,
57+
"configFile": "lakefile.lean"},
58+
{"url": "https://github.com/dupuisf/BibtexQuery",
59+
"type": "git",
60+
"subDir": null,
61+
"scope": "",
62+
"rev": "b648facb6be09a29be636bbc02d28ddee77565c7",
63+
"name": "BibtexQuery",
64+
"manifestFile": "lake-manifest.json",
65+
"inputRev": "master",
66+
"inherited": true,
67+
"configFile": "lakefile.toml"},
68+
{"url": "https://github.com/acmepjz/md4lean",
69+
"type": "git",
70+
"subDir": null,
71+
"scope": "",
72+
"rev": "31907cc18f48a95384f99cee5582c00fb39e0f67",
73+
"name": "MD4Lean",
74+
"manifestFile": "lake-manifest.json",
75+
"inputRev": "main",
76+
"inherited": true,
77+
"configFile": "lakefile.lean"},
2878
{"type": "path",
2979
"scope": "",
3080
"name": "WasmInterpreterLean",
@@ -36,17 +86,17 @@
3686
"type": "git",
3787
"subDir": null,
3888
"scope": "leanprover-community",
39-
"rev": "c5ea00351c28e24afc9f0f84379aa41082b1188f",
89+
"rev": "81a5d257c8e410db227a6665ed08f64fea08e997",
4090
"name": "mathlib",
4191
"manifestFile": "lake-manifest.json",
42-
"inputRev": "v4.30.0",
92+
"inputRev": "v4.32.0",
4393
"inherited": true,
4494
"configFile": "lakefile.lean"},
4595
{"url": "https://github.com/leanprover-community/plausible",
4696
"type": "git",
4797
"subDir": null,
4898
"scope": "leanprover-community",
49-
"rev": "a456461b368b71d2accd95234832cd9c174b5437",
99+
"rev": "e12c1910fe855cbfc38803cd4e55543906d5fa62",
50100
"name": "plausible",
51101
"manifestFile": "lake-manifest.json",
52102
"inputRev": "main",
@@ -66,7 +116,7 @@
66116
"type": "git",
67117
"subDir": null,
68118
"scope": "leanprover-community",
69-
"rev": "515cf9d0c00ece5e661f6de4326a53dedc1e8ea1",
119+
"rev": "7e9612bf0b9ee66db3cb5b9988a35afc706f5a12",
70120
"name": "importGraph",
71121
"manifestFile": "lake-manifest.json",
72122
"inputRev": "main",
@@ -76,92 +126,42 @@
76126
"type": "git",
77127
"subDir": null,
78128
"scope": "leanprover-community",
79-
"rev": "a84b3e2475d5c5ab979567b1ad8aea21b764bcf8",
129+
"rev": "6e311e2a844da9b2cc3971187df2fe0066947b93",
80130
"name": "proofwidgets",
81131
"manifestFile": "lake-manifest.json",
82-
"inputRev": "v0.0.99",
132+
"inputRev": "main",
83133
"inherited": true,
84134
"configFile": "lakefile.lean"},
85135
{"url": "https://github.com/leanprover-community/aesop",
86136
"type": "git",
87137
"subDir": null,
88138
"scope": "leanprover-community",
89-
"rev": "558915ae105bfd8074e22d597613d1961822adc2",
139+
"rev": "a7dbf0c63b694e47f425f3dcddbc0e178bb432d3",
90140
"name": "aesop",
91141
"manifestFile": "lake-manifest.json",
92-
"inputRev": "v4.30.0",
142+
"inputRev": "master",
93143
"inherited": true,
94144
"configFile": "lakefile.toml"},
95145
{"url": "https://github.com/leanprover-community/quote4",
96146
"type": "git",
97147
"subDir": null,
98148
"scope": "leanprover-community",
99-
"rev": "a6e6c34c4ef182f83b219a3a5a385f51f44bdc4c",
149+
"rev": "38d591e778f100aec9762bb582f9c7f55f50e9dc",
100150
"name": "Qq",
101151
"manifestFile": "lake-manifest.json",
102-
"inputRev": "v4.30.0",
152+
"inputRev": "master",
103153
"inherited": true,
104154
"configFile": "lakefile.toml"},
105155
{"url": "https://github.com/leanprover-community/batteries",
106156
"type": "git",
107157
"subDir": null,
108158
"scope": "leanprover-community",
109-
"rev": "32dc18cde3684679f3c003de608743b57498c56f",
159+
"rev": "023ce7d62a0531e22a5331e20b587817a80d49ff",
110160
"name": "batteries",
111161
"manifestFile": "lake-manifest.json",
112162
"inputRev": "main",
113163
"inherited": true,
114-
"configFile": "lakefile.toml"},
115-
{"url": "https://github.com/leanprover/lean4-cli",
116-
"type": "git",
117-
"subDir": null,
118-
"scope": "leanprover",
119-
"rev": "6b907cf12b2e445ccb7c24bc208ef04a1f39e84c",
120-
"name": "Cli",
121-
"manifestFile": "lake-manifest.json",
122-
"inputRev": "v4.30.0",
123-
"inherited": true,
124-
"configFile": "lakefile.toml"},
125-
{"url": "https://github.com/leanprover/leansqlite",
126-
"type": "git",
127-
"subDir": null,
128-
"scope": "",
129-
"rev": "a1d21d8b5f230205bb04c3bff479383f66802c0b",
130-
"name": "leansqlite",
131-
"manifestFile": "lake-manifest.json",
132-
"inputRev": "main",
133-
"inherited": true,
134-
"configFile": "lakefile.lean"},
135-
{"url": "https://github.com/fgdorais/lean4-unicode-basic",
136-
"type": "git",
137-
"subDir": null,
138-
"scope": "",
139-
"rev": "f8c99ff779ec217063545b3b191747c92e7fbfb3",
140-
"name": "UnicodeBasic",
141-
"manifestFile": "lake-manifest.json",
142-
"inputRev": "main",
143-
"inherited": true,
144-
"configFile": "lakefile.lean"},
145-
{"url": "https://github.com/dupuisf/BibtexQuery",
146-
"type": "git",
147-
"subDir": null,
148-
"scope": "",
149-
"rev": "5d31b64fb703c5d77f6ef4d1fb958f9bdf1ea539",
150-
"name": "BibtexQuery",
151-
"manifestFile": "lake-manifest.json",
152-
"inputRev": "nightly-testing",
153-
"inherited": true,
154-
"configFile": "lakefile.toml"},
155-
{"url": "https://github.com/acmepjz/md4lean",
156-
"type": "git",
157-
"subDir": null,
158-
"scope": "",
159-
"rev": "6a3fb240133bcb7e1a066fdc784b3fdc304e3fc5",
160-
"name": "MD4Lean",
161-
"manifestFile": "lake-manifest.json",
162-
"inputRev": "main",
163-
"inherited": true,
164-
"configFile": "lakefile.lean"}],
164+
"configFile": "lakefile.toml"}],
165165
"name": "docbuild",
166166
"lakeDir": ".lake",
167167
"fixedToolchain": false}

‎docbuild/lakefile.toml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ packagesDir = "../.lake/packages"
66
[[require]]
77
scope = "leanprover"
88
name = "«doc-gen4»"
9-
rev = "689fdeecf45e08cc048214680d40cfe2491be78b"
9+
rev = "092d6318789e7bb9160ade1e85bdbcc0abfd7f6e"
1010

1111
[[require]]
1212
name = "Project"

‎docbuild/lean-toolchain‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
leanprover/lean4:v4.31.0
1+
leanprover/lean4:v4.32.0

‎interpreter/lake-manifest.json‎

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -5,17 +5,17 @@
55
"type": "git",
66
"subDir": null,
77
"scope": "leanprover-community",
8-
"rev": "fabf563a7c95a166b8d7b6efca11c8b4dc9d911f",
8+
"rev": "81a5d257c8e410db227a6665ed08f64fea08e997",
99
"name": "mathlib",
1010
"manifestFile": "lake-manifest.json",
11-
"inputRev": "v4.31.0",
11+
"inputRev": "v4.32.0",
1212
"inherited": false,
1313
"configFile": "lakefile.lean"},
1414
{"url": "https://github.com/leanprover-community/plausible",
1515
"type": "git",
1616
"subDir": null,
1717
"scope": "leanprover-community",
18-
"rev": "63045536fe95024e6c18fc7b48e03f506701c5bc",
18+
"rev": "e12c1910fe855cbfc38803cd4e55543906d5fa62",
1919
"name": "plausible",
2020
"manifestFile": "lake-manifest.json",
2121
"inputRev": "main",
@@ -35,7 +35,7 @@
3535
"type": "git",
3636
"subDir": null,
3737
"scope": "leanprover-community",
38-
"rev": "5c7542ed018c78194f1e2b903eaf6a792b74c03d",
38+
"rev": "7e9612bf0b9ee66db3cb5b9988a35afc706f5a12",
3939
"name": "importGraph",
4040
"manifestFile": "lake-manifest.json",
4141
"inputRev": "main",
@@ -45,7 +45,7 @@
4545
"type": "git",
4646
"subDir": null,
4747
"scope": "leanprover-community",
48-
"rev": "24b0d9dc081c5423f8eec7e866c441e5184f29d9",
48+
"rev": "6e311e2a844da9b2cc3971187df2fe0066947b93",
4949
"name": "proofwidgets",
5050
"manifestFile": "lake-manifest.json",
5151
"inputRev": "main",
@@ -55,7 +55,7 @@
5555
"type": "git",
5656
"subDir": null,
5757
"scope": "leanprover-community",
58-
"rev": "e3cb2f741431ce31bf73549fb52316a57368b06f",
58+
"rev": "a7dbf0c63b694e47f425f3dcddbc0e178bb432d3",
5959
"name": "aesop",
6060
"manifestFile": "lake-manifest.json",
6161
"inputRev": "master",
@@ -65,7 +65,7 @@
6565
"type": "git",
6666
"subDir": null,
6767
"scope": "leanprover-community",
68-
"rev": "f46324995fca5f0483b742e4eb4daec7f4ee50d2",
68+
"rev": "38d591e778f100aec9762bb582f9c7f55f50e9dc",
6969
"name": "Qq",
7070
"manifestFile": "lake-manifest.json",
7171
"inputRev": "master",
@@ -75,7 +75,7 @@
7575
"type": "git",
7676
"subDir": null,
7777
"scope": "leanprover-community",
78-
"rev": "fa08db58b30eb033edcdab331bba000827f9f785",
78+
"rev": "023ce7d62a0531e22a5331e20b587817a80d49ff",
7979
"name": "batteries",
8080
"manifestFile": "lake-manifest.json",
8181
"inputRev": "main",
@@ -85,10 +85,10 @@
8585
"type": "git",
8686
"subDir": null,
8787
"scope": "leanprover",
88-
"rev": "92564e5770e4d09f2d86dfbf8ada1e9c715b384c",
88+
"rev": "88679d088c9720c27ebdf2ba4dafe17341747f94",
8989
"name": "Cli",
9090
"manifestFile": "lake-manifest.json",
91-
"inputRev": "v4.31.0",
91+
"inputRev": "v4.32.0",
9292
"inherited": true,
9393
"configFile": "lakefile.toml"}],
9494
"name": "Interpreter",

‎interpreter/lakefile.toml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ packagesDir = "../.lake/packages"
66
[[require]]
77
name = "mathlib"
88
scope = "leanprover-community"
9-
rev = "v4.31.0"
9+
rev = "v4.32.0"
1010

1111
[[lean_lib]]
1212
name = "Interpreter"

‎interpreter/lean-toolchain‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
leanprover/lean4:v4.31.0
1+
leanprover/lean4:v4.32.0

‎lean-toolchain‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
leanprover/lean4:v4.31.0
1+
leanprover/lean4:v4.32.0

0 commit comments

Comments
 (0)