949 B
949 B
Scripts associated with HepLean
lint-style.py and lint-style.sh
Taken from Mathlib's linters. These perform text-based linting of the code.
These are to be slowly replaced with code written in Lean.
double_line_lint
Checks for double empty lines in HepLean. Passing this linter is currently not required to pass CI on github.
Run using
lake exe double_line_lint
check_file_imports.lean
Checks all files are correctly imported into HepLean.lean.
Run using
lake exe check_file_imports
type_former_lint.lean
Checks whether the name of definitions which form a type or prop starts with a capital letter.
Run using
lake exe type_former_lint
lint-all.sh
Performs all linting checks on HepLean.
Run using
./scripts/lint-all.sh
Other useful commands
- To build HepLean use
lake exe cache get
lake build
- To update HepLean's dependencies use
lake update