Merge branch 'main' of github.com:lean-dojo/LeanInfer into main

Dockerfile

@@ -4,7 +4,7 @@ WORKDIR /LeanInfer
 COPY . .
 
 # Install dependencies.
-RUN apt-get update && apt-get install -y curl wget git git-lfs cmake clang lld libc++-dev libopenblas-dev
+RUN apt-get update && apt-get install -y curl wget git git-lfs cmake clang lld libc++-dev
 RUN git lfs update --force
 
 # Install elan.

LeanInfer/Cache.lean

@@ -11,7 +11,7 @@ private def getHomeDir : IO FilePath := do
   return dir
 
 
-private def ensureExists (dir : FilePath) : IO Unit := do
+private def ensureDirExists (dir : FilePath) : IO Unit := do
   if !(← dir.pathExists)  then
     IO.FS.createDirAll dir
 
@@ -25,7 +25,7 @@ def getCacheDir : IO FilePath := do
   let dir := match ← IO.getEnv "LEAN_INFER_CACHE_DIR" with
   | some dir => (dir : FilePath)
   | none => defaultCacheDir
-  ensureExists dir
+  ensureDirExists dir
   return dir.normalize
 
 

LeanInferTests/Examples.lean

@@ -33,3 +33,8 @@ example (a b c : Nat) : a + b + c = a + c + b := by
 example (a b c : Nat) : a + b + c = a + c + b := by
   suggest_tactics "rw"  -- You may provide a prefix to constrain the generated tactics.
   sorry
+
+
+example (a b c : Nat) : a + b + c = a + c + b := by
+  select_premises
+  sorry

README.md

@@ -10,21 +10,16 @@ LeanInfer provides tactic suggestions by running LLMs through Lean's foreign fun
 
 * Supported platforms: Linux and macOS (:warning: maybe also Windows WSL, but untested)
 * Git LFS
-* A C++17 compatible compiler, e.g., recent versions of GCC or Clang
-* CMake >= 3.7
-* At least one of [MKL](https://www.intel.com/content/www/us/en/developer/tools/oneapi/onemkl.html), [Accelerate](https://developer.apple.com/documentation/accelerate), [DNNL](https://github.com/oneapi-src/oneDNN), or [OpenBLAS](https://www.openblas.net/). Most systems have them pre-installed, so you may not need to do anything. However, if you see the error `No BLAS library found`, it means you don't have any of these libraries. In that case, we recommend MKL for Intel CPUs, Accelerate for Apple, and DNNL for AMD CPUs. OpenBLAS is cross-platform and can be used as a last resort if you cannot install the others. We are happy to help if you have trouble installing these libraries.
 * Optional (recommended if you have a [CUDA-enabled GPU](https://developer.nvidia.com/cuda-gpus)): CUDA and [cuDNN](https://developer.nvidia.com/cudnn)
 
-**Please run `lake script run LeanInfer/check` to check if the requirements have been satisfied.**
-
 
 ## Adding LeanInfer as a Dependency to Your Project
 
 :warning: Your package must use a Lean version of at least `lean4:v4.3.0-rc2`.
 
 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" @ "main"
+require LeanInfer from git "https://github.com/lean-dojo/LeanInfer.git" @ "v0.0.9"
 ```
 2. Run `lake update LeanInfer`
 3. Run `lake script run LeanInfer/download` to download the models from Hugging Face to `~/.cache/lean_infer/`