Lake: add to LEAN_PATH via Lake

Stream: lean4

[Scott Morrison]

Currently in mathport, to open a synported file in VSCode (or just ./Test.lean), I have to add

    "lean4.serverEnv": {
        "LEAN_PATH": "./Lib4/leanbin/build/lib:./Lib4/mathbin/build/lib"
    }

to settings.json.

What is "the lake way" to do this? Presumably there is something I can put in the lakefile.lean.

Note here I don't want lake to do any compilation in those directories; I just want the oleans there (which have been created by the binport part of mathport) to be on the LEAN_PATH.

[Mac]

This should already be automatically done via print-paths in the server if leanbin/mathbin/liquidbin is listed as dependency. This worked for me the last time I tested test-mathport.

[Scott Morrison]

Ah, okay, maybe I just need to transport some settings back from test-mathport to mathport itself.

[Scott Morrison]

@Mac, ah, so the subtlety is that I would like to be able to:

1. build mathport (at which point ./Lib4 doesn't exist),
2. run it (thereby creating ./Lib4 and its contents, and then
3. open files that are in, or depend on, ./Lib4.

Thus if I add mathbin as a dependency in the lakefile, that last stage works fine, but I can't actually build mathport, as very reasonably lake can't find a declared dependency:

build error: no such file or directory (error code: 2)
  file: ././Lib4/mathbin/./lakefile.lean
error: build failed

I appreciate this is a bit of a weird thing to do, but it's the workflow in mathport for now! I can get by with overriding LEAN_PATH, but if you have better suggestions for lake to cope with this setup I'm all ears.

[Mac]

Scott Morrison said:

@Mac, ah, so the subtlety is that I would like to be able to:

1. build mathport (at which point ./Lib4 doesn't exist),
2. run it (thereby creating ./Lib4 and its contents, and then
3. open files that are in, or depend on, ./Lib4.

Thus if I add mathbin as a dependency in the lakefile, that last stage works fine, but I can't actually build mathport, as very reasonably lake can't find a declared dependency:

What is "the lakefile" here? The lakefile for mathport, mathbin/Lib4, or the thing that depends on mathbin/Lib4?

[Mac]

Fyi, from your description, I am fairly confident that lake as it stands can handle this kind of setup, but I need a bit more info on how this all interconnects to explain exactly how.

[Scott Morrison]

When I was saying "the lakefile" above, I was always referring to ./lakefile.lean.

[Mac]

Oh, thinking about this a bit more: is the problem that you are trying to open mathbin/leanbin/liquidbin files within a VSCode instance opened to mathport?

[Scott Morrison]

Yes!

[Mac]

Ah, that is not supported by the VSCode extension itself

[Mac]

it only uses the package configuration from the root directory not those of subdirectories

[Mac]

See the discussion at e.g., https://github.com/leanprover/vscode-lean4/issues/15

[Mac]

The VSCode extension only starts a Lean server in the root directory and server only uses information from the root configuration, so subpackages do not have extension/server support.

[Mac]

This is also a problem in the lake repo itself as none of the examples in the lake/examples folder get proper editor support (when viewed from VSCode instance opened tothe root of repo)

[Mac]

Your particular use case could be incidentally solved by lake in the future when it supports multiple libraries/packages in a single configuration/workspace (and the thus mathport/liquidbin/mathbin/leanbin could all live in the same configuration file), but even that would have the downside of tying them all together when they are conceptually distinct packages.

[Scott Morrison]

Okay. I have been trying instead to directly open the Lib4/mathbin/ directory in VSCode, so far without success, but for different reasons. :-)