lake
lake copied to clipboard
Support different "environments" / non-mandatory dependencies
(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.
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?
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.
@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?
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?
@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?
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.
@Julian
will runs of
lake -Kenv=foo
andlake -Kenv=bar
continually hit the network and fight each other installing the corresponding version ofquux-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.
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?
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.