How to use with lakefile.toml?

[alok]

The instructions are for lakefile.lean but lake new now uses a TOML file and the syntax for local deps is unclear.

[sonmarcho]

Indeed, I hadn't noticed the change. You just need to set up the path to the standard library of Aeneas properly.
I think something like base = { path = "PATH_TO_AENEAS/backends/lean" } should work.