Merge pull request #66 from HEPLean/Update-versions

chore: Update check file import

.github/workflows/build.yml

@@ -24,12 +24,7 @@ jobs:
         run: |
           lean --version
           lake --version
-      
-      - name: check ls 
-        run: |
-          ls -a
-          
-      
+
       - name: build cache
         run: |
           lake exe cache get
@@ -41,8 +36,12 @@ jobs:
           linters: gcc
           run: |
             bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build -KCI | tee stdout.log"
-      
-      - name: lint HepLean
+
+      - name: check file imports 
+        run: | 
+          bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake exe check_file_imports"
+
+      - name: runLinter on HepLean
         if: ${{ always() && steps.build.outcome == 'success' || steps.build.outcome == 'failure' }}
         id: lint
         uses: liskin/gh-problem-matcher-wrap@v3
@@ -51,7 +50,7 @@ jobs:
           run: env LEAN_ABORT_ON_PANIC=1 lake exe runLinter HepLean
 
   style_lint: 
-    name: Lint style
+    name: Python based style linter
     runs-on: ubuntu-latest
     steps:
       - name: cleanup

.github/workflows/check_file_import.yml

@@ -1,23 +0,0 @@
-on: 
-  push: 
-  pull_request: 
-
-name: check file import
-
-jobs: 
-  check_file_import: 
-    name: check file import 
-    runs-on: ubuntu-latest
-    steps: 
-      - name: clean up
-        run: |
-         find . -name . -o -prune -exec rm -rf -- {} +
-
-      - uses: actions/checkout@v4
-  
-      - name: update HepLean.lean 
-        run: |
-          git ls-files 'HepLean/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > HepLean.lean
-
-      - name: check that all files are imported
-        run: git diff --exit-code

HepLean/BeyondTheStandardModel/TwoHDM/Basic.lean

@@ -33,6 +33,5 @@ def potential (Φ1 Φ2 : higgsField)
   + (lam₆ * Φ1.normSq x * (Φ1.innerProd Φ2) x + conj lam₆ * Φ1.normSq x * (Φ2.innerProd Φ1) x).re
   + (lam₇ * Φ2.normSq x * (Φ1.innerProd Φ2) x + conj lam₇ * Φ2.normSq x * (Φ2.innerProd Φ1) x).re
 
-
 end
 end TwoHDM

doc/index.markdown

@@ -58,5 +58,5 @@ Any area not appearing in the below table has zero coverage in HepLean.
 | [Feynman diagrams](https://heplean.github.io/HepLean/docs/HepLean/FeynmanDiagrams/Basic.html) | ✔️ | ✘  | ✘  |  |
 | [Lorentz Group](https://heplean.github.io/HepLean/docs/HepLean/SpaceTime/LorentzGroup/Basic.html) | ✔️ | ✘  | ✘  | New lemmas etc.|
 | [2HDM](https://heplean.github.io/HepLean/docs/HepLean/SpaceTime/LorentzGroup/Basic.html) | ✔️ | ✘  | ✘  | New lemmas etc. |
-
+| All other areas |  ✘ | ✘  | ✘  | New lemmas etc.|
 

lakefile.toml

@@ -1,5 +1,7 @@
 name = "hep_lean"
 defaultTargets = ["HepLean"]
+# -- Optional inclusion for LeanCopilot
+#moreLinkArgs = ["-L./.lake/packages/LeanCopilot/.lake/build/lib", "-lctranslate2"]
 
 [[require]]
 name = "mathlib"
@@ -12,3 +14,19 @@ rev = "main"
 
 [[lean_lib]]
 name = "HepLean"
+
+# -- Optional inclusion of tryAtEachStep
+#[[require]]
+#name = "tryAtEachStep" 
+#git = "https://github.com/dwrensha/tryAtEachStep"
+#rev = "main"
+
+# -- Optional inclusion of LeanCopilot
+#[[require]]
+#name = "LeanCopilot"
+#git = "https://github.com/lean-dojo/LeanCopilot.git"
+#rev = "v1.2.2"
+
+[[lean_exe]]
+name = "check_file_imports"
+srcDir = "scripts"

scripts/add-copilot.sh

@@ -1,18 +0,0 @@
-#!/usr/bin/env bash
-
-
-cp ./scripts/copilot_lakefile.txt lakefile.lean
-
-lake update LeanCopilot 
-
-lake exe LeanCopilot/download
-
-lake build 
-
-echo ".........................................................................."
-echo "Please do not push changes to the following files: 
-     - lakefile.lean
-     - .lake/lakefile.olean
-     - .lake/lakefile.olean.trace
-     - lake-manifest.json
-Please ensure that there are no 'import LeanCopilot' statements in the lean files."

scripts/check-file-import.py

@@ -1,63 +0,0 @@
-#!/usr/bin/env python3
-"""
-This file locally checks if all files in the HepLean directory are imported correctly in 
-the HepLean.lean file.
-"""
-import os
-import re
-
-directory = "./HepLean/"
-files = []
-for root, _, filenames in os.walk(directory):
-    for filename in filenames:
-        if filename.endswith(".lean"):
-            files.append(os.path.join(root, filename))
-
-
-with open("./HepLean.lean", 'r') as f:
-    content = f.read()
-    
-imports = []
-for line in content.split('\n'):
-    match = re.match(r'import\s+(.*)', line)
-    if match:
-        imports.append(match.group(1))
-
-files_as_imports = [] 
-for file in files:
-    file_name = file 
-    file_name = file.replace("./", "").replace("/", ".").replace(".lean", "")
-    files_as_imports.append(file_name)
-
-files_as_imports.sort()
-a = [0,3,2]
-
-def file_check(imports, files_as_imports):
-    fail = False 
-    if imports != sorted(imports):
-        print("The imports list is not sorted.")
-        fail = True
-    to_add = [] 
-    for file in files_as_imports:
-        if file not in imports:
-            fail = True
-            to_add.append(file)
-    to_delete = []
-    for file in imports:
-        if file not in files_as_imports:
-            fail = True
-            to_delete.append(file)
-    if len(to_add) != 0 : 
-        print("The following files are not imported: ")
-        for f in to_add:
-            print(f)
-    if len(to_delete) != 0 : 
-        print("The following files should be deleted from HepLean.lean: ")
-        for f in to_delete:
-            print(f)
-    if not fail:
-        print("All files are imported correctly.")
-
-print ("----- Local import check of files: ")
-file_check(imports, files_as_imports)
-print ("----- End of local import check of files ")

scripts/check_file_imports.lean

@@ -0,0 +1,94 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import Batteries.Lean.HashSet
+import Lean
+/-!
+
+# Check file imports
+
+This file checks that the imports in `HepLean.lean` are sorted and complete.
+
+It can be run from the terminal using
+`lake exe check_file_imports`.
+
+## Note on adaptation
+
+The functions
+
+`addModulesIn`, `expectedHepLeanImports`, and `checkMissingImports`
+
+are adapted from `batteries.scripts.check_imports.lean` authored by Joe Hendrix.
+
+
+-/
+open Lean System Meta
+
+
+/--  Recursively finds files in directory. -/
+partial def addModulesIn (recurse : Bool) (prev : Array Name) (root : Name := .anonymous)
+    (path : FilePath) : IO (Array Name) := do
+  let mut r := prev
+  for entry in ← path.readDir do
+    if ← entry.path.isDir then
+      if recurse then
+        r ← addModulesIn recurse r (root.mkStr entry.fileName) entry.path
+    else
+      let .some mod := FilePath.fileStem entry.fileName
+        | continue
+      r := r.push (root.mkStr mod)
+  pure r
+
+
+/-- Compute imports expected by `HepLean.lean` by looking at file structure. -/
+def expectedHepLeanImports : IO (Array Name) := do
+  let mut needed := #[]
+  for top in ← FilePath.readDir "HepLean" do
+      let nm := `HepLean
+      let rootname := FilePath.withExtension top.fileName ""
+      let root :=  nm.mkStr rootname.toString
+      if ← top.path.isDir then
+        needed ← addModulesIn (recurse := true) needed (root := root) top.path
+      else
+        needed :=
+        needed.push root
+  pure needed
+
+/-- Checks whether an array `imports` is sorted after `Init` is removed.  -/
+def arrayImportSorted (imports : Array Import) : IO Bool :=  do
+  let X := (imports.map (fun x => x.module.toString)).filter (fun x => x != "Init")
+  let mut warned := false
+  if ! X = X.qsort (· < ·) then
+    IO.print s!"Import file is not sorted. \n"
+    warned := true
+  pure warned
+
+/-- Checks every file in `reqImports` is imported into `modData`
+  return true if this is NOT the case. -/
+def checkMissingImports (modData : ModuleData) (reqImports : Array Name) :
+    IO Bool := do
+  let names : HashSet Name := HashSet.ofArray (modData.imports.map (·.module))
+  let mut warned := false
+  for req in reqImports do
+    if !names.contains req then
+      IO.print s!"File {req} is not imported. \n"
+      warned := true
+  pure warned
+
+def main (_ : List String) : IO UInt32 := do
+  initSearchPath (← findSysroot)
+  let mods : Name :=  `HepLean
+  let imp :  Import := {module := mods}
+  let mFile ← findOLean imp.module
+  unless (← mFile.pathExists) do
+        throw <| IO.userError s!"object file '{mFile}' of module {imp.module} does not exist"
+  let (hepLeanMod, _) ← readModuleData mFile
+  let eHepLeanImports ← expectedHepLeanImports
+  let sortedWarned ← arrayImportSorted hepLeanMod.imports
+  let warned ← checkMissingImports hepLeanMod eHepLeanImports
+  if (warned ∨ sortedWarned) then
+    throw <| IO.userError s!"The HepLean module is not sorted, or has missing imports."
+  IO.println s!"Import check complete."
+  pure 0

scripts/copilot_lakefile.txt

@@ -1,23 +0,0 @@
-import Lake
-open Lake DSL
-
-package «hep_lean» {
-  -- add any package configuration options here
-}
-
-require mathlib from git
-  "https://github.com/leanprover-community/mathlib4.git"
-
-@[default_target]
-lean_lib «HepLean» {
-  -- add any library configuration options here
-  moreLinkArgs := #[
-    "-L./.lake/packages/LeanCopilot/.lake/build/lib",
-    "-lctranslate2"
-  ]
-}
-
-meta if get_config? env = some "dev" then -- dev is so not everyone has to build it
-require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"
-
-require LeanCopilot from git "https://github.com/lean-dojo/LeanCopilot.git" @ "v1.2.1"