Merge branch 'main' of https://github.com/lean-dojo/LeanCopilot into …

…main

Sync with remote

.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

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