leanpkg `path` setting

Stream: lean4

[Mac]

What is the path setting in a leanpkg.toml file suppose to do (i.e. what is it used for)?

[Sebastian Ullrich]

Lean 3 leftover, we should probably remove it. I'd rather have something like Cargo's workspaces to enable more dynamic directory layouts.

[Kevin Buzzard]

I had no understanding of the discussion about plugins / repos containing more than one library earlier, but is this related to it?

[Mac]

Sebastian Ullrich said:

Lean 3 leftover, we should probably remove it. I'd rather have something like Cargo's workspaces to enable more dynamic directory layouts.

Okay! That's great! now I don't feel bad about mucking around with it. :smile:

[Sebastian Ullrich]

Kevin Buzzard said:

I had no understanding of the discussion about plugins / repos containing more than one library earlier, but is this related to it?

Not really I'd say; since you can have only one leanpkg.toml per directory and exactly one package per leanpkg.toml, you'll first have to find a place for those in a multi-package repo. When you've done that, or changed the format to allow for multiple packages in a single directory, there is still no reason to place the source code at a nonstandard location relative to its leanpkg.toml file.