Support different "environments" / non-mandatory dependencies

[Julian]

(I'm assuming this has at least been thought about, but filing it since I don't see another place tracking it).

I'd like to add a dev dependency which isn't/shouldn't be required by users of my thing. It would be nice to have syntax in a lakefile to create separate environments with their own dependencies (and perhaps subcommands or scripts only relevant to them), so a "testing" environment, where I'd declare a dependency on LSpec and some testing related commands, a "dev" environment where I'd install some future nice development tools, and then a "normal" environment which end-users use.

[tydeu]

I thought about this some more and have a question: How do you propose setting the environment Lake uses? Are you envisioning having to pass a flag e.g., -Edev to every Lake CLI invocation? Or is there some way you think this could be persisted across invocations?

[Julian]

I'm recently quite enamored with how hatch does this, which is our cool new Python ecosystem tool. It supports both dropping into an activated shell or separately also explicitly passing the name of the environment as an argument or envvar.

[tydeu]

@Julian I am a little confused as to how that would apply here. I imagine the goal here is not to run a shell (as this issue, at least as far as I understand, is about dependency sets), so what are you envisioning as the Lake equivalent?

[Julian]

I sort of mixed the two (dependency sets and environment-specific commands) in the issue description and title, because they're quite related.

Concretely, if I just make up some lakefile syntax for a minute, given:

import Lake

open Lake DSL

package Scratch

@[defaultTarget] lean_lib Scratch

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git"@"master"

environment testing do
  require lspec from git
    "https://github.com/yatima-inc/lspec"@"master"

  script greet (args) do
    if h : 0 < args.length then
      IO.println s!"Hello, {args.get 0 h}!"
    else
      IO.println "Hello, world!"
    return 0

I now have 2 environments, a default one and a testing one with one additional dependency and a script that works only within it.

Running lake exe scratch runs scratch from the default environment, but now lake exe -e testing lspec should run lspec from within the testing env.

Or for the script, similarly, lake run -e testing greet.

Of course running lake run lspec or lake exe lspec fails, as it's not installed in the default environment.

Where a shell comes in is if you want to allow someone to be able to run 10 commands in a row within an environment foo without needing to continually write lake exe -e foo -- they instead run lake shell -e foo once, and now within that subshell would get essentially just a LAKE_ENV=foo environment variable set, so now they can run lake run lspec and that automatically means lake run -e lspec.

The last part with a shell is for me personally not top priority relative to the other, I never use it in Python, but it's undoubtedly extremely popular, so I mentioned it given your question about

Or is there some way you think this could be persisted across invocations?

Does that help?

[tydeu]

@Julian okay, that helps. Note that you can already pass options to a Lake configuration via -Kopt=val and then you could do some elaboration magic to execute a part of the configuration based on such a setting. For example, using the meta if helper I just pushed. your example could be implemented like so:

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git"@"master"

meta if get_config? env = "testing" then
require lspec from git  "https://github.com/yatima-inc/lspec"@"master"

meta if get_config? env = "testing" then
script greet (args) do
 -- ...

Then running lake -Kenv=testing <cmd> would depend on lspec and make greet available whereas not passing it would not. Would that be sufficient, or are there other features to environments you would like to see?

[Julian]

Ah nice. That indeed would seem like it'd get reasonably far. I don't know much about lake's internals but if you had conflicting dependency versions -- e.g. if an environment "foo" depends transitively on quux-dependency v1 and env "bar" depends transitively on quux-dependency v0.5 -- will runs of lake -Kenv=foo and lake -Kenv=bar continually hit the network and fight each other installing the corresponding version of quux-dependency each time? Or will it just pull both versions and store them and then properly use the right one each time?

If the above works too then yeah I think that likely does get quite far and maybe just could be documented as the way to do this with no real extra support.

[tydeu]

@Julian

will runs of lake -Kenv=foo and lake -Kenv=bar continually hit the network and fight each other installing the corresponding version of quux-dependency each time? Or will it just pull both versions and store them and then properly use the right one each time?

They would not fight but they would also not select the right one each time. They would end up on which ever one was installed first. However, Lean itself, at the moment, doesn't really support competing versions of used modules in the first place (i.e., you would need to rebuild all dependent code every time you swapped back and forth). So, unless the code in environment foo and bar were entirely independent (in which case they could probably be separate packages), it is unlikely the package would cleanly compile in both environments anyway.

[Julian]

Aha, got it. Good to know, thanks for explaining. Certainly I'm happy if you close this then and we see how things go with the meta if helper, maybe it's enough until some more intricate need arises -- though possibly mentioning it in the README would be helpful?

[tydeu]

The Lake repository is being deprecated and its issues transferred to leanprover/lean4. As meta if did solve this problem initially and leanprover/lean4#2755 is a newer issue that tracks some problems with that solution, I transferred that issue and am closing this.