leancopilot

Stream: new members

[stark]

Hello, I just tried to install leancopilot on my machine. The guide says 'Add the package configuration option moreLinkArgs := #["-L./.lake/packages/LeanCopilot/.lake/build/lib", "-lctranslate2"] to lakefile.lean'. But there are many lakefile.lean under .elan. Which one should I add this configuration?

[Mauricio Collares]

I assume you don't have a project yet. You'll have to create one with lake new ProjectName math to add dependencies. Then you can edit the project's Lakefile as instructed above.