Imports

[KieranL2075]

Hi, Just starting out using neovim and lean4 (have used lean3 before but not lean4) so solution probably trivial.

lac ex1/
├── Lac/
│ ├── ex/
│ │ └── ex1.lean
│ ├── lec/
│ │ ├── lang.lean
│ │ └── langOp.lean
│ ├── Basic.lean
│ ├── lake-manifest.json
│ ├── lakefile.tmol
│ └── lean-toolchain
├── lake-manifest.json
├── lakefile.tmol
└── lean-toolchain

My issue is that i cannot import Lec module any of the lean files lang.lean, langOp.lean nor ex1.lean.

I wanted to ask here because other IDEs work file with the project structure I just cannot get the lean.nvim plugin to understand the project. I am sure its something obvious.

Any help or advice would be awesome. Thanks.

[Julian]

Hi. You have multiple lean-toolchain and lake-manifest.jsons there, which means this isn't one project it's at least two -- you also have .tmol rather than .toml -- is this a typo from typing it manually or is your file really called lakefile.tmol?

In general lean.nvim should essentially work the same as VSCode here I think.

[KieranL2075]

The tmol is a typo my bad, oops.

lake doesn't read it as multiple projects due to only one Lac.lean file (which i might have forgot to include, sitting in the out most directory. It seems to work if I open that file (Lac.lean) before any other file, but not if i open it in a different order. Just thought that was interesting behavior. VS code opens it fine, Neovim seems to depend on the order I open the files.

[Julian]

(lean.nvim also uses lake)

But basically I'd recommend you fix the package layout regardless. I suspect you'd get different VSCode behavior as well depending on which directory you open as your workspace.