From e19bc86b156dbef4f0b4d636cfb3fd8790e2c607 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Tue, 9 Jul 2024 11:39:02 -0400
Subject: [PATCH] docs: Add documentation for scripts

---
 scripts/README.md              | 58 ++++++++++++++++++++++++++++++++++
 scripts/build.sh               |  6 ----
 scripts/update-lean-mathlib.sh |  4 ---
 3 files changed, 58 insertions(+), 10 deletions(-)
 create mode 100644 scripts/README.md
 delete mode 100755 scripts/build.sh
 delete mode 100755 scripts/update-lean-mathlib.sh

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 
-