Merge pull request #77 from HEPLean/Update-versions

chore: Add TODO list

.github/workflows/docs.yml

@@ -21,30 +21,30 @@ jobs:
         with:
           fetch-depth: 0
       
-      - name: Print files to upstream
-        run: |
-          grep -r --files-without-match 'import HepLean' HepLean | sort > 1.txt
-          grep -r --files-with-match 'sorry' HepLean | sort > 2.txt
-          mkdir -p docs/_includes
-          comm -23 1.txt 2.txt | sed -e 's/^\(.*\)$/- [`\1`](https:\/\/github.com\/teorth\/HepLean\/blob\/master\/\1)/' > docs/_includes/files_to_upstream.md
-          rm 1.txt 2.txt
       ##################
       # Remove this section if you don't want docs to be made
       - name: Install elan
-        run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:4.0.0
+        run: |
+          set -o pipefail
+          curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y
+          ~/.elan/bin/lean --version
+          echo "$HOME/.elan/bin" >> $GITHUB_PATH
 
-      - name: Get cache
-        run: ~/.elan/bin/lake -Kenv=dev exe cache get || true
+      - name: Get Mathlib cache
+        run: lake -Kenv=dev exe cache get || true
 
       - name: Build project
-        run: ~/.elan/bin/lake -Kenv=dev build HepLean
+        run: lake -Kenv=dev build HepLean
 
-      - name: Cache mathlib docs
+      - name: Get doc cache
         uses: actions/cache@v3
         with:
           path: |
             .lake/build/doc/Init
+            .lake/build/doc/DocGen4
+            .lake/build/doc/Aesop
             .lake/build/doc/Lake
+            .lake/build/doc/Batteries
             .lake/build/doc/Lean
             .lake/build/doc/Std
             .lake/build/doc/Mathlib
@@ -55,7 +55,10 @@ jobs:
             MathlibDoc-
       
       - name: Build documentation
-        run: ~/.elan/bin/lake -Kenv=dev build HepLean:docs
+        run: lake -Kenv=dev build HepLean:docs
+      
+      - name: make TODO list 
+        run : lake exe find_TODOs mkFile 
 
       - name: Copy documentation to `docs/docs`
         run: |

README.md

@@ -3,6 +3,7 @@
 [![](https://img.shields.io/badge/Read_The-Docs-green)](https://heplean.github.io/HepLean/)
 [![](https://img.shields.io/badge/PRs-Welcome-green)](https://github.com/HEPLean/HepLean/pulls)
 [![](https://img.shields.io/badge/Lean-Zulip-green)](https://leanprover.zulipchat.com)
+[![](https://img.shields.io/badge/TODO-List-green)](https://heplean.github.io/HepLean/TODOList)
 [![](https://img.shields.io/badge/Lean-v4.9.0-blue)](https://github.com/leanprover/lean4/releases/tag/v4.9.0)
 
 A project to digitalize high energy physics.

lakefile.toml

@@ -40,4 +40,8 @@ srcDir = "scripts"
 
 [[lean_exe]]
 name = "double_line_lint"
+srcDir = "scripts"
+
+[[lean_exe]]
+name = "find_TODOs"
 srcDir = "scripts"

scripts/find_TODOs.lean

@@ -0,0 +1,100 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license.
+Authors: Joseph Tooby-Smith
+-/
+import Lean
+import Batteries.Data.String.Matcher
+import Mathlib.Init.Data.Nat.Notation
+/-!
+
+# TODO finder
+
+This program finds all instances of `/<!> TODO: ...` (without the `<>`) in HepLean files.
+
+## Note
+
+Parts of this file are adapted from `Mathlib.Tactic.Linter.TextBased`,
+  authored by Michael Rothgang.
+
+
+-
+-/
+open Lean System Meta
+
+/-- Given a list of lines, outputs an error message and a line number. -/
+def HepLeanTODOItem : Type := Array String → Array (String × ℕ)
+
+/-- Checks if a . -/
+def TODOFinder : HepLeanTODOItem := fun lines ↦ Id.run do
+  let enumLines := (lines.toList.enumFrom 1)
+  let todos := enumLines.filterMap (fun (lno1, l1) ↦
+    if l1.startsWith "/-! TODO:"   then
+      some ((l1.replace "/-! TODO: " "").replace "-/" "", lno1)
+    else none)
+  todos.toArray
+
+structure TODOContext where
+  /-- The underlying `message`. -/
+  statement : String
+  /-- The line number -/
+  lineNumber : ℕ
+  /-- The file path -/
+  path : FilePath
+
+def printTODO (todos : Array TODOContext) : IO Unit := do
+  for e in todos do
+    IO.println (s!"{e.path}:{e.lineNumber}: {e.statement}")
+
+def filePathToGitPath (S : FilePath) (n : ℕ) : String :=
+  "https://github.com/HEPLean/HepLean/blob/master/"++
+  (S.toString.replace "." "/").replace "/lean" ".lean"
+  ++ "#L" ++ toString n
+
+def docTODO  (todos : Array TODOContext) : IO String := do
+  let mut out := ""
+  for e in todos do
+    out := out ++ (s!" - [{e.statement}]("++ filePathToGitPath e.path e.lineNumber ++ ")\n")
+  return out
+
+def hepLeanLintFile (path : FilePath) : IO String := do
+  let lines ← IO.FS.lines path
+  let allOutput := (Array.map (fun lint ↦
+    (Array.map (fun (e, n) ↦ TODOContext.mk e n path)) (lint lines)))
+    #[TODOFinder]
+  let errors := allOutput.flatten
+  printTODO errors
+  docTODO errors
+
+def todoFileHeader : String := s!"
+# TODO List
+
+This is an automatically generated list of TODOs appearing as `/-! TODO:...` in HepLean.
+
+Please feel free to contribute to the completion of these tasks.
+
+
+"
+
+def main (args : 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 mut out :  String :=  ""
+  for imp in hepLeanMod.imports do
+    if imp.module == `Init then continue
+    let filePath := (mkFilePath (imp.module.toString.split (· == '.'))).addExtension "lean"
+    let l ← hepLeanLintFile filePath
+    if l != "" then
+      out := out ++ "\n### " ++ imp.module.toString ++ "\n"
+      out := out ++ l
+  let fileOut : System.FilePath := {toString := "./docs/TODOList.md"}
+  /- Below here is concerned with writing out to the docs. -/
+  if "mkFile" ∈ args then
+    IO.println (s!"TODOList file made.")
+    IO.FS.writeFile fileOut (todoFileHeader ++ out)
+  return 0