feat: add Cslib.Init module and checkInitImports linter

.github/workflows/lean_action_ci.yml

@@ -17,3 +17,4 @@ jobs:
       - uses: leanprover/lean-action@v1
         with:
           build-args: "--wfail"
+          mk_all-check: "true"

Cslib.lean

@@ -27,6 +27,7 @@ import Cslib.Foundations.Semantics.ReductionSystem.Basic
 import Cslib.Foundations.Syntax.HasAlphaEquiv
 import Cslib.Foundations.Syntax.HasSubstitution
 import Cslib.Foundations.Syntax.HasWellFormed
+import Cslib.Init
 import Cslib.Languages.CCS.Basic
 import Cslib.Languages.CCS.BehaviouralTheory
 import Cslib.Languages.CCS.Semantics

Cslib/Computability/Languages/Language.lean

@@ -6,6 +6,7 @@ Authors: Ching-Tsun Chou
 
 import Mathlib.Computability.Language
 import Mathlib.Tactic
+import Cslib.Init
 
 /-!
 # Language (additional definitions and theorems)

Cslib/Computability/Languages/OmegaLanguage.lean

@@ -256,11 +256,11 @@ theorem le_omegaPow_congr [Inhabited α] {l1 l2 : Language α} (h : l1 ≤ l2) :
 theorem omegaPow_of_sub_one [Inhabited α] : (l - 1)^ω = l^ω := by
   ext s ; simp
 
-@[simp]
+@[simp, nolint simpNF]
 theorem zero_omegaPow [Inhabited α] : (0 : Language α)^ω = ⊥ := by
   ext s ; simp
 
-@[simp]
+@[simp, nolint simpNF]
 theorem one_omegaPow [Inhabited α] : (1 : Language α)^ω = ⊥ := by
   rw [← omegaPow_of_sub_one, tsub_self, zero_omegaPow]
 

Cslib/Foundations/Control/Monad/Free.lean

@@ -3,6 +3,7 @@ Copyright (c) 2025 Tanner Duve. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Tanner Duve, Eric Wieser
 -/
+import Cslib.Init
 import Mathlib.Tactic.Lemma
 import Mathlib.Tactic.SimpRw
 

Cslib/Foundations/Data/FinFun.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fabrizio Montesi, Xueying Qin
 -/
 
+-- TODO: Notation conflict with Mathlib.Finsupp (both use →₀)
+-- import Cslib.Init
 import Mathlib.Data.Finset.Basic
 
 /-! # Finite functions

Cslib/Foundations/Data/HasFresh.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fabrizio Montesi, Kenny Lau
 -/
 
+import Cslib.Init
 import Mathlib.Algebra.Field.Rat
 import Mathlib.Algebra.Ring.CharZero
 import Mathlib.Algebra.Ring.Int.Defs

Cslib/Foundations/Data/Nat/Segment.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Ching-Tsun Chou
 -/
 
+import Cslib.Init
 import Mathlib.Algebra.Order.Sub.Basic
 import Mathlib.Data.Nat.Nth
 import Mathlib.Tactic

Cslib/Foundations/Data/OmegaSequence/Defs.lean

@@ -3,6 +3,7 @@ Copyright (c) 2025 Ching-Tsun Chou. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Ching-Tsun Chou, Fabrizio Montesi
 -/
+import Cslib.Init
 import Mathlib.Data.Nat.Notation
 import Mathlib.Data.FunLike.Basic
 import Mathlib.Logic.Function.Iterate

Cslib/Foundations/Data/OmegaSequence/Flatten.lean

@@ -121,8 +121,8 @@ theorem append_flatten [Inhabited α] {ls : ωSequence (List α)} (h_ls : ∀ k,
   induction n generalizing ls <;> grind [tail_eq_drop, take_succ]
 
 /-- The length of `(ls.take n).flatten` is `ls.cumLen n`. -/
-@[simp, scoped grind =]
-theorem length_flatten_take [Inhabited α] {ls : ωSequence (List α)} (h_ls : ∀ k, (ls k).length > 0)
+@[simp, nolint simpNF, scoped grind =]
+theorem length_flatten_take {ls : ωSequence (List α)} (h_ls : ∀ k, (ls k).length > 0)
     (n : ℕ) : (ls.take n).flatten.length = ls.cumLen n := by
   induction n <;> grind [take_succ']
 
@@ -169,7 +169,7 @@ theorem toSegs_def (s : ωSequence α) (f : ℕ → ℕ) (n : ℕ) :
 
 /-- `(s.toSegs f).cumLen` is `f` itself. -/
 @[simp]
-theorem segment_toSegs_cumLen [Inhabited α] {f : ℕ → ℕ}
+theorem segment_toSegs_cumLen {f : ℕ → ℕ}
     (hm : StrictMono f) (h0 : f 0 = 0) (s : ωSequence α) :
     (s.toSegs f).cumLen = f := by
   ext n

Cslib/Foundations/Data/Relation.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fabrizio Montesi, Thomas Waring, Chris Henson
 -/
 
+import Cslib.Init
 import Mathlib.Logic.Relation
 
 /-! # Relations -/

Cslib/Foundations/Semantics/LTS/Basic.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fabrizio Montesi
 -/
 
+-- TODO: Causes type elaboration ambiguities in downstream files (Automata)
+-- import Cslib.Init
 import Mathlib.Tactic.Lemma
 import Mathlib.Data.Finite.Defs
 import Mathlib.Data.Fintype.Basic

Cslib/Foundations/Semantics/ReductionSystem/Basic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fabrizio Montesi, Thomas Waring
 -/
 
+import Cslib.Init
 import Mathlib.Logic.Relation
 import Mathlib.Util.Notation3
 

Cslib/Foundations/Syntax/HasAlphaEquiv.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fabrizio Montesi
 -/
 
+import Cslib.Init
+
 namespace Cslib
 
 /-- Typeclass for the α-equivalence notation `x =α y`. -/

Cslib/Foundations/Syntax/HasSubstitution.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fabrizio Montesi
 -/
 
+import Cslib.Init
+
 namespace Cslib
 
 /-- Typeclass for substitution relations and access to their notation. -/

Cslib/Foundations/Syntax/HasWellFormed.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fabrizio Montesi
 -/
 
+import Cslib.Init
+
 namespace Cslib
 
 /-- Typeclass for types equipped with a well-formedness predicate. -/

Cslib/Init.lean

@@ -0,0 +1,18 @@
+/-
+Copyright (c) 2025 Jesse Alama. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jesse Alama
+-/
+
+import Mathlib.Init
+import Cslib.Foundations.Lint.Basic
+
+/-!
+# CSLib Initialization
+
+This is the root file in CSLib: it is imported by virtually *all* CSLib files.
+For this reason, the imports of this file are carefully curated.
+
+Similar to Mathlib.Init, this file imports linters that should be active by default
+throughout the CSLib library.
+-/

Cslib/Languages/CCS/Basic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fabrizio Montesi
 -/
 
+import Cslib.Init
 import Mathlib.Init
 
 /-! # Calculus of Communicating Systems (CCS)

Cslib/Logics/LinearLogic/CLL/Basic.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fabrizio Montesi
 -/
 
+-- TODO: Syntax elaboration conflicts 
+-- import Cslib.Init
 import Aesop
 import Mathlib.Tactic.ApplyAt
 import Mathlib.Order.Notation

CslibTests.lean

@@ -3,7 +3,7 @@ import CslibTests.CCS
 import CslibTests.DFA
 import CslibTests.FreeMonad
 import CslibTests.HasFresh
+import CslibTests.LTS
 import CslibTests.LambdaCalculus
 import CslibTests.Lint
-import CslibTests.LTS
 import CslibTests.ReductionSystem

lakefile.toml

@@ -1,7 +1,7 @@
 name = "cslib"
 version = "0.1.0"
 defaultTargets = ["Cslib"]
-testDriver = "CslibTests"
+testDriver = "runTests"
 
 [leanOptions]
 weak.linter.mathlibStandardSet = true
@@ -25,3 +25,13 @@ globs = ["Cslib.*"]
 [[lean_lib]]
 name = "CslibTests"
 globs = ["CslibTests.+"]
+
+[[lean_exe]]
+name = "checkInitImports"
+srcDir = "scripts"
+root = "CheckInitImports"
+
+[[lean_exe]]
+name = "runTests"
+srcDir = "scripts"
+root = "RunTests"

scripts/CheckInitImports.lean

@@ -0,0 +1,58 @@
+/-
+Copyright (c) 2025 Jesse Alama. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jesse Alama, Chris Henson
+-/
+
+import Lean
+import Mathlib.Lean.CoreM
+import Batteries.Data.List.Basic
+import ImportGraph.Imports
+
+open Lean Core Elab Command
+
+/-!
+# Check Init Imports
+
+This script checks that all CSLib modules (transitively) import Cslib.Init.
+-/
+
+/-- Modules with technical constraints preventing Cslib.Init import -/
+def exceptions : List Name := [
+  -- Circular dependency (imported by Cslib.Init)
+  `Cslib.Foundations.Lint.Basic,
+  `Cslib.Init,
+
+  -- Type elaboration issues in downstream files
+  `Cslib.Foundations.Semantics.LTS.Basic,
+  `Cslib.Foundations.Semantics.LTS.TraceEq,
+  `Cslib.Computability.Automata.DA,
+  `Cslib.Computability.Automata.DFA,
+  `Cslib.Computability.Automata.DFAToNFA,
+  `Cslib.Computability.Automata.EpsilonNFA,
+  `Cslib.Computability.Automata.EpsilonNFAToNFA,
+  `Cslib.Computability.Automata.NA,
+  `Cslib.Computability.Automata.NFA,
+  `Cslib.Computability.Automata.NFAToDFA,
+
+  -- Notation conflict with Mathlib.Finsupp (→₀)
+  `Cslib.Foundations.Data.FinFun,
+
+  -- Syntax elaboration conflicts 
+  `Cslib.Logics.LinearLogic.CLL.Basic,
+  `Cslib.Logics.LinearLogic.CLL.CutElimination,
+  `Cslib.Logics.LinearLogic.CLL.MProof,
+  `Cslib.Logics.LinearLogic.CLL.PhaseSemantics.Basic,
+]
+
+def main : IO UInt32 := do
+  let searchPath ← addSearchPathFromEnv (← getBuiltinSearchPath (← findSysroot))
+  CoreM.withImportModules #[`Cslib] (searchPath := searchPath) (trustLevel := 1024) do
+    let env ← getEnv
+    let graph := env.importGraph.transitiveClosure
+    let noInitGraph := 
+      graph.filter (fun name imports => name.getRoot = `Cslib ∧ !imports.contains `Cslib.Init)
+    let diff := noInitGraph.keys.diff exceptions
+    if diff.length > 0 then
+      IO.eprintln s!"error: the following modules do not import `Cslib.Init`: {diff}"
+    return diff.length.toUInt32

scripts/RunTests.lean

@@ -0,0 +1,41 @@
+/-
+Copyright (c) 2025 Jesse Alama. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jesse Alama
+-/
+
+/-!
+# Test Runner
+
+This script runs all CSLib tests including:
+- Building the CslibTests library
+- Running init imports validation
+-/
+
+def main (_ : List String) : IO UInt32 := do
+  -- build CslibTests
+  IO.println "building CslibTests..."
+  let CslibTestsResult ← IO.Process.spawn {
+    cmd := "lake"
+    args := #["build", "CslibTests"]
+  } >>= (·.wait)
+
+  if CslibTestsResult != 0 then
+    IO.eprintln "\n✗ CslibTests build failed"
+    return CslibTestsResult
+  else
+    println! ""
+
+  -- Run init imports check
+  IO.println "\nChecking init imports..."
+  let checkResult ← IO.Process.spawn {
+    cmd := "lake"
+    args := #["exe", "checkInitImports"]
+  } >>= (·.wait)
+
+  if checkResult != 0 then
+    IO.eprintln "\n✗ Init imports check failed"
+    return checkResult
+
+  IO.println "\n✓ All tests passed"
+  return 0