$ lake exe mk_all
No update necessary
$ lake build
Build completed successfully (538 jobs).
- Create a new repository from this template.
- Review the GitHub Actions workflows in
.github/workflows/.
- Review the lint settings in
pyproject.toml and lefthook.yml.
- Update the Lean version in
.devcontainer/Dockerfile, lakefile.toml, lean-toolchain, and pyproject.toml.
- Run Dev Containers: Rebuild Container. Alternatively, delete
lake-manifest.json and .lake/, then run
lake exe cache get.
- Remove
Project.lean and Project/, then add your own project files.