lake serve and lake env override existing LEAN_PATH

[alexf91]

LEAN_PATH is used with lake build, but it is overridden with lake serve and lake env.
It is still used when the Lakefile is elaborated, but not for the processes spawned afterwards.

Example for lake env:

$ LEAN_PATH=/path/to/lib lake env printenv LEAN_PATH
./build/lib

This is a problem when a package is located in a non-standard location. In this case, building with Lake works, but editing with a running language server does not because the package is not found anymore.

This is where LEAN_PATH is set:

lake/Lake/Config/Monad.lean

Lines 39 to 48 in 175793d

	def getLeanEnv [Monad m] : m (Array (String × Option String)) := do
	let ws ← getWorkspace
	let lean ← getLeanInstall
	return #[
	("LEAN_SYSROOT", lean.sysroot.toString),
	("LEAN_AR", lean.ar.toString),
	("LEAN_CC", lean.cc.toString),
	("LEAN_PATH", ws.oleanPath.toString),
	("LEAN_SRC_PATH", ws.leanSrcPath.toString)
	]

[tydeu]

This is intentional. Setting LEAN_PATH affects Lake's own elaboration but not the elaboration of packages, as their configuration is intended to be fully specified within / through their configuration file (e.g., lakefile.lean). Could you elaborate on why this is a problem for your use case? Otherwise, this issue seems like an XY problem.

[alexf91]

This is all experimental, but I want to extend or simplify some of my Lakefiles with a custom package. This is mostly focused on FFI experiments.
I have a package, let's call it LakeFFI, which I want to import in my Lakefile to create targets and (maybe later) generate some code.

The only solution I found for this was to set LEAN_PATH to the build/lib directory of the LakeFFI package before running lake build. This successfully builds the package, but the modified LEAN_PATH is a problem for editing with a language server.

I don't see how it would be possible to specify the LakeFFI dependency in the Lakefile (the same file where it is imported), because Lake can't elaborate the file without adding LakeFFI to LEAN_PATH first.

[tydeu]

@alexf91

The only solution I found for this was to set LEAN_PATH to the build/lib directory of the LakeFFI package before running lake build. This successfully builds the package, but the modified LEAN_PATH is a problem for editing with a language server.

If you are using VSCode (and vscode-lean4), you can augment the server environment's LEAN_PATH (and thus Lake's) by adding a LEAN_PATH key to the lean4.serverEnv setting.

I have a package, let's call it LakeFFI, which I want to import in my Lakefile to create targets and (maybe later) generate some code.
I don't see how it would be possible to specify the LakeFFI dependency in the Lakefile (the same file where it is imported), because Lake can't elaborate the file without adding LakeFFI to LEAN_PATH first.

Yeah, importing modules is essentially a no-go in Lake at the moment. For your example of code generation, the current "best practice" would be build a separate executable that generates the code and run that instead (potentially from the lakefile).

[alexf91]

If you are using VSCode (and vscode-lean4), you can augment the server environment's LEAN_PATH (and thus Lake's) by adding a LEAN_PATH key to the lean4.serverEnv setting.

This relies on the same mechanism. LEAN_PATH is overridden if it is set this way.

Anyways, I'll just look for another solution for now.
I have a patch to solve my part of this issue, but it's quite hacky and I'm not sure if it causes the dependency problems mentioned at the end of the README.

[tydeu]

@alexf91

This relies on the same mechanism. LEAN_PATH is overridden if it is set this.

Oh, yeah. Lake's elaboration works but once it starts the server, the server elaboration of the lakefile doesn't. ::(

As an alternative, you could have LakeFFI also be a lean_lib in the lakefile.lean. Then its olean path would be passed to the server as part of ws.oleanPath.