error loading library, libleanmd4c.so

[lecopivo]

I wanted to have a look at the textbook example. It builds all fine but the infoview is broken in VS Code as well in Emacs. It errors with

error loading library, libleanmd4c.so: cannot open shared object file: No such file or directory

Solvable by on Linux

export LD_LIBRARY_PATH=~/Documents/verso/.lake/packages/MD4Lean/.lake/build/md4c/

before running Emacs or VS Code.

[david-christiansen]

Thanks for the report!

I haven't been able to reproduce this issue - for me, opening the example in a fresh checkout works without issue.

Can you walk me through the precise series of steps you're following?

Here's what I did:

1. In a terminal, I ran git clone [email protected]/leanprover/verso.git
2. I then ran cd verso, and then codium . (if you're using the closed-source version, that'd be code .)
3. I opened the file examples/textbook/DemoTextbook.lean and checked that the InfoView worked as expected once all the dependencies had built, in particular that it showed proof states in the example exercises

I then deleted the checkout with cd .. and rm -r verso and did this:

1. I again ran git clone [email protected]/leanprover/verso.git
2. In Emacs, I did C-x C-f and opened the same file as step 3 above
3. I waited for the build to complete and then checked that the InfoView worked as expected, showing proof states in the example exercises

This was on a Mac, but given that doc-gen uses the same FFI setup and that our CI runs on Linux, it would surprise me if it's an OS issue. Can you try these steps and let me know what happens on your machine?

Thanks again!

[lecopivo]

I did the exact steps as you described with code . and with cd verso; emacs examples/textbook/DemoTextbook.lean

My system:

$ uname -a
Linux tskrivan 5.15.0-117-generic #127~20.04.1-Ubuntu SMP Thu Jul 11 15:36:12 UTC 2024 x86_64 x86_64 x86_64 GNU/Linux

VS Code version: 1.91.1
Emacs version: 28.1

Happy to provide any other info about my system.

[david-christiansen]

Just a status update: we spoke about this, and the problem only occurs in interactive use (regardless of editor), not in batch mode, so CI succeeding is not really a positive indication here.

[david-christiansen]

OK, something else to check.

What do you get if you run #eval IO.getEnv "LD_LIBRARY_PATH" interactively without the extra export line?

[david-christiansen]

And is it different when used interactively vs batch-mode compilation?

[lecopivo]

I have added

#eval IO.getEnv "LD_LIBRARY_PATH"
#eval IO.getEnv "PWD"

to lakefile.lean and DemoTextbookMain.lean

In lakefile.lean the output is:
interactive:

some "././.lake/packages/subverso/.lake/build/lib:././.lake/packages/MD4Lean/.lake/build/lib:././.lake/build/lib:/home/tskrivan/.elan/toolchains/leanprover--lean4---nightly-2024-07-12/lib/lean:/home/tskrivan/.elan/toolchains/leanprover--lean4---nightly-2024-07-12/lib"
some "/home/tskrivan/Documents/verso"

build lake build:

info: none
info: some "/home/tskrivan/Documents/verso"

In DemoTextbookMain.lean the output is:
interactive (after commenting out everything else as import Verso.Genre.Manual causes the issue)

some "././.lake/packages/subverso/.lake/build/lib:././.lake/packages/MD4Lean/.lake/build/lib:././.lake/build/lib:/home/tskrivan/.elan/toolchains/leanprover--lean4---nightly-2024-07-12/lib/lean:/home/tskrivan/.elan/toolchains/leanprover--lean4---nightly-2024-07-12/lib"
some "/home/tskrivan/Documents/verso"

(I was conjecturing that PWD would return /home/tskrivan/Documents/verso/examples/textbook so those paths should be ../../.lake/... and not ././.lake/.... But this does not seem to be the case)
in build lake exe demotextbook --output _out/examples/demotextbook

info: none
info: some "/home/tskrivan/Documents/verso"

[david-christiansen]

Another user has reported this, also on Linux:

Linux moucherolle 6.8.0-41-generic #41-Ubuntu SMP PREEMPT_DYNAMIC Fri Aug  2 20:41:06 UTC 2024 x86_64 x86_64 x86_64 GNU/Linux