Skip to content

Commit

Permalink
Update README.md
Browse files Browse the repository at this point in the history
  • Loading branch information
yangky11 authored Dec 25, 2024
1 parent 5589a25 commit 5afd874
Showing 1 changed file with 8 additions and 1 deletion.
9 changes: 8 additions & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -52,7 +52,7 @@ package «my-package» {
}
```
Alternatively, if your project uses lakefile.toml, it should include:
```
```toml
moreLinkArgs = ["-L./.lake/packages/LeanCopilot/.lake/build/lib", "-lctranslate2"]
```

Expand All @@ -61,6 +61,13 @@ moreLinkArgs = ["-L./.lake/packages/LeanCopilot/.lake/build/lib", "-lctranslate2
require LeanCopilot from git "https://github.com/lean-dojo/LeanCopilot.git" @ "LEAN_COPILOT_VERSION"
```
`LEAN_COPILOT_VERSION` must match with your lean-toolchain.
If your project uses lakefile.toml, it should include:
```toml
[[require]]
name = "LeanCopilot"
git = "https://github.com/lean-dojo/LeanCopilot.git"
rev = "LEAN_COPILOT_VERSION"
```

3. Run `lake update LeanCopilot`.

Expand Down

0 comments on commit 5afd874

Please sign in to comment.