From 83396ed5478126f0d92698854e5eed6006b813d6 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 9 Jul 2024 15:25:06 -0400 Subject: [PATCH 1/6] feat: change docs --- .github/workflows/docs.yml | 17 +++---- scripts/find_TODOs.lean | 100 +++++++++++++++++++++++++++++++++++++ 2 files changed, 107 insertions(+), 10 deletions(-) create mode 100644 scripts/find_TODOs.lean diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index 2d58d3e..dcd0b99 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -2,6 +2,7 @@ on: push: branches: - master + - Update-versions name: Build and deploy documentation @@ -21,30 +22,26 @@ 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 - name: Get cache - run: ~/.elan/bin/lake -Kenv=dev exe cache get || true + 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 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 +52,7 @@ jobs: MathlibDoc- - name: Build documentation - run: ~/.elan/bin/lake -Kenv=dev build HepLean:docs + run: lake -Kenv=dev build HepLean:docs - name: Copy documentation to `docs/docs` run: | diff --git a/scripts/find_TODOs.lean b/scripts/find_TODOs.lean new file mode 100644 index 0000000..9faf776 --- /dev/null +++ b/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 From 678a35899dc7b49ed65174171c86d1b3f641e9d5 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 9 Jul 2024 15:26:48 -0400 Subject: [PATCH 2/6] Update docs.yml --- .github/workflows/docs.yml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index dcd0b99..a7f8b7e 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -25,8 +25,12 @@ jobs: ################## # 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: lake -Kenv=dev exe cache get || true From 594020f0e8b8dcb314f79b6f4b1e4dc51a8261a5 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 9 Jul 2024 15:45:15 -0400 Subject: [PATCH 3/6] feat: Add todo list to docs --- .github/workflows/docs.yml | 11 +++++++---- lakefile.toml | 4 ++++ 2 files changed, 11 insertions(+), 4 deletions(-) diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index a7f8b7e..44bcfe2 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -30,14 +30,14 @@ jobs: 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 + + - name: Get Mathlib cache run: lake -Kenv=dev exe cache get || true - name: Build project run: lake -Kenv=dev build HepLean - - name: Cache mathlib docs + - name: Get doc cache uses: actions/cache@v3 with: path: | @@ -57,7 +57,10 @@ jobs: - name: Build documentation run: lake -Kenv=dev build HepLean:docs - + + - name: make TODO list + run : lake exe find_TODOs mkFile + - name: Copy documentation to `docs/docs` run: | mv .lake/build/doc docs/docs diff --git a/lakefile.toml b/lakefile.toml index 5029023..bf4acda 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -40,4 +40,8 @@ srcDir = "scripts" [[lean_exe]] name = "double_line_lint" +srcDir = "scripts" + +[[lean_exe]] +name = "find_TODOs" srcDir = "scripts" \ No newline at end of file From d1162cc827ac760e3189de635424fd52d66e2e0f Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 9 Jul 2024 16:04:52 -0400 Subject: [PATCH 4/6] Update docs.yml --- .github/workflows/docs.yml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index 44bcfe2..08b43fb 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -2,7 +2,6 @@ on: push: branches: - master - - Update-versions name: Build and deploy documentation @@ -60,7 +59,7 @@ jobs: - name: make TODO list run : lake exe find_TODOs mkFile - + - name: Copy documentation to `docs/docs` run: | mv .lake/build/doc docs/docs From 7f7459da7a18a2c46124be0167d56fca22a75111 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 9 Jul 2024 16:06:50 -0400 Subject: [PATCH 5/6] Update README.md --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index d6efa61..3c77a1b 100644 --- a/README.md +++ b/README.md @@ -3,8 +3,8 @@ [![](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. ## Aims of this project From 4c0291ae7b2d7ee374a4eefa4fd428ecc2fb4526 Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Tue, 9 Jul 2024 16:07:15 -0400 Subject: [PATCH 6/6] Update README.md --- README.md | 1 + 1 file changed, 1 insertion(+) diff --git a/README.md b/README.md index 3c77a1b..9225176 100644 --- a/README.md +++ b/README.md @@ -5,6 +5,7 @@ [![](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. ## Aims of this project