Recommended way to install a package from Reservoir?

Stream: new members

[Isak Colboubrani]

What is the recommended method to install a package from Reservoir (https://reservoir.lean-lang.org) using the command line?

And how should it be done within VS Code (with the Lean extension installed)?

For example, if you have a Reservoir package named foo, is there a command equivalent to pip install foo in the Python world?

Currently, I'm using the following approach:

% echo '[[require]]' >> lakefile.toml
% echo 'name = "<foo>"' >> lakefile.toml
% echo 'git = "<some git repo for foo>"' >> lakefile.toml
% lake update foo

[Arthur Paulino]

The current readme doesn't mention a CLI command for this. I don't think it's possible as of today

[Julian Berman]

https://github.com/leanprover/lean4/issues/5453 is I think the relevant issue to follow. I'll just note though that in the interim there's no reason to run multiple shell commands, you can just do it all at once.

[Isak Colboubrani]

I read the Lake README.md and if I understand it correct the way to install a Reservoir package @bar/foo the recommended way would be:

% (echo '[[require]]'; echo 'name = "foo"'; echo 'scope = "bar"') >> lakefile.toml
% lake update foo

Sounds about right?

[Julian Berman]

Sorry I was just pointing out a silly shell thing, there's nothing wrong with what you have -- what I meant was you can just do:

% >>lakefile.toml printf '

[[require]]
name = "bar"
scope = "baz"
'

(or echo if you prefer.) and that looks a bit more "normal".

Or even if you're really annoyed by this:

lake-add() { >>lakefile.toml printf '\n[[require]]\nscope = "'$1'"\nname = "'$2'"\n' }

and then you can run lake-add leanprover-community mathlib4.

[Isak Colboubrani]

I’m picturing something similar to cargo install foo, pip install foo, or npm install foo.

Would it be useful to have a command like lake install baz/bar to install the Reservoir package baz/bar (it seems like Reservoir packages are always scoped)?

And if so, does it make sense for the install subcommand to fall under the lake command, or is there a better place?

In the simplest scenario, that command would do the equivalent of (echo '[[require]]'; echo 'name = "bar"'; echo 'scope = "baz"') >> lakefile.toml && lake update bar (modulo idempotence).

[Julian Berman]

I'm not sure I see the relation between "add a dependency" and "globally install a piece of software which happens to be written in Lean out of Reservoir", but yes I'd bet both of those are on the roadmap. The former is the issue I linked. And the latter I think is somewhere on the issue tracker as well but I'm not finding it at the minute.

[Isak Colboubrani]

@Julian Berman Oh, I'm specifically talking about "add a dependency" from Reservoir" (which is the only case I've ever had a need for).

I'm not entirely sure I understand: are you suggesting that lake install baz/bar would be "globally install a piece of software which happens to be written in Lean out of Reservoir"?

If so, would lake add baz/bar be a more suitable command for "add a dependency"?

(Update: I now realize that I wrote "install the Reservoir package baz/bar" in the previous message when I meant to say "install locally in the repository as a dependency" — or, more precisely, "add as a dependency". Sorry about that.)

[Julian Berman]

Got it, sorry, the confusing thing to me was that those 3 package manager commands do 3 slightly different things from "add a dependency to the packaging manifest" -- that'd be cargo add, uv add (pip doesn't have such a thing) and pnpm add (or fine npm install --save if you're using last month's package manager :)

[Julian Berman]

Anyways yeah I linked to the issue on lake add, you should thumbs up it, and I'm sure at some point it's on the agenda.