Skip to content

Commit 74693cf

Browse files
justincasherjustincasher
authored
Merge pull request #65 from justincasher/track-lean-workspaces
Track Lean package workspaces in version control
2 parents e7b41b5 + b192aee commit 74693cf

20 files changed

+801
-6
lines changed

‎.gitignore‎

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -35,10 +35,4 @@ temp/
3535
# Generated files
3636
AGENTS.md
3737
CLAUDE.md
38-
# Per-package Lean workspaces (generated by extraction)
39-
lean/mathlib/
40-
lean/physlean/
41-
lean/flt/
42-
lean/formal-conjectures/
43-
lean/cslib/
4438
dist/

‎lean/cslib/CslibExtract.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
import Cslib

‎lean/cslib/lake-manifest.json‎

Lines changed: 145 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,145 @@
1+
{"version": "1.1.0",
2+
"packagesDir": ".lake/packages",
3+
"packages":
4+
[{"url": "https://github.com/leanprover/doc-gen4",
5+
"type": "git",
6+
"subDir": null,
7+
"scope": "",
8+
"rev": "7be6082d00bb0cfc1e136505dba7718cd5fcaa84",
9+
"name": "«doc-gen4»",
10+
"manifestFile": "lake-manifest.json",
11+
"inputRev": "v4.28.0-rc1",
12+
"inherited": false,
13+
"configFile": "lakefile.lean"},
14+
{"url": "https://github.com/leanprover/cslib",
15+
"type": "git",
16+
"subDir": null,
17+
"scope": "",
18+
"rev": "00d68a39497c0954bd52ca5237eea2aa152a5387",
19+
"name": "Cslib",
20+
"manifestFile": "lake-manifest.json",
21+
"inputRev": "main",
22+
"inherited": false,
23+
"configFile": "lakefile.toml"},
24+
{"url": "https://github.com/leanprover/lean4-cli",
25+
"type": "git",
26+
"subDir": null,
27+
"scope": "",
28+
"rev": "28e0856d4424863a85b18f38868c5420c55f9bae",
29+
"name": "Cli",
30+
"manifestFile": "lake-manifest.json",
31+
"inputRev": "main",
32+
"inherited": true,
33+
"configFile": "lakefile.toml"},
34+
{"url": "https://github.com/fgdorais/lean4-unicode-basic",
35+
"type": "git",
36+
"subDir": null,
37+
"scope": "",
38+
"rev": "8668e1ab7c987fb8ed1349f14c3b7b60bd5f27b6",
39+
"name": "UnicodeBasic",
40+
"manifestFile": "lake-manifest.json",
41+
"inputRev": "main",
42+
"inherited": true,
43+
"configFile": "lakefile.lean"},
44+
{"url": "https://github.com/dupuisf/BibtexQuery",
45+
"type": "git",
46+
"subDir": null,
47+
"scope": "",
48+
"rev": "1c5c543d2637aebf90c80aead2d401ae88db13cc",
49+
"name": "BibtexQuery",
50+
"manifestFile": "lake-manifest.json",
51+
"inputRev": "master",
52+
"inherited": true,
53+
"configFile": "lakefile.toml"},
54+
{"url": "https://github.com/acmepjz/md4lean",
55+
"type": "git",
56+
"subDir": null,
57+
"scope": "",
58+
"rev": "38ac5945d744903ffcc473ce1030223991b11cf6",
59+
"name": "MD4Lean",
60+
"manifestFile": "lake-manifest.json",
61+
"inputRev": "main",
62+
"inherited": true,
63+
"configFile": "lakefile.lean"},
64+
{"url": "https://github.com/leanprover-community/mathlib4",
65+
"type": "git",
66+
"subDir": null,
67+
"scope": "leanprover-community",
68+
"rev": "5352afccd6866369be9de43f5b7ec47203555f44",
69+
"name": "mathlib",
70+
"manifestFile": "lake-manifest.json",
71+
"inputRev": "v4.28.0-rc1",
72+
"inherited": true,
73+
"configFile": "lakefile.lean"},
74+
{"url": "https://github.com/leanprover-community/plausible",
75+
"type": "git",
76+
"subDir": null,
77+
"scope": "leanprover-community",
78+
"rev": "7311586e1a56af887b1081d05e80c11b6c41d212",
79+
"name": "plausible",
80+
"manifestFile": "lake-manifest.json",
81+
"inputRev": "main",
82+
"inherited": true,
83+
"configFile": "lakefile.toml"},
84+
{"url": "https://github.com/leanprover-community/LeanSearchClient",
85+
"type": "git",
86+
"subDir": null,
87+
"scope": "leanprover-community",
88+
"rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28",
89+
"name": "LeanSearchClient",
90+
"manifestFile": "lake-manifest.json",
91+
"inputRev": "main",
92+
"inherited": true,
93+
"configFile": "lakefile.toml"},
94+
{"url": "https://github.com/leanprover-community/import-graph",
95+
"type": "git",
96+
"subDir": null,
97+
"scope": "leanprover-community",
98+
"rev": "875ad9d88ed684e39c16bdea260e6ecfa15afd60",
99+
"name": "importGraph",
100+
"manifestFile": "lake-manifest.json",
101+
"inputRev": "main",
102+
"inherited": true,
103+
"configFile": "lakefile.toml"},
104+
{"url": "https://github.com/leanprover-community/ProofWidgets4",
105+
"type": "git",
106+
"subDir": null,
107+
"scope": "leanprover-community",
108+
"rev": "6d65c6e0a25b8a52c13c3adeb63ecde3bfbb6294",
109+
"name": "proofwidgets",
110+
"manifestFile": "lake-manifest.json",
111+
"inputRev": "v0.0.86",
112+
"inherited": true,
113+
"configFile": "lakefile.lean"},
114+
{"url": "https://github.com/leanprover-community/aesop",
115+
"type": "git",
116+
"subDir": null,
117+
"scope": "leanprover-community",
118+
"rev": "f08e838d4f9aea519f3cde06260cfb686fd4bab0",
119+
"name": "aesop",
120+
"manifestFile": "lake-manifest.json",
121+
"inputRev": "master",
122+
"inherited": true,
123+
"configFile": "lakefile.toml"},
124+
{"url": "https://github.com/leanprover-community/quote4",
125+
"type": "git",
126+
"subDir": null,
127+
"scope": "leanprover-community",
128+
"rev": "23324752757bf28124a518ec284044c8db79fee5",
129+
"name": "Qq",
130+
"manifestFile": "lake-manifest.json",
131+
"inputRev": "master",
132+
"inherited": true,
133+
"configFile": "lakefile.toml"},
134+
{"url": "https://github.com/leanprover-community/batteries",
135+
"type": "git",
136+
"subDir": null,
137+
"scope": "leanprover-community",
138+
"rev": "cabbb5a025bfbbc50af9184ed2dfdde6ea4f53a7",
139+
"name": "batteries",
140+
"manifestFile": "lake-manifest.json",
141+
"inputRev": "main",
142+
"inherited": true,
143+
"configFile": "lakefile.toml"}],
144+
"name": "«cslib-extractor»",
145+
"lakeDir": ".lake"}

‎lean/cslib/lakefile.lean‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
import Lake
2+
open Lake DSL
3+
4+
package «cslib-extractor» where
5+
-- Workspace for extracting cslib documentation
6+
7+
lean_lib «CslibExtract» where
8+
roots := #[`CslibExtract]
9+
10+
require Cslib from git
11+
"https://github.com/leanprover/cslib" @ "main"
12+
13+
require «doc-gen4» from git
14+
"https://github.com/leanprover/doc-gen4" @ "v4.28.0-rc1"

‎lean/cslib/lean-toolchain‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
leanprover/lean4:v4.28.0-rc1

‎lean/flt/FLTExtract.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
import FLT

‎lean/flt/lake-manifest.json‎

Lines changed: 155 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,155 @@
1+
{"version": "1.1.0",
2+
"packagesDir": ".lake/packages",
3+
"packages":
4+
[{"url": "https://github.com/leanprover/doc-gen4",
5+
"type": "git",
6+
"subDir": null,
7+
"scope": "",
8+
"rev": "01e143329f2f79abbb8559344e836c221ae84cfd",
9+
"name": "«doc-gen4»",
10+
"manifestFile": "lake-manifest.json",
11+
"inputRev": "v4.27.0",
12+
"inherited": false,
13+
"configFile": "lakefile.lean"},
14+
{"url": "https://github.com/ImperialCollegeLondon/FLT",
15+
"type": "git",
16+
"subDir": null,
17+
"scope": "",
18+
"rev": "782d8b962dd96be0c767b7b99e390e32c52ea583",
19+
"name": "FLT",
20+
"manifestFile": "lake-manifest.json",
21+
"inputRev": "main",
22+
"inherited": false,
23+
"configFile": "lakefile.toml"},
24+
{"url": "https://github.com/leanprover/lean4-cli",
25+
"type": "git",
26+
"subDir": null,
27+
"scope": "",
28+
"rev": "55c37290ff6186e2e965d68cf853a57c0702db82",
29+
"name": "Cli",
30+
"manifestFile": "lake-manifest.json",
31+
"inputRev": "main",
32+
"inherited": true,
33+
"configFile": "lakefile.toml"},
34+
{"url": "https://github.com/fgdorais/lean4-unicode-basic",
35+
"type": "git",
36+
"subDir": null,
37+
"scope": "",
38+
"rev": "b09d573cbacf5a8e767292e0edeec787a81689ce",
39+
"name": "UnicodeBasic",
40+
"manifestFile": "lake-manifest.json",
41+
"inputRev": "main",
42+
"inherited": true,
43+
"configFile": "lakefile.lean"},
44+
{"url": "https://github.com/dupuisf/BibtexQuery",
45+
"type": "git",
46+
"subDir": null,
47+
"scope": "",
48+
"rev": "c8a6a4dae7c7f42949a1058427a75c20447e990f",
49+
"name": "BibtexQuery",
50+
"manifestFile": "lake-manifest.json",
51+
"inputRev": "master",
52+
"inherited": true,
53+
"configFile": "lakefile.toml"},
54+
{"url": "https://github.com/acmepjz/md4lean",
55+
"type": "git",
56+
"subDir": null,
57+
"scope": "",
58+
"rev": "38ac5945d744903ffcc473ce1030223991b11cf6",
59+
"name": "MD4Lean",
60+
"manifestFile": "lake-manifest.json",
61+
"inputRev": "main",
62+
"inherited": true,
63+
"configFile": "lakefile.lean"},
64+
{"url": "https://github.com/PatrickMassot/checkdecls.git",
65+
"type": "git",
66+
"subDir": null,
67+
"scope": "",
68+
"rev": "3d425859e73fcfbef85b9638c2a91708ef4a22d4",
69+
"name": "checkdecls",
70+
"manifestFile": "lake-manifest.json",
71+
"inputRev": null,
72+
"inherited": true,
73+
"configFile": "lakefile.lean"},
74+
{"url": "https://github.com/leanprover-community/mathlib4.git",
75+
"type": "git",
76+
"subDir": null,
77+
"scope": "",
78+
"rev": "a3a10db0e9d66acbebf76c5e6a135066525ac900",
79+
"name": "mathlib",
80+
"manifestFile": "lake-manifest.json",
81+
"inputRev": null,
82+
"inherited": true,
83+
"configFile": "lakefile.lean"},
84+
{"url": "https://github.com/leanprover-community/plausible",
85+
"type": "git",
86+
"subDir": null,
87+
"scope": "leanprover-community",
88+
"rev": "009dc1e6f2feb2c96c081537d80a0905b2c6498f",
89+
"name": "plausible",
90+
"manifestFile": "lake-manifest.json",
91+
"inputRev": "main",
92+
"inherited": true,
93+
"configFile": "lakefile.toml"},
94+
{"url": "https://github.com/leanprover-community/LeanSearchClient",
95+
"type": "git",
96+
"subDir": null,
97+
"scope": "leanprover-community",
98+
"rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28",
99+
"name": "LeanSearchClient",
100+
"manifestFile": "lake-manifest.json",
101+
"inputRev": "main",
102+
"inherited": true,
103+
"configFile": "lakefile.toml"},
104+
{"url": "https://github.com/leanprover-community/import-graph",
105+
"type": "git",
106+
"subDir": null,
107+
"scope": "leanprover-community",
108+
"rev": "8f497d55985a189cea8020d9dc51260af1e41ad2",
109+
"name": "importGraph",
110+
"manifestFile": "lake-manifest.json",
111+
"inputRev": "main",
112+
"inherited": true,
113+
"configFile": "lakefile.toml"},
114+
{"url": "https://github.com/leanprover-community/ProofWidgets4",
115+
"type": "git",
116+
"subDir": null,
117+
"scope": "leanprover-community",
118+
"rev": "c04225ee7c0585effbd933662b3151f01b600e40",
119+
"name": "proofwidgets",
120+
"manifestFile": "lake-manifest.json",
121+
"inputRev": "v0.0.85",
122+
"inherited": true,
123+
"configFile": "lakefile.lean"},
124+
{"url": "https://github.com/leanprover-community/aesop",
125+
"type": "git",
126+
"subDir": null,
127+
"scope": "leanprover-community",
128+
"rev": "cb837cc26236ada03c81837bebe0acd9c70ced7d",
129+
"name": "aesop",
130+
"manifestFile": "lake-manifest.json",
131+
"inputRev": "master",
132+
"inherited": true,
133+
"configFile": "lakefile.toml"},
134+
{"url": "https://github.com/leanprover-community/quote4",
135+
"type": "git",
136+
"subDir": null,
137+
"scope": "leanprover-community",
138+
"rev": "bd58c9efe2086d56ca361807014141a860ddbf8c",
139+
"name": "Qq",
140+
"manifestFile": "lake-manifest.json",
141+
"inputRev": "master",
142+
"inherited": true,
143+
"configFile": "lakefile.toml"},
144+
{"url": "https://github.com/leanprover-community/batteries",
145+
"type": "git",
146+
"subDir": null,
147+
"scope": "leanprover-community",
148+
"rev": "b25b36a7caf8e237e7d1e6121543078a06777c8a",
149+
"name": "batteries",
150+
"manifestFile": "lake-manifest.json",
151+
"inputRev": "main",
152+
"inherited": true,
153+
"configFile": "lakefile.toml"}],
154+
"name": "«flt-extractor»",
155+
"lakeDir": ".lake"}

‎lean/flt/lakefile.lean‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
import Lake
2+
open Lake DSL
3+
4+
package «flt-extractor» where
5+
-- Workspace for extracting FLT documentation
6+
7+
lean_lib «FLTExtract» where
8+
roots := #[`FLTExtract]
9+
10+
require FLT from git
11+
"https://github.com/ImperialCollegeLondon/FLT" @ "main"
12+
13+
require «doc-gen4» from git
14+
"https://github.com/leanprover/doc-gen4" @ "v4.27.0"

‎lean/flt/lean-toolchain‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
leanprover/lean4:v4.27.0

0 commit comments

Comments
 (0)