-
Notifications
You must be signed in to change notification settings - Fork 9
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #234 from HEPLean/NoDocs
feat: No docs script
- Loading branch information
Showing
15 changed files
with
349 additions
and
65 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,193 @@ | ||
| /- | ||
| 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 | ||
| import Mathlib.Lean.Expr.Basic | ||
| import Mathlib.Lean.CoreM | ||
| import ImportGraph.RequiredModules | ||
| import HepLean.Meta.Informal | ||
| /-! | ||
| ## Basic Lean meta programming commands | ||
| -/ | ||
|
|
||
| namespace HepLean | ||
| open Lean System Meta | ||
|
|
||
| /-! | ||
| ## Imports | ||
| -/ | ||
|
|
||
| /-- Gets all imports within HepLean. -/ | ||
| def allImports : IO (Array Import) := 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 imports := hepLeanMod.imports.filter (fun c => c.module ≠ `Init) | ||
| return imports | ||
|
|
||
| /-- Number of files within HepLean. -/ | ||
| def noImports : IO Nat := do | ||
| let imports ← allImports | ||
| pure imports.size | ||
|
|
||
| /-- Gets all constants from an import. -/ | ||
| def Imports.getConsts (imp : Import) : IO (Array ConstantInfo) := do | ||
| let mFile ← findOLean imp.module | ||
| let (modData, _) ← readModuleData mFile | ||
| pure modData.constants | ||
|
|
||
| /-- Gets all user defined constants from an import. -/ | ||
| def Imports.getUserConsts (imp : Import) : MetaM (Array ConstantInfo) := do | ||
| let env ← getEnv | ||
| let x := (← Imports.getConsts imp).filter (fun c => ¬ c.name.isInternal) | ||
| let x := x.filter (fun c => ¬ Lean.isCasesOnRecursor env c.name) | ||
| let x := x.filter (fun c => ¬ Lean.isRecOnRecursor env c.name) | ||
| let x := x.filter (fun c => ¬ Lean.isNoConfusion env c.name) | ||
| let x := x.filter (fun c => ¬ Lean.isBRecOnRecursor env c.name) | ||
| let x := x.filter (fun c => ¬ Lean.isAuxRecursorWithSuffix env c.name Lean.binductionOnSuffix) | ||
| let x := x.filter (fun c => ¬ Lean.isAuxRecursorWithSuffix env c.name Lean.belowSuffix) | ||
| let x := x.filter (fun c => ¬ Lean.isAuxRecursorWithSuffix env c.name Lean.ibelowSuffix) | ||
| /- Removing syntax category declarations. -/ | ||
| let x := x.filter (fun c => ¬ c.name.toString = "Informal.informalAssignment.quot" ) | ||
| let x := x.filter (fun c => ¬ c.name.toString = "TensorTree.indexExpr.quot" ) | ||
| let x := x.filter (fun c => ¬ c.name.toString = "TensorTree.tensorExpr.quot" ) | ||
| pure x | ||
|
|
||
| /-- Lines from import. -/ | ||
| def Imports.getLines (imp : Import) : IO (Array String) := do | ||
| let filePath := (mkFilePath (imp.module.toString.split (· == '.'))).addExtension "lean" | ||
| let lines ← IO.FS.lines filePath | ||
| return lines | ||
|
|
||
| /-! | ||
| ## Name | ||
| -/ | ||
|
|
||
|
|
||
| /-- Turns a name into a Lean file. -/ | ||
| def Name.toFile (c : Name) : MetaM String := do | ||
| return s!"./{c.toString.replace "." "/" ++ ".lean"}" | ||
|
|
||
| /-- Given a name, returns the line number. -/ | ||
| def Name.lineNumber (c : Name) : MetaM Nat := do | ||
| match ← findDeclarationRanges? c with | ||
| | some decl => pure decl.range.pos.line | ||
| | none => panic! s!"{c} is a declaration without position" | ||
|
|
||
| /-- Returns the location of a name. -/ | ||
| def Name.location (c : Name) : MetaM String := do | ||
| let env ← getEnv | ||
| let x := env.getModuleFor? c | ||
| match x with | ||
| | some decl => pure ((← Name.toFile decl) ++ ":" ++ toString (← Name.lineNumber c) ++ " " | ||
| ++ c.toString) | ||
| | none => panic! s!"{c} is a declaration without position" | ||
|
|
||
| /-- Determines if a name has a location. -/ | ||
| def Name.hasPos (c : Name) : MetaM Bool := do | ||
| match ← findDeclarationRanges? c with | ||
| | some _ => pure true | ||
| | none => pure false | ||
|
|
||
| /-- Determines if a name has a doc string. -/ | ||
| def Name.hasDocString (c : Name) : MetaM Bool := do | ||
| let env ← getEnv | ||
| let doc ← Lean.findDocString? env c | ||
| match doc with | ||
| | some _ => pure true | ||
| | none => pure false | ||
|
|
||
| /-- Number of definitions. -/ | ||
| def noDefs : MetaM Nat := do | ||
| let imports ← allImports | ||
| let x ← imports.mapM Imports.getUserConsts | ||
| let x := x.flatten | ||
| let x := x.filter (fun c => c.isDef) | ||
| let x ← x.filterM (fun c => (Name.hasPos c.name)) | ||
| pure x.toList.length | ||
|
|
||
| /-- Number of definitions. -/ | ||
| def noLemmas : MetaM Nat := do | ||
| let imports ← allImports | ||
| let x ← imports.mapM Imports.getUserConsts | ||
| let x := x.flatten | ||
| let x := x.filter (fun c => ¬ c.isDef) | ||
| let x ← x.filterM (fun c => (Name.hasPos c.name)) | ||
| pure x.toList.length | ||
|
|
||
| /-- Number of definitions without a doc-string. -/ | ||
| def noDefsNoDocString : MetaM Nat := do | ||
| let imports ← allImports | ||
| let x ← imports.mapM Imports.getUserConsts | ||
| let x := x.flatten | ||
| let x := x.filter (fun c => c.isDef) | ||
| let x ← x.filterM (fun c => (Name.hasPos c.name)) | ||
| let x ← x.filterM (fun c => do | ||
| return Bool.not (← (Name.hasDocString c.name))) | ||
| pure x.toList.length | ||
|
|
||
| /-- Number of definitions without a doc-string. -/ | ||
| def noLemmasNoDocString : MetaM Nat := do | ||
| let imports ← allImports | ||
| let x ← imports.mapM Imports.getUserConsts | ||
| let x := x.flatten | ||
| let x := x.filter (fun c => ¬ c.isDef) | ||
| let x ← x.filterM (fun c => (Name.hasPos c.name)) | ||
| let x ← x.filterM (fun c => do | ||
| return Bool.not (← (Name.hasDocString c.name))) | ||
| pure x.toList.length | ||
|
|
||
| /-- The number of lines in HepLean. -/ | ||
| def noLines : IO Nat := do | ||
| let imports ← HepLean.allImports | ||
| let x ← imports.mapM HepLean.Imports.getLines | ||
| let x := x.flatten | ||
| pure x.toList.length | ||
|
|
||
| /-- The number of informal lemmas in HepLean. -/ | ||
| def noInformalLemmas : MetaM Nat := do | ||
| let imports ← allImports | ||
| let x ← imports.mapM Imports.getUserConsts | ||
| let x := x.flatten | ||
| let x := x.filter (Informal.isInformal) | ||
| let x := x.filter (Informal.isInformalLemma) | ||
| pure x.toList.length | ||
|
|
||
| /-- The number of informal definitions in HepLean. -/ | ||
| def noInformalDefs : MetaM Nat := do | ||
| let imports ← allImports | ||
| let x ← imports.mapM Imports.getUserConsts | ||
| let x := x.flatten | ||
| let x := x.filter (Informal.isInformal) | ||
| let x := x.filter (Informal.isInformalDef) | ||
| pure x.toList.length | ||
|
|
||
| /-- The number of TODO items. -/ | ||
| def noTODOs : IO Nat := do | ||
| let imports ← HepLean.allImports | ||
| let x ← imports.mapM HepLean.Imports.getLines | ||
| let x := x.flatten | ||
| let x := x.filter fun l => l.startsWith "/-! TODO:" | ||
| pure x.size | ||
|
|
||
| /-- The number of files with a TODO item. -/ | ||
| def noFilesWithTODOs : IO Nat := do | ||
| let imports ← HepLean.allImports | ||
| let x ← imports.mapM HepLean.Imports.getLines | ||
| let x := x.filter (fun M => M.any fun l => l.startsWith "/-! TODO:") | ||
| pure x.size | ||
|
|
||
| end HepLean |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,44 @@ | ||
| /- | ||
| Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved. | ||
| Released under Apache 2.0 license. | ||
| Authors: Joseph Tooby-Smith | ||
| -/ | ||
| import HepLean.Meta.Basic | ||
| /-! | ||
| # Extracting commands with no doc strings. | ||
| -/ | ||
|
|
||
| open Lean System Meta HepLean | ||
|
|
||
| def Imports.NoDocStringDef (imp : Import) : MetaM UInt32 := do | ||
| let x := (← Imports.getUserConsts imp).filter (fun c => c.isDef) | ||
| let x ← x.filterM (fun c => do | ||
| return Bool.not (← (Name.hasDocString c.name))) | ||
| let y ← x.filterM (fun c => Name.hasPos c.name) | ||
| let loc ← y.mapM (fun c => (Name.location c.name)) | ||
| if loc.toList.length > 0 then | ||
| IO.println "\n" | ||
| IO.println s!"Module {imp.module} has the following definitions without doc strings:" | ||
| IO.println (String.intercalate "\n" loc.toList) | ||
| pure 0 | ||
|
|
||
| def Imports.NoDocStringLemma (imp : Import) : MetaM UInt32 := do | ||
| let x := (← Imports.getUserConsts imp).filter (fun c => ¬ c.isDef) | ||
| let x ← x.filterM (fun c => do | ||
| return Bool.not (← (Name.hasDocString c.name))) | ||
| let y ← x.filterM (fun c => Name.hasPos c.name) | ||
| let loc ← y.mapM (fun c => (Name.location c.name)) | ||
| if loc.toList.length > 0 then | ||
| IO.println "\n" | ||
| IO.println s!"Module {imp.module} has the following lemmas without doc strings:" | ||
| IO.println (String.intercalate "\n" loc.toList) | ||
| pure 0 | ||
|
|
||
| unsafe def main (args : List String) : IO UInt32 := do | ||
| let imports ← allImports | ||
| let _ ← CoreM.withImportModules #[`HepLean] (imports.mapM Imports.NoDocStringDef).run' | ||
| if "--lemmas" ∈ args then | ||
| let _ ← CoreM.withImportModules #[`HepLean] (imports.mapM Imports.NoDocStringLemma).run' | ||
| pure 0 |
Oops, something went wrong.