Merge pull request #418 from HEPLean/style-lint-changes

chore: Style lint changes

.github/ISSUE_TEMPLATE/Bump.yml

@@ -2,6 +2,16 @@ name: Bump Issue
 description: Issue used to bump the version of a Lean.
 title: "Bump to version: "
 body:
+- type: textarea
+  id: bump_details
+  attributes:
+    label: Version bump
+    description: Please do not modify this text.
+    value: |
+      This issue is a tracker issue for bumping PhysLean to new versions of Lean.
+      The checklist below should be used to ensure that the bump is done correctly.
+  validations:
+    required: true
 - type: checkboxes
   id: basics
   attributes:
@@ -30,7 +40,7 @@ body:
     label: Scripts
     description: Please check off these items as you complete them
     options:
-      - label: Ensure `lake exe hepLean_style_lint` runs without errors.
+      - label: Ensure `lake exe style_lint` runs without errors.
       - label: Ensure `lake exe TODO_to_yml mkFile` runs without errors.
       - label: Ensure `lake exe stats mkHTML` runs without errors.
       - label: Ensure `lake exe informal mkFile mkDot mkHTML` runs without errors.

lakefile.toml

@@ -45,8 +45,8 @@ name = "type_former_lint"
 srcDir = "scripts"
 
 [[lean_exe]]
-name = "hepLean_style_lint"
-srcDir = "scripts"
+name = "style_lint"
+srcDir = "scripts/MetaPrograms"
 
 [[lean_exe]]
 name = "find_TODOs"

scripts/lint_all.lean

@@ -6,7 +6,7 @@ Authors: Joseph Tooby-Smith
 
 def main (_: List String) : IO UInt32 := do
   println! "Style lint ... "
-  let styleLint ← IO.Process.output {cmd := "lake", args := #["exe", "hepLean_style_lint"]}
+  let styleLint ← IO.Process.output {cmd := "lake", args := #["exe", "style_lint"]}
   println! styleLint.stdout
   println! "Building ... "
   let build ← IO.Process.output {cmd := "lake", args := #["build"]}