From 82badd6cee172b480c31c69cd921b40c613dec81 Mon Sep 17 00:00:00 2001
From: Kaiyu Yang <kaiyuy@caltech.edu>
Date: Mon, 4 Dec 2023 06:00:50 -0800
Subject: [PATCH] Update README.md

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 97c2501..188eb02 100644
--- a/README.md
+++ b/README.md
@@ -19,7 +19,7 @@ LeanInfer provides tactic suggestions by running LLMs through Lean's foreign fun
 
 1. Add the package configuration option `moreLinkArgs := #["-L./.lake/packages/LeanInfer/.lake/build/lib", "-lonnxruntime", "-lctranslate2"]` to lakefile.lean. Also add LeanInfer as a dependency:
 ```lean
-require LeanInfer from git "https://github.com/lean-dojo/LeanInfer.git" @ "v0.0.9"
+require LeanInfer from git "https://github.com/lean-dojo/LeanInfer.git" @ "v0.1.0"
 ```
 2. Run `lake update LeanInfer`
 3. Run `lake script run LeanInfer/download` to download the models from Hugging Face to `~/.cache/lean_infer/`