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