feat: environment linters

Cslib.lean

@@ -16,6 +16,7 @@ import Cslib.Foundations.Data.OmegaSequence.Defs
 import Cslib.Foundations.Data.OmegaSequence.Flatten
 import Cslib.Foundations.Data.OmegaSequence.Init
 import Cslib.Foundations.Data.Relation
+import Cslib.Foundations.Lint.Basic
 import Cslib.Foundations.Semantics.LTS.Basic
 import Cslib.Foundations.Semantics.LTS.Bisimulation
 import Cslib.Foundations.Semantics.LTS.Simulation

Cslib/Foundations/Lint/Basic.lean

@@ -0,0 +1,38 @@
+/-
+Copyright (c) 2025 Chris Henson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Henson
+-/
+
+import Mathlib
+
+namespace Cslib.Lint
+
+open Lean Meta Std Batteries.Tactic.Lint
+
+/-- A linter for checking that new declarations fall under some preexisting namespace. -/
+@[env_linter]
+def topNamespace : Batteries.Tactic.Lint.Linter where
+  noErrorsFound := "No declarations are outside a namespace."
+  errorsFound := "TOP LEVEL DECLARATIONS:"
+  test declName := do
+    if ← isAutoDecl declName then return none
+    let env ← getEnv
+    if isGlobalInstance env declName then return none
+    let nss := env.getNamespaceSet
+    let top := nss.fold (init := (∅ : NameSet)) fun tot n =>
+      match n.components with
+      | r::_::_ => tot.insert r
+      | _ => tot    
+    if top.contains declName.components[0]! then
+      return none
+    else
+      let ty := env.find? declName |>.get! |>.type
+      /- TODO: this is a temporary allowance for unscoped notations generated
+         for `LTS` and `ReductionSystem`. -/
+      if ty == .const ``Lean.TrailingParserDescr [] then
+        return none
+      else
+        return m!"{declName} is not namespaced."
+
+end Cslib.Lint

CslibTests/Lint.lean

@@ -0,0 +1,35 @@
+/-
+Copyright (c) 2025 Chris Henson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Henson
+-/
+
+import Cslib
+
+set_option linter.hashCommand false
+
+namespace CslibTests
+
+/-! Failing linters. Some (but not all!) may be too strict for practical use. -/
+
+-- #lint- only simpNF in Cslib
+-- #lint- only explicitVarsOfIff in Cslib
+-- #lint- only impossibleInstance in Cslib
+-- #lint- only unusedArguments in Cslib
+-- #lint- only defLemma in Cslib
+-- #lint- only docBlame in Cslib
+-- #lint- only docBlameThm in Cslib
+-- #lint- only simpComm in Cslib
+-- #lint- only nonClassInstance in Cslib
+
+/-! Passing linters. -/
+
+#lint- only topNamespace in Cslib
+#lint- only synTaut in Cslib
+#lint- only checkType in Cslib
+#lint- only simpVarHead in Cslib
+#lint- only unusedHavesSuffices in Cslib
+#lint- only dupNamespace in Cslib
+#lint- only checkUnivs in Cslib
+
+end CslibTests