Open metakunt opened 1 month ago
ammkrn
commented
1 month ago Can you include some information about your versions of lake, lean, and dependencies? This is most likely due to a version mismatch (then we can get to your point about the instructions not being clear).
metakunt
commented
1 month ago Sure thing. In lean4export folder:
lake --version
Lake version 5.0.0-8e5cf64 (Lean version 4.3.0)In test folder:
lake --version
Lake version 5.0.0-873ef2d (Lean version 4.8.0-rc2)I hope this helps. If not I can also update the lake-manifest, lakefile or lean-toolchain files.
digama0
commented
1 month ago Here's an example use:
lean4export into a lean4export folder, run lake build insidelake new test from the root to produce a test folder sibling to lean4exportlake env ../lean4export/.lake/build/bin/lean4export Test.Basic -- hello and it will export the transitive dependencies of the def hello := "world" definition generated in the sample projectNote that the argument to lean4export is first the module path (not the file name), and second the definitions you want to export. You can leave off the definition list but in that case it will export all of Init, which is quite large (I get a 33 MB export in this manner, compared to only 4 KB if you restrict to hello).
metakunt
commented
1 month ago Thanks @digama0. Here is the output from scratch.
mkdir newfolder
cd newfolder/
git clone https://github.com/leanprover/lean4export.git
OUTPUT:
Cloning into 'lean4export'...
remote: Enumerating objects: 58, done.
remote: Counting objects: 100% (58/58), done.
remote: Compressing objects: 100% (39/39), done.
remote: Total 58 (delta 20), reused 51 (delta 13), pack-reused 0 (from 0)
Receiving objects: 100% (58/58), 7.35 MiB | 10.59 MiB/s, done.
Resolving deltas: 100% (20/20), done.
cd lean4export/
lake build
OUTPUT:
info: downloading component 'lean'
227.4 MiB / 227.4 MiB (100 %) 11.2 MiB/s ETA: 0 s
info: installing component 'lean'
Build completed successfully.
cd ..
lake new test
cd test
lake env ../lean4export/.lake/build/bin/lean4export Test.Basic -- hello
OUTPUT:
info: test: no previous manifest, creating one from scratch
uncaught exception: unknown module prefix 'Test'
No directory 'Test' or file 'Test.olean' in the search path entries:
./.lake/build/lib
/home/xxx/.elan/toolchains/stable/lib/lean
/home/xxx/.elan/toolchains/stable/lib/leanI guess once I can get this minimal example fixed I'll try to think about how to export parts of mathlib.
metakunt
commented
1 month ago Lean versions are different in test and lean4export directory. I don't know if that matters. In test directory
lean --version
Lean (version 4.7.0, x86_64-unknown-linux-gnu, commit 6fce8f7d5cd1, Release)In lean4export directory
lean --version
Lean (version 4.12.0, x86_64-unknown-linux-gnu, commit dc2533473114, Release)Oh, yes lake new has an issue whereby it puts stable in the lean-toolchain, which is basically never what you want. You should copy the lean-toolchain of lean4export or otherwise ensure that they are using the same version (and I recommend you use a recent version, i.e. 4.12.0).
metakunt
commented
1 month ago Alright, here is the output of the commands, I still get the same issue that it appears not to find Test.
cp lean4export/lean-toolchain test/lean-toolchain
cat test/lean-toolchain
OUTPUT:
leanprover/lean4:v4.12.0
cd test
lake env ../lean4export/.lake/build/bin/lean4export Test.Basic -- hello
OUTPUT:
uncaught exception: unknown module prefix 'Test'
No directory 'Test' or file 'Test.olean' in the search path entries:
././.lake/build/lib
/home/xxx/.elan/toolchains/leanprover--lean4---v4.12.0/lib/lean
/home/xxx/.elan/toolchains/leanprover--lean4---v4.12.0/lib/leanSo apparently it is looking for the Test directory. Do I need to append the current path to the search path or do I need to compile the Test "module"?
Here is the output of some extra info:
ls
OUTPUT:
lakefile.lean lake-manifest.json lean-toolchain Main.lean Test Test.leanIn a non-lean folder i get the following output:
lean --version
Lean (version 4.7.0, x86_64-unknown-linux-gnu, commit 6fce8f7d5cd1, Release)
lake --version
Lake version 5.0.0-6fce8f7 (Lean version 4.7.0)I am not sure how I installed lean, probably by installing the vscode extension. Do I need to update lean?
digama0
commented
1 month ago You need to compile Test first, i.e. lake build inside the test directory. If it worked, you should see a file at test/.lake/build/lib/Test/Basic.olean. (Note that you didn't use ls -a so you probably missed the .lake directory.)
metakunt
commented
1 month ago cd newfolder/
cd test
lake build
Build completed successfully.
lake env ../lean4export/.lake/build/bin/lean4export Test.Basic -- hello > O.txt
cat O.txt
OUTPUT
1 #NS 0 List
2 #NS 1 nil
3 #NS 0 α
4 #NS 0 u
1 #UP 4
2 #US 1
0 #ES 2
1 #EC 1 1
2 #EV 0
3 #EA 1 2
4 #EP #BI 3 0 3
5 #NS 1 cons
6 #NS 0 head
7 #NS 0 tail
5 #EV 1
6 #EA 1 5
7 #EV 2
8 #EA 1 7
9 #EP #BD 7 6 8
10 #EP #BD 6 2 9
11 #EP #BI 3 0 10
12 #EP #BD 3 0 0
#IND 1 1 12 2 2 4 5 11 4
8 #NS 0 Nat
9 #NS 8 zero
13 #EC 8
10 #NS 8 succ
11 #NS 0 n
14 #EP #BD 11 13 13
3 #US 0
15 #ES 3
#IND 0 8 15 2 9 13 10 14
12 #NS 0 LT
13 #NS 12 mk
14 #NS 0 lt
15 #NS 0 a
16 #NS 15 _@
17 #NS 16 Init
18 #NS 17 Prelude
19 #NS 18 _hyg
20 #NI 19 2234
21 #NI 19 2236
16 #ES 0
17 #EP #BD 21 5 16
18 #EP #BD 20 2 17
19 #EC 12 1
20 #EA 19 5
21 #EP #BD 14 18 20
22 #EP #BI 3 0 21
#IND 1 12 12 1 13 22 4
22 #NS 12 lt
23 #NS 0 self
23 #EA 19 2
24 #EP #BD 21 7 16
25 #EP #BD 20 5 24
26 #EP #BC 23 23 25
27 #EP #BI 3 0 26
28 #EJ 12 0 2
29 #EL #BC 23 23 28
30 #EL #BD 3 0 29
#DEF 22 27 30 4
24 #NS 8 le
25 #NS 24 refl
31 #EC 24
32 #EA 31 2
33 #EA 32 2
34 #EP #BI 11 13 33
26 #NS 24 step
27 #NS 0 m
28 #NI 19 4046
35 #EA 31 5
36 #EA 35 2
37 #EA 31 7
38 #EC 10
39 #EA 38 5
40 #EA 37 39
41 #EP #BD 28 36 40
42 #EP #BI 27 13 41
43 #EP #BI 11 13 42
29 #NI 19 4039
44 #EP #BD 29 13 16
45 #EP #BD 11 13 44
#IND 1 24 45 2 25 34 26 43
30 #NS 8 lt
46 #EA 31 39
47 #EA 46 2
48 #EL #BD 27 13 47
49 #EL #BD 11 13 48
#DEF 30 45 49
31 #NS 0 instLTNat
50 #EC 12 0
51 #EA 50 13
52 #EC 13 0
53 #EA 52 13
54 #EC 30
55 #EA 53 54
#DEF 31 51 55
32 #NS 0 Fin
33 #NS 32 mk
34 #NS 0 val
35 #NS 0 isLt
56 #EC 22 0
57 #EA 56 13
58 #EC 31
59 #EA 57 58
60 #EA 59 2
61 #EA 60 5
62 #EC 32
63 #EA 62 7
64 #EP #BD 35 61 63
65 #EP #BD 34 13 64
66 #EP #BI 11 13 65
67 #EP #BD 11 13 15
#IND 1 32 67 1 33 66
36 #NS 0 OfNat
37 #NS 36 mk
38 #NS 0 x
39 #NS 38 _@
40 #NS 39 Init
41 #NS 40 Prelude
42 #NS 41 _hyg
43 #NI 42 2207
44 #NS 0 ofNat
68 #EC 36 1
69 #EA 68 7
70 #EA 69 5
71 #EP #BD 44 5 70
72 #EP #BI 43 13 71
73 #EP #BI 3 0 72
74 #EP #BD 43 13 0
75 #EP #BD 3 0 74
#IND 2 36 75 1 37 73 4
45 #NS 36 ofNat
76 #EA 68 5
77 #EA 76 2
78 #EP #BC 23 77 7
79 #EP #BD 43 13 78
80 #EP #BI 3 0 79
81 #EJ 36 0 2
82 #EL #BC 23 77 81
83 #EL #BD 43 13 82
84 #EL #BD 3 0 83
#DEF 45 80 84 4
46 #NS 0 instOfNatNat
85 #EC 36 0
86 #EA 85 13
87 #EA 86 2
88 #EP #BD 11 13 87
89 #EC 37 0
90 #EA 89 13
91 #EA 90 2
92 #EA 91 2
93 #EL #BD 11 13 92
#DEF 46 88 93
47 #NS 0 UInt32
48 #NS 47 size
94 #EC 45 0
95 #EA 94 13
96 #ELN 4294967296
97 #EA 95 96
98 #EC 46
99 #EA 98 96
100 #EA 97 99
#DEF 48 13 100
49 #NS 47 mk
101 #EC 48
102 #EA 62 101
103 #EC 47
104 #EP #BD 34 102 103
#IND 0 47 15 1 49 104
50 #NS 0 Or
51 #NS 50 inl
52 #NS 0 b
53 #NS 0 h
105 #EC 50
106 #EA 105 7
107 #EA 106 5
108 #EP #BD 53 5 107
109 #EP #BI 52 16 108
110 #EP #BI 15 16 109
54 #NS 50 inr
111 #EP #BD 53 2 107
112 #EP #BI 52 16 111
113 #EP #BI 15 16 112
114 #EP #BD 52 16 16
115 #EP #BD 15 16 114
#IND 2 50 115 2 51 110 54 113
55 #NS 0 And
56 #NS 55 intro
57 #NS 0 left
58 #NS 0 right
116 #EC 55
117 #EV 3
118 #EA 116 117
119 #EA 118 7
120 #EP #BD 58 5 119
121 #EP #BD 57 5 120
122 #EP #BI 52 16 121
123 #EP #BI 15 16 122
#IND 2 55 115 1 56 123
59 #NS 8 isValidChar
124 #ELN 55296
125 #EA 95 124
126 #EA 98 124
127 #EA 125 126
128 #EA 60 127
129 #EA 105 128
130 #ELN 57343
131 #EA 95 130
132 #EA 98 130
133 #EA 131 132
134 #EA 59 133
135 #EA 134 2
136 #EA 116 135
137 #ELN 1114112
138 #EA 95 137
139 #EA 98 137
140 #EA 138 139
141 #EA 60 140
142 #EA 136 141
143 #EA 129 142
144 #EL #BD 11 13 143
#DEF 59 44 144
60 #NS 32 val
145 #EA 62 2
146 #EP #BD 23 145 13
147 #EP #BI 11 13 146
148 #EJ 32 0 2
149 #EL #BD 23 145 148
150 #EL #BD 11 13 149
#DEF 60 147 150
61 #NS 47 val
151 #EP #BD 23 103 102
152 #EJ 47 0 2
153 #EL #BD 23 103 152
#DEF 61 151 153
62 #NS 47 toNat
154 #EP #BD 11 103 13
155 #EC 60
156 #EA 155 101
157 #EC 61
158 #EA 157 2
159 #EA 156 158
160 #EL #BD 11 103 159
#DEF 62 154 160
63 #NS 47 isValidChar
161 #EP #BD 11 103 16
162 #EC 59
163 #EC 62
164 #EA 163 2
165 #EA 162 164
166 #EL #BD 11 103 165
#DEF 63 161 166
64 #NS 0 Char
65 #NS 64 mk
66 #NS 0 valid
167 #EC 63
168 #EA 167 2
169 #EC 64
170 #EP #BD 66 168 169
171 #EP #BD 34 103 170
#IND 0 64 15 1 65 171
67 #NS 0 String
68 #NS 67 mk
69 #NS 0 data
172 #EC 1 0
173 #EA 172 169
174 #EC 67
175 #EP #BD 69 173 174
#IND 0 67 15 1 68 175
70 #NS 0 hello
176 #ELS 77 6F 72 6C 64
#DEF 70 174 176Ok cool, this appears to be working.
I will try to experiment a bit and see if I can export a theorem.
Greetings. I've tried to use the export with no avail.
Process to reproduce.
Stacktrace:
I think I am doing something horribly wrong, but I just can't grasp the how to run. I don't know what the input for the cli is. My goal is quite simple, given an input file that contains one or more theorems, export it.
Also it would be awesome if the exported examples in the example folder had some reproducible steps.
Help is much appreciated.