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.

[alok]

It’s out of date in another way since the package was renamed from base too. A coworker had trouble with that one

[sonmarcho]

Yes, I updated the name of the package to Aeneas. But it doesn't significantly change the shape of the instruction you have to put in the Cargo.toml: you should use aeneas = ... instead of base = ....