diff --git a/scripts/README.md b/scripts/README.md new file mode 100644 index 0000000..2b6e300 --- /dev/null +++ b/scripts/README.md @@ -0,0 +1,58 @@ + +# 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 +``` \ No newline at end of file diff --git a/scripts/build.sh b/scripts/build.sh deleted file mode 100755 index 9312991..0000000 --- a/scripts/build.sh +++ /dev/null @@ -1,6 +0,0 @@ -#!/usr/bin/env bash - - - -lake exe cache get -lake build \ No newline at end of file diff --git a/scripts/update-lean-mathlib.sh b/scripts/update-lean-mathlib.sh deleted file mode 100755 index 43fdc71..0000000 --- a/scripts/update-lean-mathlib.sh +++ /dev/null @@ -1,4 +0,0 @@ -#!/usr/bin/env bash - -lake update -