Bump to Lean v4.33.0; support prebuilt system libraries

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=<path to your libopenblas.so/.dylib>` skips cloning and building OpenBLAS (Linux/Windows only; macOS uses Apple's Accelerate framework instead of OpenBLAS).
+* `-KsystemCtranslate2Lib=<path to your libctranslate2.so/.dylib>` together with `-KsystemCtranslate2Include=<path to a directory containing the ctranslate2/, nlohmann/, and half_float/ header trees>` 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`.

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",

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=<path
+    -- to libopenblas.so/.dylib>` 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=<path
+  -- to libctranslate2.so/.dylib>` and `-KsystemCtranslate2Include=<path to a directory containing
+  -- the ctranslate2/, nlohmann/, and half_float/ header trees>` 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"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.32.0
+leanprover/lean4:v4.33.0