setting copilot

Author: yoh-tanimoto

lakefile.lean

@@ -14,6 +14,7 @@ require "leanprover-community" / "proofwidgets" @ git "v0.0.48"
 require "leanprover-community" / "importGraph" @ git "v4.15.0-rc1"
 require "leanprover-community" / "LeanSearchClient" @ git "main"
 require "leanprover-community" / "plausible" @ git "v4.15.0-rc1"
+require LeanCopilot from git "https://github.com/lean-dojo/LeanCopilot.git" @ "v4.15.0"
 
 /-!
 ## Options for building mathlib
@@ -55,6 +56,10 @@ package mathlib where
   -- Warning: Do not put any options here that actually change the olean files,
   -- or inconsistent behavior may result
   -- weakLeanArgs := #[]
+  moreLinkArgs := #[
+    "-L./.lake/packages/LeanCopilot/.lake/build/lib",
+    "-lctranslate2"
+  ]
 
 /-!
 ## Mathlib libraries

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.15.0-rc1
+leanprover/lean4:v4.15.0