Bump to latest

.github/workflows/push_pr.yml

@@ -12,12 +12,39 @@ on:
       - stable
 
 jobs:
-  build:
+  build-release:
     runs-on: ${{ matrix.os }}
     strategy:
       matrix:
-        os: [macos-latest, ubuntu-latest, windows-latest]
-    name: Build
+        os: [macos-latest, ubuntu-latest]
+    name: BuildRelease
+    steps:
+      - name: Checkout project
+        uses: actions/checkout@v4
+        with:
+          fetch-depth: 0
+      - name: Install Git LFS
+        run: |
+          git lfs update --force
+          git lfs install
+      - name: Set up elan
+        run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
+      - name: Add .lake/build/lib to PATH
+        shell: bash
+        run: |
+          echo "$GITHUB_WORKSPACE/.lake/build/lib" >> $GITHUB_PATH
+      - name: Build project
+        run: ~/.elan/bin/lake build
+      - name: Download model
+        run: |
+          ~/.elan/bin/lake exe LeanCopilot/download
+      - name: Build tests
+        run: ~/.elan/bin/lake build LeanCopilotTests
+
+  build-beta:
+    runs-on: windows-latest
+    name: BuildBeta
+    continue-on-error: true
     steps:
       - name: Checkout project
         uses: actions/checkout@v4

README.md

@@ -8,20 +8,20 @@ Lean Copilot allows large language models (LLMs) to be used natively in Lean for
 ## Table of Contents
 
 1. [Requirements](#requirements)  
-2. [Using Lean Copilot in Your Project](#using-lean-copilot-in-your-project)
+1. [Using Lean Copilot in Your Project](#using-lean-copilot-in-your-project)
    1. [Adding Lean Copilot as a Dependency](#adding-lean-copilot-as-a-dependency)
-   3. [Getting Started with Lean Copilot](#getting-started-with-lean-copilot)
+   1. [Getting Started with Lean Copilot](#getting-started-with-lean-copilot)
       1. [Tactic Suggestion](#tactic-suggestion)
-      2. [Proof Search](#proof-search)
-      3. [Premise Selection](#premise-selection)
-5. [Advanced Usage](#advanced-usage)
+      1. [Proof Search](#proof-search)
+      1. [Premise Selection](#premise-selection)
+1. [Advanced Usage](#advanced-usage)
    1. [Tactic APIs](#tactic-apis)
-   2. [Model APIs](#model-apis)
-   3. [Bring Your Own Model](#bring-your-own-model)
-8. [Caveats](#caveats)
-9. [Getting in Touch](#getting-in-touch)
-10. [Acknowledgements](#acknowledgements)
-11. [Citation](#citation)
+   1. [Model APIs](#model-apis)
+   1. [Bring Your Own Model](#bring-your-own-model)
+1. [Caveats](#caveats)
+1. [Getting in Touch](#getting-in-touch)
+1. [Acknowledgements](#acknowledgements)
+1. [Citation](#citation)
 
 ## Requirements
 
@@ -59,7 +59,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.18.0`), set `LEAN_COPILOT_VERSION` to be that version. For the latest unstable Lean versions, 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.19.0`), set `LEAN_COPILOT_VERSION` to be that version. For the latest unstable Lean versions, 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]]

lake-manifest.json

@@ -5,20 +5,20 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "2bcdf2985dbe37cff63ca18346d8b26b8a448d3d",
+   "rev": "5d50b08dedd7d69b3d9b3176e0d58a23af228884",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "2bcdf2985dbe37cff63ca18346d8b26b8a448d3d",
+   "inputRev": "5d50b08dedd7d69b3d9b3176e0d58a23af228884",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "613510345e4d4b3ce3d8c129595e7241990d5b39",
+   "rev": "f5d04a9c4973d401c8c92500711518f7c656f034",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "613510345e4d4b3ce3d8c129595e7241990d5b39",
+   "inputRev": "f5d04a9c4973d401c8c92500711518f7c656f034",
    "inherited": false,
    "configFile": "lakefile.toml"}],
  "name": "LeanCopilot",

lakefile.lean

@@ -388,8 +388,8 @@ extern_lib libleanffi pkg := do
   buildStaticLib (pkg.nativeLibDir / name) #[ct2O]
 
 
-require batteries from git "https://github.com/leanprover-community/batteries.git" @ "613510345e4d4b3ce3d8c129595e7241990d5b39"
-require aesop from git "https://github.com/leanprover-community/aesop" @ "2bcdf2985dbe37cff63ca18346d8b26b8a448d3d"
+require batteries from git "https://github.com/leanprover-community/batteries.git" @ "f5d04a9c4973d401c8c92500711518f7c656f034"
+require aesop from git "https://github.com/leanprover-community/aesop" @ "5d50b08dedd7d69b3d9b3176e0d58a23af228884"
 
 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.18.0
+leanprover/lean4:v4.19.0