Open lecopivo opened 1 month ago
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:
git clone git@github.com/leanprover/verso.git
cd verso
, and then codium .
(if you're using the closed-source version, that'd be code .
)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 exercisesI then deleted the checkout with cd ..
and rm -r verso
and did this:
git clone git@github.com/leanprover/verso.git
C-x C-f
and opened the same file as step 3 aboveThis 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!
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.
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.
OK, something else to check.
What do you get if you run #eval IO.getEnv "LD_LIBRARY_PATH"
interactively without the extra export
line?
And is it different when used interactively vs batch-mode compilation?
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"
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
Solvable by on Linux
before running Emacs or VS Code.