Skip to content

Commit

Permalink
Update README.md
Browse files Browse the repository at this point in the history
  • Loading branch information
@yangky11
yangky11 authored Dec 30, 2024
1 parent aa07d21 commit 1c84b5b
Showing 1 changed file with 5 additions and 6 deletions.
11 changes: 5 additions & 6 deletions README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -71,12 +71,11 @@ rev = "LEAN_COPILOT_VERSION"
3. Run `lake update LeanCopilot`.

4. Run `lake exe LeanCopilot/download` to download the built-in models from Hugging Face to `~/.cache/lean_copilot/`. *Alternatively*, you can download the models from Hugging Face manually from
```url
"https://huggingface.co/kaiyuy/ct2-leandojo-lean4-tacgen-byt5-small"
"https://huggingface.co/kaiyuy/ct2-leandojo-lean4-retriever-byt5-small"
"https://huggingface.co/kaiyuy/premise-embeddings-leandojo-lean4-retriever-byt5-small"
"https://huggingface.co/kaiyuy/ct2-byt5-small"
```
* [ct2-leandojo-lean4-tacgen-byt5-small](https://huggingface.co/kaiyuy/ct2-leandojo-lean4-tacgen-byt5-small)
* [ct2-leandojo-lean4-retriever-byt5-small](https://huggingface.co/kaiyuy/ct2-leandojo-lean4-retriever-byt5-small)
* [premise-embeddings-leandojo-lean4-retriever-byt5-small](https://huggingface.co/kaiyuy/premise-embeddings-leandojo-lean4-retriever-byt5-small)
* [ct2-byt5-small](https://huggingface.co/kaiyuy/ct2-byt5-small)


5. Run `lake build`.

Expand Down

0 comments on commit 1c84b5b

Please sign in to comment.