Using lean4export

Stream: new members

[Philip Stetson]

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]

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]

I bumped lean4export to 4.3.0

[Twm Stone]

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]

When you ask for help with an error, it's helpful to say what the error is

[Twm Stone]

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]

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]

The readme says the executable takes a sequence of modules (i.e. .olean files), not a directory

[Twm Stone]

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]

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