diff --git a/README.md b/README.md index a6d5915..d3f3a9e 100644 --- a/README.md +++ b/README.md @@ -20,6 +20,7 @@ Lean Copilot allows large language models (LLMs) to be used natively in Lean for 1. [Tactic APIs](#tactic-apis) 1. [Model APIs](#model-apis) 1. [Bring Your Own Model](#bring-your-own-model) + 1. [Using Prebuilt System Libraries](#using-prebuilt-system-libraries) 1. [Caveats](#caveats) 1. [Getting in Touch](#getting-in-touch) 1. [Acknowledgements](#acknowledgements) @@ -30,7 +31,7 @@ Lean Copilot allows large language models (LLMs) to be used natively in Lean for * Supported platforms: Linux (priority), macOS (priority), Windows and [Windows WSL](https://learn.microsoft.com/en-us/windows/wsl/install). * [Git LFS](https://git-lfs.com/). * Optional (recommended if you have a [CUDA-enabled GPU](https://developer.nvidia.com/cuda-gpus)): CUDA and [cuDNN](https://developer.nvidia.com/cudnn). -* Required for building Lean Copilot itself (rather than a downstream package): CMake >= 3.7 and a C++17 compatible compiler. +* Required for building Lean Copilot itself (rather than a downstream package): CMake >= 3.7 and a C++17 compatible compiler. A downstream package normally downloads a prebuilt release instead of needing these, *except* on a platform we don't publish a release for (e.g. Intel macOS), where it automatically falls back to building from source and so needs them too. ## Using Lean Copilot in Your Project @@ -61,7 +62,7 @@ moreLinkArgs = ["-L./.lake/packages/LeanCopilot/.lake/build/lib", "-lctranslate2 require LeanCopilot from git "https://github.com/lean-dojo/LeanCopilot.git" @ "LEAN_COPILOT_VERSION" ``` -For stable Lean versions (e.g., `v4.32.0`), set `LEAN_COPILOT_VERSION` to be that version. For the latest unstable Lean versions (e.g., `v4.33.0-rc1`), set `LEAN_COPILOT_VERSION` to `main`. In either case, make sure the version is compatible with other dependencies such as mathlib. If your project uses lakefile.toml instead of lakefile.lean, it should include: +For stable Lean versions (e.g., `v4.33.0`), set `LEAN_COPILOT_VERSION` to be that version. For the latest unstable Lean versions (e.g., `v4.34.0-rc1`), set `LEAN_COPILOT_VERSION` to `main`. In either case, make sure the version is compatible with other dependencies such as mathlib. If your project uses lakefile.toml instead of lakefile.lean, it should include: ```toml [[require]] @@ -162,6 +163,22 @@ Similar to generators, we have `NativeEncoder`, `ExternalEncoder`, and `GenericE In principle, it is possible to run any model using Lean Copilot through `ExternalGenerator` or `ExternalEncoder` (examples in [ModelAPIs.lean](LeanCopilotTests/ModelAPIs.lean)). To use a model, you need to wrap it properly to expose the APIs in [external_model_api.yaml](./external_model_api.yaml). As an example, we provide a [Python API server](./python) and use it to run a few models. +### Using Prebuilt System Libraries + +By default, building Lean Copilot from source clones and compiles its native dependencies, OpenBLAS and CTranslate2, which can be slow or awkward on systems (e.g., Nix-based distros) that already package these libraries or make it difficult to compile them from source. If you already have compatible builds available, you can point Lean Copilot at them instead with `lake`'s `-K` flag (add `-R` too if you already have a `.lake/build` from a previous build, so that the new options take effect): + +* `-KsystemOpenblas=` skips cloning and building OpenBLAS (Linux/Windows only; macOS uses Apple's Accelerate framework instead of OpenBLAS). +* `-KsystemCtranslate2Lib=` together with `-KsystemCtranslate2Include=` skips cloning and building CTranslate2. + +For example, on Linux: + +```sh +lake -R -KsystemOpenblas=/usr/lib/libopenblas.so \ + -KsystemCtranslate2Lib=/usr/lib/libctranslate2.so \ + -KsystemCtranslate2Include=/usr/include \ + build +``` + ## Caveats * `select_premises` always retrieves the original form of a premise. For example, `Nat.add_left_comm` is a result of the theorem below. In this case, `select_premises` retrieves `Nat.mul_left_comm` instead of `Nat.add_left_comm`. diff --git a/lake-manifest.json b/lake-manifest.json index c056302..9a2cecd 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,20 +5,20 @@ "type": "git", "subDir": null, "scope": "", - "rev": "a7dbf0c63b694e47f425f3dcddbc0e178bb432d3", + "rev": "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "a7dbf0c63b694e47f425f3dcddbc0e178bb432d3", + "inputRev": "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/batteries.git", "type": "git", "subDir": null, "scope": "", - "rev": "023ce7d62a0531e22a5331e20b587817a80d49ff", + "rev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "023ce7d62a0531e22a5331e20b587817a80d49ff", + "inputRev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d", "inherited": false, "configFile": "lakefile.toml"}], "name": "LeanCopilot", diff --git a/lakefile.lean b/lakefile.lean index 0615862..685c3df 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -278,10 +278,25 @@ def ct2Pin : String := "v4.8.1" target libopenblas pkg : FilePath := do afterReleaseAsync pkg do - let rootDir := pkg.buildDir / "OpenBLAS" - ensureDirExists rootDir let dst := pkg.sharedLibDir / (nameToSharedLib (if getOS! == .windows then "libopenblas" else "openblas")) createParentDirs dst + + -- Distros that already package OpenBLAS (e.g. Nix) can point `-KsystemOpenblas=` at their own build instead of us cloning and compiling one + -- from source (see lean-dojo/LeanCopilot#187). + if let some path := get_config? systemOpenblas then + let depTrace := Hash.ofString s!"systemOpenblas:{path}" + setTrace depTrace + buildFileUnlessUpToDate' dst do + logInfo s!"Using system OpenBLAS from {path}" + copySingleFile (FilePath.mk path) dst + -- TODO: Don't hardcode the version "0". + copySingleFile dst (pkg.sharedLibDir / (nameToVersionedSharedLib "openblas" "0")) + let _ := (← getTrace) + return dst + + let rootDir := pkg.buildDir / "OpenBLAS" + ensureDirExists rootDir let url := "https://github.com/OpenMathLib/OpenBLAS" let depTrace := Hash.ofString (url ++ openblasPin) @@ -356,6 +371,28 @@ def getCt2CmakeFlags : IO (Array String) := do /- Download and build CTranslate2. Copy its C++ header files to `build/include` and shared libraries to `build/lib` -/ target libctranslate2 pkg : FilePath := do + -- Distros that already package CTranslate2 (e.g. Nix) can point `-KsystemCtranslate2Lib=` and `-KsystemCtranslate2Include=` at their own build instead of us + -- cloning and compiling one (and its OpenBLAS dependency) from source (see lean-dojo/LeanCopilot#187). + if let (some libPath, some includePath) := (get_config? systemCtranslate2Lib, get_config? systemCtranslate2Include) then + return ← afterReleaseAsync pkg do + let dst := pkg.sharedLibDir / (nameToSharedLib (if getOS! == .windows then "libctranslate2" else "ctranslate2")) + createParentDirs dst + let depTrace := Hash.ofString s!"systemCtranslate2:{libPath}:{includePath}" + setTrace depTrace + buildFileUnlessUpToDate' dst do + logInfo s!"Using system CTranslate2 from {libPath} (headers: {includePath})" + copySingleFile (FilePath.mk libPath) dst + -- TODO: Don't hardcode the version "4". + copySingleFile dst (pkg.sharedLibDir / (nameToVersionedSharedLib "ctranslate2" "4")) + ensureDirExists $ pkg.buildDir / "include" + copyFolder (FilePath.mk includePath / "ctranslate2") (pkg.buildDir / "include" / "ctranslate2") + copyFolder (FilePath.mk includePath / "nlohmann") (pkg.buildDir / "include" / "nlohmann") + copyFolder (FilePath.mk includePath / "half_float") (pkg.buildDir / "include" / "half_float") + let _ := (← getTrace) + return dst + if getOS! == .linux ∨ getOS! == .windows then let openblas ← libopenblas.fetch let _ ← openblas.await @@ -543,8 +580,8 @@ extern_lib libleanffi pkg := do buildStaticLib (pkg.sharedLibDir / name) #[ct2O, stubO] -require batteries from git "https://github.com/leanprover-community/batteries.git" @ "023ce7d62a0531e22a5331e20b587817a80d49ff" -require aesop from git "https://github.com/leanprover-community/aesop" @ "a7dbf0c63b694e47f425f3dcddbc0e178bb432d3" +require batteries from git "https://github.com/leanprover-community/batteries.git" @ "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d" +require aesop from git "https://github.com/leanprover-community/aesop" @ "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e" meta if get_config? env = some "dev" then -- dev is so not everyone has to build it require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main" diff --git a/lean-toolchain b/lean-toolchain index 2544c30..6a884ba 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.32.0 \ No newline at end of file +leanprover/lean4:v4.33.0 \ No newline at end of file