Skip to content

Commit

Permalink
Update README.md
Browse files Browse the repository at this point in the history
minor
  • Loading branch information
Peiyang-Song authored Dec 7, 2023
1 parent c9e7334 commit 13235af
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,7 @@ Coming soon.*



## Building LeanCopilot
## Building Lean Copilot

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
Expand All @@ -77,7 +77,7 @@ You don't need to build Lean Copilot directly if you use it only in downstream p
## Acknowledgements

* [llmstep](https://github.com/wellecks/llmstep) is another tool providing tactic suggestions using LLMs. We use their frontend for displaying tactics but a different mechanism for running the model.
* We thank Scott Morrison for suggestions on simplifying LeanCopilot's installation and Mac Malone for helping implement it. Both Scott and Mac work for the [Lean FRO](https://lean-fro.org/).
* We thank Scott Morrison for suggestions on simplifying Lean Copilot's installation and Mac Malone for helping implement it. Both Scott and Mac work for the [Lean FRO](https://lean-fro.org/).
* We thank Jannis Limperg for integrating our LLM-generated tactics into aesop (https://github.com/leanprover-community/aesop/pull/70).


Expand Down

0 comments on commit 13235af

Please sign in to comment.