lakefile.lean and lakefile.toml are both present

Stream: new members

[Lars Ericson]

I get this message in my project:

info: [root]: lakefile.lean and lakefile.toml are both present; using lakefile.lean

Is it safe to delete lakefile.toml from my project/github repo? Is it obsolete?

[Mauricio Collares]

Ideally you'd just have lakefile.toml, unless you need the extra "expressive power" lakefile.lean provides.

[Mauricio Collares]

lakefile.toml is the new kid on the block. It is not obsolete.

[Lars Ericson]

I am working on a fork of @Alex Oltean's github which was written in year-and-a-half-ago Lean 4 and I am using today Lean 4. The original github has only lakefile.lean. I did a lake update mathlib or something similar inside VS Code and the lakefile.toml file appeared. I don't need any additional expressive power. The info message is telling me that it prefers the older file which means I guess that it is ignoring the newer one. I would like to get my setup to a state where the setup is "clean" from Lean's point of view.

@Mauricio Collares I will try deleting the lakefile.lean and see if it picks up the lakefile.toml and continues to be happy.

[Ruben Van de Velde]

I'm very surprised that anything would create the toml file automatically. You don't happen to have steps that reproduce this behaviour?

[Lars Ericson]

I did something a little convoluted. I wanted to create an environment that was totally up to date and copy into that the old application code that needed to be brought up to date:

1. I forked the old github
2. I cloned it on my machine
3. I deleted the Lean config files and just left the folder with the Lean application code
4. In a different folder, inside VS Code, I did something like this, which I'm pretty sure resulted in both a lakefile.lean and a lakefile.toml file:

>Lean 4: Project: Create project using Mathlib...

4. I copied the resulting up-to-date config files into my Github clone.

[Julian Berman]

Is it possible you copied the lakefile.lean back in? The default Mathlib template will generate a lakefile.toml.

[Lars Ericson]

Yes. I will try just deleting it and see if it is still happy.

[Lars Ericson]

Taking out the lakefile.lean makes it very unhappy. It can't find and recompile separate files that are used in import statements in the directory. Putting it back it is more happy. I don't know what this file does or how to program it. Here are the contents:

import Lake
open Lake DSL

package hybrid {
  -- add package configuration options here
}

lean_lib Hybrid {
  -- add library configuration options here
}

@[default_target]
lean_lib hybrid

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git"

[Lars Ericson]

So I'll just leave it in and the toml file too for future compatibility.

[Lars Ericson]

Actually in the end it seems happy without the lakefile.toml file so I'll just delete that one for now since it is preferring the lakefile.lean file.