|
1 | 1 | # lean-project |
2 | 2 |
|
| 3 | +```bash |
| 4 | +$ lake build |
| 5 | +Build completed successfully (574 jobs). |
3 | 6 | ``` |
4 | | -$ lake build Project/Example.lean |
5 | | -Build completed successfully. |
6 | | -``` |
7 | | -If you need further information, see https://lean-lang.org/. |
8 | 7 |
|
9 | | -## Customize Copilot Instructions |
| 8 | +## How to use |
| 9 | + |
| 10 | +1. Create a repository from this template. |
| 11 | +2. Confirm lint settings in `package.json`, `.lefthook/`, and `lefthook.yml`. |
| 12 | +3. Remove `Project.lean` and `Project/`. |
| 13 | +4. Make your project files, then update `lakefile.toml`. |
| 14 | +5. Bump lean version in `.devcontainer/Dockerfile`, `lakefile.toml`, and `lean-toolchain`. |
| 15 | +6. Reomve `lake-manifest.json` and `.lake/`. |
| 16 | +7. Execute `lake exe cache get`. |
| 17 | + |
| 18 | +## Recommend to use |
| 19 | + |
| 20 | +### VSCode Extensions |
| 21 | + |
| 22 | +- [ms-vscode-remote.remote-containers](https://marketplace.visualstudio.com/items?itemName=ms-vscode-remote.remote-containers) |
| 23 | +- [github.copilot](https://marketplace.visualstudio.com/items?itemName=GitHub.copilot) |
| 24 | +- [github.copilot-chat](https://marketplace.visualstudio.com/items?itemName=GitHub.copilot-chat) |
10 | 25 |
|
11 | | -Make sure your vscode settings `github.copilot.chat.codeGeneration.useInstructionFiles` is `true`, and add `.github/copilot-instructions.md`. If you need further information, see below: |
12 | | -- https://code.visualstudio.com/docs/copilot/copilot-customization |
13 | | -- https://code.visualstudio.com/docs/copilot/reference/copilot-settings |
| 26 | +### MCP Servers |
14 | 27 |
|
15 | | -If you want to customize chatmode, for example, see https://burkeholland.github.io/posts/beast-mode-3-1/. |
| 28 | +- https://github.com/oOo0oOo/lean-lsp-mcp |
0 commit comments