docs: Add documentation for scripts

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
+```

scripts/build.sh

@@ -1,6 +0,0 @@
-#!/usr/bin/env bash
-
-
-
-lake exe cache get 
-lake build

scripts/update-lean-mathlib.sh

@@ -1,4 +0,0 @@
-#!/usr/bin/env bash
-
-lake update 
-