use standard library in alternative location

Stream: lean4

[Locria Cyber]

I'm developing the Lean standard library (not std4). However, the lean LSP does not recognize changes to the standard library.

[Locria Cyber]

Is there a way to let Lean use Lean.xxx source files from another directory?

[Mario Carneiro]

I don't know what you mean by "the Lean standard library (not std4)". Is this a project of your own? What kind of LSP changes are you noticing?

[Mario Carneiro]

@Locria Cyber

[Mario Carneiro]

By Lean.xxx are you talking about the Lean package, i.e. the lean compiler itself? (We usually call that the lean core library for disambiguation)

[Mario Carneiro]

You should be able to refer to it via import Lean from any lean file, assuming you are using lake to build the project. It is bundled with the compiler itself so you should always be able to access it even if your project has no dependencies

[Locria Cyber]

Mario Carneiro said:

By Lean.xxx are you talking about the Lean package, i.e. the lean compiler itself? (We usually call that the lean core library for disambiguation)

yes

[Locria Cyber]

I'm modifying the Lean package. I want the LSP to pick up on the change.

[Mario Carneiro]

Several things in lean core dev are weird compared to regular lean projects, this is one of them. The equivalent of "Refresh File Dependencies" in lean core is make