From 03a1d17a9ccbf42a3d8a0f41cc4879b726bdde09 Mon Sep 17 00:00:00 2001 From: Peiyang-Song Date: Wed, 6 Dec 2023 14:50:29 -0800 Subject: [PATCH 1/2] Add git lfs init --- .github/workflows/push.yml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/.github/workflows/push.yml b/.github/workflows/push.yml index fe051ca..6d2c901 100644 --- a/.github/workflows/push.yml +++ b/.github/workflows/push.yml @@ -17,6 +17,10 @@ jobs: uses: actions/checkout@v2 with: fetch-depth: 0 + - name: Install Git LFS + run: | + git lfs install + git lfs pull - name: Set up elan run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y - name: Build project From ccf22e3f8e703950458bddc3e0d075e4f9972692 Mon Sep 17 00:00:00 2001 From: Kaiyu Yang Date: Wed, 6 Dec 2023 19:58:26 -0800 Subject: [PATCH 2/2] Update README.md --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index d753d0e..0f6ee13 100644 --- a/README.md +++ b/README.md @@ -56,7 +56,7 @@ Coming soon.* ## Building LeanCopilot -You don't need to build LeanCopilot directly if you use it in a downstream package. Nevertheless, if you really need to build LeanCopilot, it can be done by `lake build`. However, make sure you have installed these dependencies: +You don't need to build Lean Copilot directly if you use it only in downstream packages. However, you may need to do that in some cases, e.g., if you want to contribute to Lean Copilot. You can run `lake build`, but make sure you have installed these dependencies: * CMake >= 3.7 * A C++17 compatible compiler, e.g., recent versions of GCC or Clang