From 5e5b19486d8b850aa4f3f3169e95de560f39b2f8 Mon Sep 17 00:00:00 2001 From: Kaiyu Yang Date: Thu, 21 Dec 2023 18:19:03 -0800 Subject: [PATCH] bump to v1.0.1 --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index c39d823..e6110a7 100644 --- a/README.md +++ b/README.md @@ -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.0" +require LeanCopilot from git "https://github.com/lean-dojo/LeanCopilot.git" @ "v1.0.1" ``` 3. Run `lake update LeanCopilot` 4. Run `lake exe LeanCopilot/download` to download the built-in models from Hugging Face to `~/.cache/lean_copilot/`