lake CLI add dependency

Stream: lean4

[Jakob von Raumer]

Is there a way to add a dependency to a project via the command line? Like what lake new ... math does, but with math generalized to an arbitrary dependency?

[Kim Morrison]

No, you need to edit your lakefile.toml/lean.

[Jakob von Raumer]

Thanks (this is not about manual edits but about generation of Lake projects by a script, so would have been nice if we could have just called the command line tool instead of writing around in the lakefile.lean..)

[Kim Morrison]

I agree! lean#5453

[Sebastian Ullrich]

(for a very generic solution, yq can edit TOML files programmatically)

[Jakob von Raumer]

Is lakefile.lean still valid TOML? :thinking:

[Henrik Böving]

No you are supposed to rewrite the file to TOML/Lean or use lake translate-config if possible

[Jakob von Raumer]

Thanks, that didn't know translate-config!

[Kim Morrison]

Hopefully by the next release (depending on how @Mac Malone prioritises things) new projects will all start out with a TOML and life will start getting simpler from there.

[Jakob von Raumer]

Im out of the loop here: Didn't we switch from .toml to .lean in the earlier days of Lake for some reason? (Or was that even before Lake was a thing?)

[Patrick Massot]

You can still use lakefile.lean for really complicated projects.