Create index and unseen declarations list in CI

Signed-off-by: zeramorphic <[email protected]>

.github/workflows/push_main.yml

@@ -30,6 +30,11 @@ jobs:
       - name: build project
         run: ~/.elan/bin/lake -Kenv=dev build ConNF
 
+      - name: build index
+        run: |
+          printf "\n#deptree\n#index\n#unseen\n" >> DependencyGraph.lean
+          ~/.elan/bin/lake -Kenv=dev build DependencyGraph
+
       # - name: build lean4checker
       #   run: |
       #     git clone https://github.com/leanprover/lean4checker

.gitignore

@@ -2,5 +2,3 @@
 /lake-packages/*
 /.lake/*
 **.olean
-depgraph.*
-unseen_defs.txt

ConNF/Counting/StrongSupport.lean

@@ -710,52 +710,6 @@ theorem smul_comp_ext {γ : Λ} [LeLevel γ]
       · rintro ⟨c, hc⟩
         exact h ⟨ρ⁻¹ • c, h₃ i hT' hS' c hc⟩
 
-/- theorem canComp_comp {γ δ : Λ} {S : Support β}
-    {A : Path (β : TypeIndex) γ} {B : Path (γ : TypeIndex) δ}
-    (h : S.CanComp (A.comp B)) : S.CanComp A := by
-  obtain ⟨i, hi, c, hc⟩ := h
-  rw [Path.comp_assoc] at hc
-  exact ⟨i, hi, ⟨B.comp c.1, c.2⟩, hc⟩
-
-theorem canComp_comp' {γ δ : Λ} {S : Support β}
-    {A : Path (β : TypeIndex) γ} {B : Path (γ : TypeIndex) δ} :
-    (S.comp A).CanComp B ↔ S.CanComp (A.comp B) := by
-  constructor
-  · rintro ⟨i, hi, c, hc⟩
-    obtain ⟨j, hj, hjc⟩ := comp_f_eq' hc
-    rw [← Path.comp_assoc] at hjc
-    exact ⟨j, hj, c, hjc⟩
-  · rintro ⟨i, hi, c, hc⟩
-    refine ⟨i, ?_, c, ?_⟩
-    · rw [comp_max_eq_of_canComp (canComp_comp ⟨i, hi, c, hc⟩)]
-      exact hi
-    · rw [Path.comp_assoc] at hc
-      rw [comp_f_eq, comp_decomp_eq _ _ (c := ⟨B.comp c.1, c.2⟩) hc]
-
-theorem comp_comp [LeLevel β] {γ δ : Λ} [LeLevel γ] [LeLevel δ] (S : Support β)
-    (A : Path (β : TypeIndex) γ) (B : Path (γ : TypeIndex) δ) :
-    S.comp (A.comp B) = (S.comp A).comp B := by
-  refine Enumeration.ext' ?_ ?_
-  · by_cases h : S.CanComp (A.comp B)
-    · rw [comp_max_eq_of_canComp h,
-        comp_max_eq_of_canComp (canComp_comp'.mpr h),
-        comp_max_eq_of_canComp (canComp_comp h)]
-    · rw [comp_max_eq_of_not_canComp h, comp_max_eq_of_not_canComp]
-      rw [canComp_comp']
-      exact h
-  · intro i hE hF
-    have hcomp : S.CanComp (A.comp B) := canComp_of_lt_comp_max hE
-    have hS' := lt_max_of_lt_comp_max hF
-    have hS := lt_max_of_lt_comp_max (lt_max_of_lt_comp_max hF)
-    by_cases h : ∃ c : Address δ, S.f i hS = ⟨(A.comp B).comp c.1, c.2⟩
-    · obtain ⟨c, hc⟩ := h
-      rw [comp_f_eq, comp_decomp_eq hcomp hS hc]
-      rw [comp_f_eq, comp_decomp_eq]
-      rw [comp_f_eq, comp_decomp_eq]
-      rw [hc, Path.comp_assoc]
-    · rw [comp_f_eq, comp_decomp_eq' hcomp hS h]
-      sorry -/
-
 end Support
 
 end ConNF

DependencyGraph.lean

@@ -35,7 +35,7 @@ def groups (imports : NameMap (Array Name)) : NameMap Unit :=
 elab "#deptree " : command => do
   let env ← getEnv
   let imports := env.importGraph
-  IO.FS.withFile "depgraph.dot" IO.FS.Mode.write fun h => do
+  IO.FS.withFile "docs/depgraph.dot" IO.FS.Mode.write fun h => do
   h.write "digraph {\n".toUTF8
   h.write "compound=true;\n".toUTF8
   for (gp, _) in groups imports do
@@ -54,8 +54,6 @@ elab "#deptree " : command => do
       printDeps₂ k v (fun s => h.write s.toUTF8)
   h.write "}\n".toUTF8
 
-#deptree
-
 /-- Extracts the names of the declarations in `env` on which `decl` depends. -/
 -- source:
 -- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Counting.20prerequisites.20of.20a.20theorem/near/425370265
@@ -68,7 +66,8 @@ partial def allDeclsIn (module : Name) : Elab.Command.CommandElabM (Array Name)
   unless (← mFile.pathExists) do
     logError m!"object file '{mFile}' of module {module} does not exist"
   let (md, _) ← readModuleData mFile
-  let decls ← md.constNames.filterM fun d => return !(← d.isBlackListed)
+  let decls ← md.constNames.filterM fun d =>
+    return !(← d.isBlackListed) && !(`injEq).isSuffixOf d && !(`sizeOf_spec).isSuffixOf d
   return decls
 
 def allFiles (env : Environment) : List Name :=
@@ -79,11 +78,28 @@ def allDecls (env : Environment) : Elab.Command.CommandElabM NameSet :=
   (fun l => RBTree.ofList (l.map (fun a => a.toList)).join) <$>
     (mapM allDeclsIn (allFiles env))
 
+/-- `#index` computes an index of the declations in the project and saves it to `index.csv`. -/
+elab "#index " : command => do
+  let env ← getEnv
+  let allDecls ← allDecls env
+  let result ← mapM (fun decl => do
+    let ranges ← findDeclarationRanges? decl
+    let mod ← findModuleOf? decl
+    match (ranges, mod) with
+    | (some ranges, some mod) => pure (some (decl, ranges, mod))
+    | _ => pure none)
+    (allDecls.toList.mergeSort (toString · < toString ·))
+  let result' := result.filterMap id
+  IO.FS.withFile "docs/index.csv" IO.FS.Mode.write (fun h => do
+    for (decl, ranges, mod) in result' do
+      h.write (decl.toString ++ ", " ++ mod.toString ++ ", " ++
+        ranges.range.pos.line.repr ++ ", " ++ ranges.range.pos.column.repr ++ "\n").toUTF8)
+
 def seenIn (env : Environment) (allDecls : NameSet) (decl : Name) : NameSet :=
   (getVisited env decl).fold
     (fun decls x => if allDecls.contains x then decls.insert x else decls) RBTree.empty
 
-/-- `#unseen` computes a list of the declarations of the current file that are
+/-- `#unseen` computes a list of the declarations in the project that are
 defined but not used in the current file. The list is stored in `unseen_defs.txt`.
 The average runtime on my computer is 1 minute, with 16 threads. -/
 elab "#unseen " : command => do
@@ -96,12 +112,8 @@ elab "#unseen " : command => do
   for task in tasks do
     for v in task.get do
       unseen := unseen.erase v
-  IO.FS.withFile "unseen_defs.txt" IO.FS.Mode.write (fun h => do
+  IO.FS.withFile "docs/unseen_defs.txt" IO.FS.Mode.write (fun h => do
     for v in unseen.toList.mergeSort (toString · < toString ·) do
       h.write (v.toString ++ "\n").toUTF8)
   let timeEnd ← IO.monoMsNow
   logInfo m!"operation took {(timeEnd - timeStart) / 1000}s"
-
-/-! Uncommenting the following line will run the `#unseen` program, which will take ~1 minute on a
-reasonably powerful system with about 16 threads. -/
--- #unseen

docs/.gitignore

@@ -4,3 +4,6 @@ _site
 .jekyll-metadata
 vendor
 docs/
+depgraph.*
+unseen_defs.txt
+index.csv

lakefile.lean

@@ -17,3 +17,5 @@ require «doc-gen4» from git
 
 @[default_target]
 lean_lib ConNF
+
+lean_lib DependencyGraph