Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Panic exporting #5

Open
metakunt opened this issue Oct 17, 2024 · 9 comments
Open

Panic exporting #5

metakunt opened this issue Oct 17, 2024 · 9 comments

Comments

@metakunt
Copy link

Greetings. I've tried to use the export with no avail.

Process to reproduce.

  • Clone github repo.
  • In different folder with given path create following minimal file that I want to export.
theorem iffo (a b : Prop) (h1: a->b) (h2: b->a): a↔b := by
  have hy := Iff.intro h1 h2
  exact hy
  • run in cloned gh repo "lake exe lean4export -- ../test/Test/das.lean" where "../test/Test/das.lean" is the file above I want to export.

Stacktrace:

PANIC at Option.get! Init.Data.Option.BasicAux:16:14: value is none
backtrace:
./.lake/build/bin/lean4export(lean_panic_fn+0x9e) [0x5f2dcb216e0e]
./.lake/build/bin/lean4export(l_List_mapTR_loop___at_main___spec__14+0x21a) [0x5f2dc872f5aa]
./.lake/build/bin/lean4export(_lean_main+0x36b) [0x5f2dc872fa9b]
./.lake/build/bin/lean4export(+0xae6113) [0x5f2dc8730113]
/usr/lib/libc.so.6(+0x25e08) [0x717efdb8ce08]
/usr/lib/libc.so.6(__libc_start_main+0x8c) [0x717efdb8cecc]
./.lake/build/bin/lean4export(_start+0x25) [0x5f2dc872db65]
PANIC at Option.get! Init.Data.Option.BasicAux:16:14: value is none
backtrace:
./.lake/build/bin/lean4export(lean_panic_fn+0x9e) [0x5f2dcb216e0e]
./.lake/build/bin/lean4export(l_dumpConstant___lambda__4+0x2cb) [0x5f2dc874095b]
./.lake/build/bin/lean4export(l_List_forIn_loop___at_main___spec__12+0xd3) [0x5f2dc872ed63]
./.lake/build/bin/lean4export(lean_apply_3+0x375) [0x5f2dcb222de5]
./.lake/build/bin/lean4export(l_ReaderT_bind___at_main___spec__13___rarg+0x44) [0x5f2dc872f0c4]
./.lake/build/bin/lean4export(lean_apply_3+0x375) [0x5f2dcb222de5]
./.lake/build/bin/lean4export(l_M_run___rarg+0x23) [0x5f2dc87311c3]
./.lake/build/bin/lean4export(+0xae6113) [0x5f2dc8730113]
/usr/lib/libc.so.6(+0x25e08) [0x717efdb8ce08]
/usr/lib/libc.so.6(__libc_start_main+0x8c) [0x717efdb8cecc]
./.lake/build/bin/lean4export(_start+0x25) [0x5f2dc872db65]
0 #EV 0
#AX 0 0 

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.

@ammkrn
Copy link

ammkrn commented Oct 17, 2024

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
Copy link
Author

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
Copy link
Collaborator

digama0 commented Oct 18, 2024

Here's an example use:

  • Clone lean4export into a lean4export folder, run lake build inside
  • Run lake new test from the root to produce a test folder sibling to lean4export
  • Run lake 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 project

Note 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
Copy link
Author

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/lean

I guess once I can get this minimal example fixed I'll try to think about how to export parts of mathlib.

@metakunt
Copy link
Author

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)

@digama0
Copy link
Collaborator

digama0 commented Oct 18, 2024

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
Copy link
Author

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/lean

So 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.lean

In 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
Copy link
Collaborator

digama0 commented Oct 20, 2024

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
Copy link
Author

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 176

Ok cool, this appears to be working.

I will try to experiment a bit and see if I can export a theorem.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants