Lake dependency graph command similar to `cargo tree`

Stream: lean4 dev

[Austin Letson]

What do others think of a Lake command that uses the Lake workspace to generate and display a dependency tree, similar to cargo tree? Is something like this in the current roadmap? Or am I missing an existing alternative?

This seems like it could be generally useful for troubleshooting and integration with other tools. I know of two specific places where this would be useful to have easy access to Lake dependencies:

• detecting Mathlib dependencies in lean-action (currently done brittlely by greping lakefile.lean and lakefile.toml)
• detecting default target for running the std linter (I am trying to do this using Lake's internal API, but there are downsides to that approach raised by @Kim Morrison here)

[Shreyas Srinivas]

It's a nice feature just in general. Very useful even in moderately sized formalisation projects

[Mac Malone]

Currently, the best way to do this is to read the Lake manifest. Regardless, adding a command like this is definitely a reasonable feature request. I am not sure how soon it would be addressed, though.

[Austin Letson]

Mac Malone said:

Currently, the best way to do this is to read the Lake manifest. Regardless, adding a command like this is definitely a reasonable feature request. I am not sure how soon it would be addressed, though.

Ah, thanks for the tip to use the Lake manifest. I need to look into how this would work for detecting Mathlib dependency since you want to run lake exe cache get before running lake build. I am realizing now, I can just run lake update to generate the manifest before running lake exe cache get.

[Mac Malone]

@Austin Letson You should only run lake update if the manifest does not already exist. The primary purpose of the manifest is to lock dependencies to a specific version for things like CI, which a lake update undoes (unless, of course, the manifest does not already exist).

[Austin Letson]

:thumbs_up: Okay, I will create an issue to add a step in lean-action that checks to see if the manifest exists and runs lake update before reading the manifest. This is likely an edge case in practice, however, when testing lean-action it is common for the manifest to not exist because I will run lake new test or lake new test math and then immediately run lean-action.

[Jannis Limperg]

A manifest that's not checked into the Git repo is most likely a mistake. So imo lean-action should treat this as an error rather than generate the manifest.

[Austin Letson]

Jannis Limperg said:

A manifest that's not checked into the Git repo is most likely a mistake. So imo lean-action should treat this as an error rather than generate the manifest.

The lack of a manifest does seem like an edge case. My assumption here was that lean-action should work on a fresh lake new without generating an error. However, we could add an error that says something like "you must run lake build to generate a lake manifest". @Mac Malone what do you think?

[Jannis Limperg]

I think lake update would be the minimal command that generates a manifest. One could maybe also adjust lake new to run lake update. Any of these solutions would be good imo.

[Austin Letson]

Sounds good. I have updated the issue on lean-action to log an error suggesting the user run lake update if there is no manifest.