unknown package 'CLI' in emacs

Stream: lean4

[Simon Hudon]

I have a lake package. My root directory is called CLI. If I call lake build it builds correctly. I load it in emacs and I get "unknown package 'CLI'" in emacs when I import one of my modules. No amount of restarting makes it go away. How do I solve this?

[Sebastian Ullrich]

The "in emacs" part is not actually part of the error, is it?

[Simon Hudon]

No, you're right. Haha! Let me move my quotes around

[Sebastian Ullrich]

What does M-x lsp-describe-session say?

[Simon Hudon]

[-] lean/sat
 `-[-] lean4-lsp:60470
    |-[-] Buffers
    |  |-[+] lakefile.lean
    |  `-[+] Args.lean
    `-[+] Capabilities

The lakefile is located in lean/sat/cmd-line-args/lakefile.lean

[Sebastian Ullrich]

I see. lsp-mode assumes that every repo is a single workspace by default. You will have to add the sub-package using lsp-workspace-folders-add and lsp-workspace-folders-open.

[Simon Hudon]

Ah! Thank you! Is there a way to override that default behavior?

[Sebastian Ullrich]

You mean if we could teach it to look for lakefiles instead? I don't know, would be nice though.

[Simon Hudon]

I think I'll write a bit of emacs code so that my setup does it. I can PR it if you like

[Sebastian Ullrich]

Sounds good to me

[Simon Hudon]

Thanks!