Skip to content

Commit

Permalink
Update README.md
Browse files Browse the repository at this point in the history
  • Loading branch information
Kaiyu Yang authored Jan 17, 2024
1 parent 73057bf commit 04204f7
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@ https://github.com/lean-dojo/LeanCopilot/assets/5431913/7742545f-e194-45fa-b744-

1. Add the package configuration option `moreLinkArgs := #["-L./.lake/packages/LeanCopilot/.lake/build/lib", "-lctranslate2"]` to lakefile.lean. Also add the following line:
```lean
require LeanCopilot from git "https://github.com/lean-dojo/LeanCopilot.git" @ "v1.0.2"
require LeanCopilot from git "https://github.com/lean-dojo/LeanCopilot.git" @ "v1.1.0"
```
3. Run `lake update LeanCopilot`
4. Run `lake exe LeanCopilot/download` to download the built-in models from Hugging Face to `~/.cache/lean_copilot/`
Expand Down

0 comments on commit 04204f7

Please sign in to comment.