lakefile lean vs toml

Stream: lean4

[Patrick Massot]

@Mac Malone could you clarify whether having both a lakefile.lean and a lakefile.toml in the same project makes any sense, and what lake is meant to do in the case? I am asking because I want to decide what to do in that case for other tools (in my case leanblueprint).

[Mac Malone]

At the moment, it is not expected that user projects will have both a lakefile.lean and a lakefile.toml. Currently, if both exist, Lake perfers the lakefile.lean. However, there are plans down the road to evolve this behavior to instead merge the contents of the two,. Thus. it is probable that future projects will make use of both. I don't expect this to happen for a least a few months, though.

[Shreyas Srinivas]

Can new projects be initialised with lakefile.toml by default?

[Patrick Massot]

Ok thanks, I'll try to support having both without warning users that something is weird.

[Mac Malone]

@Patrick Massot I think a warning is fine. Lake itself currently produces a warning noting the existence of both and indicating it will use lakefile.lean.

[Mac Malone]

Shreyas Srinivas said:

Can new projects be initialised with lakefile.toml by default?

Are you asking whether you can genearte lakefile.toml from lake new? If so, yes, via lake new <proj> .toml. If you are asking whether lakefile.toml will be made the default, that is lean4#4106. It probably won't happen until the merger I mentioned or, alternatively, once mathlib is ported to TOMl.

[Shreyas Srinivas]

I meant the latter but the former is a good solution for the months ahead