Need help to debug an import - and maybe a lakefile

Stream: new members

[Eduardo Ochs]

Hi all! Earlier today I uploaded my first Lean package - https://github.com/edrx/LuaTreeLean - to github, and I announced it here... but when I tried to make other (mini-)packages that also had only two Lean files, say, A.lean and B.lean, and the second one "import"ed the first with "import A", then when I opened B.lean in Emacs it always failed with "unknown package 'A'"...

I tried to debug that in two ways. First, by starting with this minimal example, and trying to fix it:

rm -Rfv /tmp/test/
mkdir   /tmp/test/
cd      /tmp/test/

cat > A.lean <<'%%%'
def a := 42
#eval a
%%%

cat > B.lean <<'%%%'
import A
#eval a
%%%

cat > lakefile.lean <<'%%%'
import Lake
open   Lake DSL
package  A
lean_lib A
%%%

...then I gave up and tried a second approach: I started with a working case - this one:

rm -Rfv /tmp/LuaTreeLean/
mkdir   /tmp/LuaTreeLean/
cd      /tmp/LuaTreeLean/
git clone https://github.com/edrx/LuaTreeLean .
# (find-file "/tmp/LuaTreeLean/Test1.lean")

...and then tried deleting files one by one until the error started to appear. But - ta-daa :confounded::confounded::confounded: - it turned out that that "working case" doesn't always work, and now my guess is that the LSP server is getting confused because some information that it stored elsewhere sometimes becames inconsistent...

How do I debug that? Or: how do I make an "import" run more verbosely? And how do I reset the LSP server in Emacs? And: can I run these tests from a shell, by doing something like "lake build; lake B.lean"? How? All pointers welcome, thanks in advance, etc...

[Eduardo Ochs]

Now there's a cleaner version of that question, with more links and a screenshot, here:

http://anggtwu.net/eev-lean4.html#import
http://anggtwu.net/IMAGES/2024-import-problem.png

@Mac Malone, is there something that I am missing? Do I need to add more ways to call lake and lean at the end of my snippet? Which ones? Should I report that as a bug? Where?...

[Mac Malone]

@Eduardo Ochs To import B in a project, you need a lean_lib B in the project's lakefile.lean. The lean_lib A invocation allows you to import modules starting with an A prefix (i.e., A.*). For example, the files A.lean or A/Basic.lean.

[Eduardo Ochs]

That's exactly what I am doing - my A.lean doesn't depend on anything, and my B.lean starts with "import A"... check the code in the beige rectangle here:
http://anggtwu.net/eev-lean4.html#import

[Mac Malone]

Oh, sorry, I misread. :man_facepalming:

[Mac Malone]

As for the screen shot, the problem there is that you are running B.lean via lean B.lean which does not use Lake (or its project configuration) at all. To give Lean the Lake informaiton, you can run lake env lean B.lean (or lake lean B.lean) instead.

[Eduardo Ochs]

Thanks!!! That - "lake env lean B.lean" - solves one of my questions, and is an indication that everything is right with my files B.lean and lakefile.lean... but when I open B.lean in Emacs it is still saying "unknown package 'A'"...

[Eduardo Ochs]

But I just found this:
https://github.com/leanprover/lean4/blob/master/src/Lean/Server/README.md
let me see what I can get by turning its debugging flags on. Thanks! =)

[Mac Malone]

Sadly, I do not use Emacs, so I am not much help in debugging Emacs LSP issues. I am not sure who is the best Emacs guru here, but @Sebastian Ullrich may be able to help.

[Eduardo Ochs]

Hi @Sebastian Ullrich!
I just discovered lsp-describe-session... here's what it shows in a case in which the "import A" in B.lean gives an error:

[Eduardo Ochs]

sshot.png

[Eduardo Ochs]

I often use /tmp/a.lean as a scratch .lean file for quick tests, and in the screenshot the window at the right, that was generated by (lsp-describe-session), is saying that both /tmp/import-test/B.lean and /tmp/a.lean are being watched by the same server (<- is that the right term?), lean4-lsp:318258...

[Eduardo Ochs]

And the buffer *lean4-lsp::stderr* contains this:

error: no such file or directory (error code: 2)
  file: ./lakefile.lean
warning: package configuration has errors, falling back to plain `lean --server`

I do have a /tmp/import-test/lakefile.lean and I don't have a /tmp/lakefile.lean.
Does that help?

[Richard Copley]

Things are set up to assume that there is a project with a lakefile.lean or lakefile.toml (and a lean-toolchain). Without those it isn't clear which lean exe to run and with what arguments.

This comes up a lot! It's not stupid to expect things to work on any old file lying around. But things do not.

[Eduardo Ochs]

I think that I've solved the problem - in a dirty way, but whatever...
One low-level way of inspecting the directories of the current session is by running this:

(lsp-session-folders (lsp-session))

That list of directories is one of the things that is saved in ~/.emacs.d/.lsp-session-v1 - a.k.a. lsp-session-file. I tried to find the "right" way to delete directories from there, then gave up after a few minutes, deleted that file, and added some directories again by visiting /tmp/import-test/B.lean and /tmp/a.lean in different orders, with and without a /tmp/lakefile.lean.

Thanks!