Zulip Chat Archive
Stream: new members
Topic: Using lean4export
Philip Stetson (Nov 30 2023 at 03:16):
I am having trouble running lean4export; I believe I have it installed properly and I can't understand the code well enough to diagnose it myself.
I have a build of mathlib with this dependency installed: https://github.com/leanprover/lean4export
I have imported the mathlib libraries that I want to export by calling them in the header of the Export.lean file. Although, whenever I run "lake exe lean4export" I get the error citing lean4export/Main.lean at lines 7 and 8:
"application type mismatch
importModules imports
argument
imports
has type
List ?m.237 : Type
but is expected to have type
Array Import : TypeLean 4"
I want am not sure whether I am using the package properly or if there is a bug. Please let me know if you know how to run lean4export.
Alex J. Best (Nov 30 2023 at 18:44):
You could try running the branch in https://github.com/leanprover/lean4export/pull/2/, I also cant work out how to use that version of export with a newer library. @Sebastian Ullrich do you plan to merge such updates into lean4export or do you have advice how to set the paths correctly to make this work as is
Mario Carneiro (Dec 01 2023 at 03:28):
I bumped lean4export to 4.3.0
Twm Stone (Jan 12 2025 at 16:06):
Hi,
I'm trying to get lean4export working on a new Lean 4 repo. There aren't really instructions there for how to install / use it (maybe this is just obvious to people who use lake a lot?) so I added the following and rebuilt, but I get an error.
[[lean_exe]]
name = "lean4export"
git = "https://github.com/leanprover/lean4export"
rev = "master"
I assume I need to copy / build the code inside my repo somehow?
Ruben Van de Velde (Jan 12 2025 at 16:11):
When you ask for help with an error, it's helpful to say what the error is
Twm Stone (Jan 12 2025 at 16:15):
gah sorry I pressed <enter> before pasting
(base) tops@TOPS:~/test4export$ lake exe lean4export
✖ [2/4] Running lean4export
error: no such file or directory (error code: 2)
file: ././././lean4export.lean
✖ [3/4] Running lean4export
error: no such file or directory (error code: 2)
file: ././././lean4export.lean
Some required builds logged failures:
- lean4export
- lean4export
error: build failed
Twm Stone (Jan 12 2025 at 16:17):
I also tried checking out the lean4export repository and running lake build
in there; this means lake exe lean4export ../path/to/my/repo
does "work" but has this error instead, and conceptually this seems a bit wrong (running it from outside the project I want to affect) so I didn't pursue that further:
(base) tops@TOPS:~/lean4export$ lake exe lean4export ../test4export/
PANIC at Option.get! Init.Data.Option.BasicAux:16:14: value is none
backtrace:
././.lake/build/bin/lean4export(lean_panic_fn+0x6d) [0x5597b5d4f03d]
././.lake/build/bin/lean4export(l_Array_mapMUnsafe_map___at_main___spec__2+0x129) [0x5597b1dfdb49]
././.lake/build/bin/lean4export(_lean_main+0x1d4) [0x5597b1dff444]
././.lake/build/bin/lean4export(+0xedcde3) [0x5597b1dffde3]
/lib/x86_64-linux-gnu/libc.so.6(+0x2a1ca) [0x7f92bfc5d1ca]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x8b) [0x7f92bfc5d28b]
././.lake/build/bin/lean4export(_start+0x25) [0x5597b1dfd7a5]
uncaught exception: import failed, trying to import module with anonymous name
Sebastian Ullrich (Jan 12 2025 at 16:57):
The readme says the executable takes a sequence of modules (i.e. .olean
files), not a directory
Twm Stone (Jan 12 2025 at 17:03):
When I try that I get the same error around anonymous names:
(base) tops@TOPS:~/lean4export$ lake exe lean4export ../test4export/.lake/build/lib/Main.olean
PANIC at Option.get! Init.Data.Option.BasicAux:16:14: value is none
backtrace:
././.lake/build/bin/lean4export(lean_panic_fn+0x6d) [0x5572f212a43d]
././.lake/build/bin/lean4export(l_Array_mapMUnsafe_map___at_main___spec__2+0x129) [0x5572ee1d8cc9]
././.lake/build/bin/lean4export(_lean_main+0x1d4) [0x5572ee1da5c4]
././.lake/build/bin/lean4export(+0xedcfa3) [0x5572ee1dafa3]
/lib/x86_64-linux-gnu/libc.so.6(+0x2a1ca) [0x7f81bc7631ca]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x8b) [0x7f81bc76328b]
././.lake/build/bin/lean4export(_start+0x25) [0x5572ee1d8925]
uncaught exception: import failed, trying to import module with anonymous name
Twm Stone (Jan 12 2025 at 17:37):
actually I get the same thing when I try export an olean file in the project itself, e.g. lake exe lean4export .lake/build/lib/Thing.olean
is complaining about trying to import module with anonymous name
Last updated: May 02 2025 at 03:31 UTC