Syntax of toml files

Stream: lean4

[Antoine Chambert-Loir]

I have tried to switch the lakefile.lean file of a mathlib4-dependent project to a lakefile.toml, but the following does not seem to be sufficient, because lake apparently can't compile the import that are within the Jordan subdirectory.

name = "Jordan"

[[require]]
name = "mathlib"
scope = "leanprover-community"

[Julian Berman]

You need to also convert your lean_lib definition. I think running lake translate-config toml seems to produce the right output for your repo