$ lake exe mk_all
No update necessary
$ lake build
ℹ [496/498] Replayed Project.Example
info: Project/Example.lean:29:0: import Mathlib.Data.Nat.Factorial.Basic
import Mathlib.Data.Nat.Prime.Defs
info: Project/Example.lean:29:0: `#`-commands, such as '#min_imports', are not allowed in 'Mathlib' [linter.hashCommand]
Build completed successfully (498 jobs).- Create a repository from this template.
- Confirm lint settings in
package.json,.lefthook/, andlefthook.yml. - Remove
Project.leanandProject/. - Make your project files, then update
lakefile.toml. - Bump lean version in
.devcontainer/Dockerfile,lakefile.toml, andlean-toolchain. - Reomve
lake-manifest.jsonand.lake/. - Execute
lake exe cache get.