Zulip Chat Archive
Stream: new members
Topic: leancopilot
stark (Jan 12 2024 at 14:56):
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 (Jan 12 2024 at 16:14):
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.
Last updated: May 02 2025 at 03:31 UTC