deps added from 2 lakefiles.

Stream: lean4

[Alok Singh]

In a repository, I have both a lakefile.toml and a lakefile.lean. I observed that the .lean file takes precedence over the .toml file. However, if I add a dependency (specifically, Mathlib) to the toml file, it will be added to dependencies instead of being ignored.

[Kevin Buzzard]

I should think that having both is a recipe for disaster

[Michael Rothgang]

Can you just delete one of them? That seems like a better solution for the medium- to long term.

[Alok Singh]

I already deleted it. The thing is that it says the lean file overrides the toml, so I expected it to do that. So I figured I'd report this behavior first

[Mac Malone]

@Alok Singh This is definitely a bug worth reporting as an issue on the GitHub if you have the time.

[Mac Malone]

I am definitely confused as to how this could occur -- there is nothing in Lake that to merge the two files. Thus,, debugging this should be interesting.