VSCode Lean4 extension doesn't like `lakefile.lean`

Stream: lean4

[Scott Morrison]

I now get error messages of the form:

`leanpkg print-paths` failed:

stderr:
configuring testdep 0.1
/Users/scott/projects/lean/test-mathport must contain a unique '.lean' file as the package root

because I have both lakefile.lean and Testdep.lean in the root of a repository. Is this a known issue? Is someone already working on having the VSCode lean4 extension talk to lake to obtain the path information?

[Mac]

@Scott Morrison Yeah, sadly Lean server and VSCode integration does not exist for Lake yet.

The way I understand it there needs to be an change to the Lean 4 server so that it will trylake print-paths if there is a lakefile.lean in the working directory. There may also be something on the VSCode side that needs to be done as well, but I am not sure what.

@Sebastian Ullrich , @Gabriel Ebner ?

[Sebastian Ullrich]

I believe that's it

[Gabriel Ebner]

Yes, the server calls leanpkg print-paths A.B C.D E.F.G to compile the specified dependencies and print the path for the oleans. Changing this to call lake is the easiest way to support lake.
I would take the opportunity to use a more descriptive command name though (like compile-imports), and maybe also upgrade the output format to json.

[Gabriel Ebner]

In the vscode extension, there is nothing to do (because we require the user to open the right directory). We'll need to adapt the neovim plugin though. I'm not sure if the emacs mode requires any changes.

[Sebastian Ullrich]

Compiling imports is merely a necessary side-effect for printing their paths :grinning_face_with_smiling_eyes:

[Gabriel Ebner]

Yeah, I'm not sure what the best name for the operation is either. If we reimplement --old, then that command will only print and not compile.

[Sebastian Ullrich]

When is --old used in Lean 3c?

[Gabriel Ebner]

You need to manually set it in the vscode settings (as an extra argument to the server). Then the server will use oleans even if they're out of date.

[Mac]

Sebastian Ullrich said:

I believe that's it

What is the plan on this? Is this something you will be implementing after merging #683? Or should i be updating the server and PR'ing a change?

[Sebastian Ullrich]

It should be part of the PR, I can write the Lean side. JSON sounds like a good idea.

[Mac]

@Sebastian Ullrich currently, lake print-paths operators the same as leanpkg print-paths. That is, it performs a build (outputting the usual build information along the way) and then spits out two lines of search paths (the first being oleans and the second being sources). How would you like to see that changed?

[Sebastian Ullrich]

How about {"LEAN_PATH": ..., "LEAN_SRC_PATH": ...}?

[Mac]

@Sebastian Ullrich works for me. What about the build output, should that be completely quieted?

[Sebastian Ullrich]

Right. We definitely want to keep streaming it to the editor, so should we put the build output on stderr and the JSON on stdout?

[Mac]

@Sebastian Ullrich okay, done (results to stdout, build output to stderr). Do you want the the values for LEAN_PATH and LEAN_SRC_PATH in the JSON to still be search paths (i.e., strings separated by a :) or would you like them to just be JSON arrays of paths?

[Sebastian Ullrich]

Thanks. I have a slight preference for search paths since most users will simply forward the values to Lean. What do you think?

[Mac]

@Sebastian Ullrich it does not matter to me. The only complaints I can imagine is that search paths could break if a file name contains a ':'/';` (which I think my a be legal on Linux?) and that said separator is different on each platform (whereas the JSON would be cross-platform). Otherwise, they are both relatively easy to parse / process.

[Mac]

@Sebastian Ullrich another, somewhat unrelated question that has been bugging me: why are the Json and Xml libraries in Lean instead of Std?

[Gabriel Ebner]

I have a slight preference for search paths since most users will simply forward the values to Lean.

We're talking about a lean-internal API here that is only called by the server. The reason I suggested json here is partly for 1) future proofness, and 2) clarity of the information when debugging (if the two arrays come with human-readable keys then you don't have to guess what the first and second lines are (or if it's possible to get a third line)).

Regarding the format, I was thinking of a slightly more typed version:

deriving instance ToJson for System.FilePath
deriving instance FromJson for System.FilePath

instance [ToJson α] : ToJson (List α) where
  toJson xs := toJson xs.toArray

instance [FromJson α] : FromJson (List α) where
  fromJson? j := (fromJson? j (α := Array α)).map Array.toList

structure OutputBikesheddable where
  sourcePath : SearchPath
  binaryPath : SearchPath
  deriving ToJson, FromJson

[Mac]

@Gabriel Ebner neat idea. @Sebastian Ullrich what do you think? If we went this route, the FilePath and List instances should be added to Lean itself not Lake.

[Gabriel Ebner]

If we choose this approach, then everything in the snippet needs to be in Lean. The server needs the FromJson OutputBikesheddable instance after all.

[Mac]

true, good point! In that case I would name that structure as follows:

structure LeanPaths where
  oleanPath : SearchPath
  sourcePath : SearchPath
  deriving ToJson, FromJson

[Gabriel Ebner]

I think we also need custom FromJson/ToJson instances for FilePath. The default one produces {"toString": "my/path"}.

[Wojciech Nawrocki]

Mac said:

why are the Json and Xml libraries in Lean instead of Std?

I think this is just because we needed them in Lean (Json for the first LSP version), and so they ended up there. They might or might not also depend on other stuff in Lean. There are many modules or parts of modules which, imo, should be in Std before version 4.0 but aren't because it's not high priority.

[Mac]

Wojciech Nawrocki [Fair enough, but to this point:

I think this is just because we needed them in Lean

it should be noted that virtually of all Std is needed in Lean (that is why it is in the Lean core in the first place), so that really shouldn't be a consideration for its placement.

[Sebastian Ullrich]

Gabriel Ebner said:

I have a slight preference for search paths since most users will simply forward the values to Lean.

We're talking about a lean-internal API here that is only called by the server

Is it likely it will stay that way for long :) ? If a user either wants to execute lean directly on a module (for which there could also be a subcommand like lake lean, much like cargo rustc) or wants to run any other Lean program that wants to importModules that module, using print-paths to set up the environment seems like the most natural solution. It is our equivalent to nix print-dev-env. In fact, perhaps it should even default to export LEAN_PATH=... Bash output just like the Nix command unless --json is given.

[Gabriel Ebner]

to set up the environment seems like the most natural solution.

I think the most natural solution would be to have a lake lean ... command that sets up the correct environment variables (and --plugin arguments!!).

[Gabriel Ebner]

or wants to run any other Lean program that wants to importModules that module,

If you are already running Lean then it is arguably easier to parse the json (with the FromJson instance) than to parse a bash script.

[Sebastian Ullrich]

I was thinking more like $(lake print-paths Mod.lean); myprogram Mod.lean

[Sebastian Ullrich]

But if myprogram wants to hardcode dependency on lake, then it can just use the same code as the server to communicate with it, sure

[Gabriel Ebner]

In fact, perhaps it should even default to export LEAN_PATH=... Bash output

This reminds me of https://github.com/NixOS/nix/pull/545. Requiring to source bash scripts is a terrible UX for other shells.

[Gabriel Ebner]

Sebastian Ullrich said:

I was thinking more like $(lake print-paths Mod.lean); myprogram Mod.lean

 $(lake print-paths Mod.lean); myprogram Mod.lean
fish: Command substitutions not allowed
$(lake print-paths Mod.lean); myprogram Mod.lean
 ^

[Sebastian Ullrich]

Also not very cross-platform, I'll give you that :)

[Sebastian Ullrich]

So probably JSON is sufficient. I would still be surprised if users didn't find other uses for print-paths.

[Gabriel Ebner]

wants to hardcode dependency on lake

I thought the plan was to hardcode a lake dependency everywhere, no? At least editors, etc., will interface directly with lake so it's not like you can get away from it.

[Gabriel Ebner]

So probably JSON is sufficient. I would still be surprised if users didn't find other uses for print-paths.

In most cases the command that is called "print-paths" right now is a pretty bad fit. For example, if you want to get the list of source directories you don't want to trigger a build.

[Sebastian Ullrich]

I think editors are more justified in being opinionated than (underlying) cmdline tools are, just like lean does not depend on leanpkg/lake while lean --server does. But it doesn't really matter, I'm sure potential external users will manage to cope with auto-generated JSON field names as well.

[Sebastian Ullrich]

Added print-paths JSON & Lake support to the Lake PR, not thoroughly tested

[Sebastian Ullrich]

I don't want the server to judge whether a project has Lake set up, so I'm assuming Lake will respond with empty output if that is not the case, like leanpkg

[Sebastian Ullrich]

If you want to test it with an external Lake, I'd suggest copying it into Lean's bin/... do we need a LAKE_PATH env var separate from LEAN_SYSROOT to make that easier?

[Mac]

@Sebastian Ullrich the structure uses sourcePath(i.e., spells out 'source') but its uses use srcPath -- how does that work?

[Mac]

I am fine with the short spelling src if that is what you would prefer

[Mac]

@Sebastian Ullrich also, from, the CI results you appear to have missed renaming a leanpkgProc somewhere.

[Sebastian Ullrich]

Huh, I must have pushed the wrong commit somehow

[Sebastian Ullrich]

Should be good now. I hope.

[Mac]

@Sebastian Ullrich it builds, but sadly many of the interactive test are now broken for some reason. Could it be because they lack both a leanpkg.toml and/or a lakefile.lean?

[Sebastian Ullrich]

I'll fix it tomorrow

[Mac]

@Sebastian Ullrich fyi, I did update Lake to mirror the JSON syntax the server is now using, so an up-to-date should (hopefully) work with the server changes

[Sebastian Ullrich]

Sebastian Ullrich said:

I don't want the server to judge whether a project has Lake set up, so I'm assuming Lake will respond with empty output if that is not the case, like leanpkg

@Mac This is not the case yet, is it? The tests are failing because of that

    "`/home/sebastian/lean/lean/build/release/stage1/bin/lake print-paths` failed:\n\nstderr:\nerror: no such file or directory (error code: 2)\n  file: ./lakefile.lean\n",

[Mac]

Sebastian Ullrich said:

Sebastian Ullrich said:

I don't want the server to judge whether a project has Lake set up, so I'm assuming Lake will respond with empty output if that is not the case, like leanpkg

Mac This is not the case yet, is it? The tests are failing because of that

    "`/home/sebastian/lean/lean/build/release/stage1/bin/lake print-paths` failed:\n\nstderr:\nerror: no such file or directory (error code: 2)\n  file: ./lakefile.lean\n",

No, I guess misunderstood what you meant by that. I thought you meant that it would output nothing to stdout (which it does not). I strikes me as very weird for a Lake command to silently succeed when there is no lakefile and it did nothing.

[Mac]

However, if you think that is best. I can make it do that. Since print-paths is a non-public command I don't feel that strongly about it.

[Sebastian Ullrich]

I'm also open to a special return code, but as you said it doesn't matter much

[Mac]

Sebastian Ullrich said:

I'm also open to a special return code

I actually quite like that solution! That way the distinction is not completely undetectable. Any particular preference which code to use?

[Sebastian Ullrich]

No :)

[Mac]

@Sebastian Ullrich pushed, I went with the very uncreative code of 2. XD

[Sebastian Ullrich]

Then we think alike :laughing:

[Mac]

Sebastian Ullrich said:

If you want to test it with an external Lake, I'd suggest copying it into Lean's bin/... do we need a LAKE_PATH env var separate from LEAN_SYSROOT to make that easier?

Also, I meant to mention this earlier, but forgot. I do think a LAKE_PATH (or, ideally, just LAKE) environment variable for configuring the Lake the Lean 4 server uses would be a good idea.

[Sebastian Ullrich]

done

[Mac]

@Sebastian Ullrich sounds great! what are the plans for when to merge the PR?

[Sebastian Ullrich]

I think we're only missing elan support

[Sebastian Ullrich]

Feel free to test-drive the CI artifact

[Mac]

@Sebastian Ullrich I gave it and go and it appears to be broken :sad: . The server running print-paths through either leanpkg or lake breaks with the error "expected JSON array, got 'null'".

[Mac]

I believe the change I suggest in the PR may fix this.

[Mac]

While attempting to debug that issue, I also discovered (and fixed) at least one bug of my own in Lake. So the Lake submodule will also need a bump.

[Sebastian Ullrich]

Pushed the JSON changes, now tested once more, to master

[Sebastian Ullrich]

elan 1.1.0 with support for lake has been released

[Sebastian Ullrich]

Added some hints to make living with submodules easier :) https://github.com/leanprover/lean4/pull/683/commits/86cf1ceb0bb5b9280f2122e6895e9d99043817af /cc @Leonardo de Moura

[Sebastian Ullrich]

I can't think of anything else that should be done before merging the PR

[Julian Berman]

(If it's not too bikeshedy or controversial, subtrees are better than submodules IMHO --though still have a problem or two of their own if you mix a commit that touches lean and lake at the same time and want to now push to lake--, but they mean someone cloning the lean4 repo wouldn't need to know it vendors the lake repo)

[Sebastian Ullrich]

I didn't know that git subtree can squash the history, to be honest. One tenuous argument for a Lake submodule is that we were considering to eventually put stage0/ into a shallow submodule to drastically reduce the size of the repo.

[Julian Berman]

Yeah, the squashing is very convenient.

[Julian Berman]

I've been using one for ~8+ years on a pair of repos I manage (here: https://github.com/Julian/jsonschema/tree/main/json) and you can see each time it's a single easy to understand commit.

[Mac]

Sebastian Ullrich said:

I can't think of anything else that should be done before merging the PR

I'd wait until at least tomorrow to merge it. That way I can update Lake to use LeanPaths and test it on today's nightly. Then the Lake submodule can be updated and the PR merged tomorrow so Lake is available in that nightly's release.