add detector from using Classical.choice

Author: awalterschulze

Katydid.lean

@@ -1,3 +1,4 @@
+import Katydid.Std.Linter.DetectClassical
 import Katydid.Std.BEq
 import Katydid.Std.Ordering
 import Katydid.Std.Decidable

Katydid/Regex/IndexedRegex.lean

@@ -1,3 +1,4 @@
+import Katydid.Std.Linter.DetectClassical
 import Katydid.Std.Decidable
 
 import Katydid.Regex.Language

Katydid/Regex/Language.lean

@@ -1,3 +1,4 @@
+import Katydid.Std.Linter.DetectClassical
 import Katydid.Std.Lists
 
 namespace Language

Katydid/Regex/SimpleRegex.lean

@@ -3,6 +3,7 @@ import Lean
 import Mathlib.Tactic.SplitIfs
 import Mathlib.Tactic.CongrM
 
+import Katydid.Std.Linter.DetectClassical
 import Katydid.Std.Decidable
 
 import Katydid.Regex.Language

Katydid/Regex/SmartRegex.lean

@@ -1,3 +1,4 @@
+import Katydid.Std.Linter.DetectClassical
 import Katydid.Std.NonEmptyList
 
 import Katydid.Regex.Language

Katydid/Std/BEq.lean

@@ -1,3 +1,5 @@
+import Katydid.Std.Linter.DetectClassical
+
 theorem beq_eq_or_neq {α: Type} [BEq α] (x y: α):
   BEq.beq x y \/ (Not (BEq.beq x y)) := by
   by_cases BEq.beq x y

Katydid/Std/Decidable.lean

@@ -1,3 +1,5 @@
+import Katydid.Std.Linter.DetectClassical
+
 namespace Decidable
 
 def or {α β: Prop} (a: Decidable α) (b: Decidable β): Decidable (α \/ β) :=

Katydid/Std/Linter/DetectClassical.lean

@@ -0,0 +1,67 @@
+-- Thank you to Damiano Testa
+-- https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/restricting.20axioms/near/501743343
+
+import Lean.Util.CollectAxioms
+import Mathlib.Tactic.DeclarationNames
+
+/-!
+#  The "detectClassical" linter
+
+The "detectClassical" linter emits a warning on declarations that depend on the `Classical.choice`
+axiom.
+-/
+
+open Lean Elab Command
+
+namespace Katydid.Std.Linter
+
+/--
+The "detectClassical" linter emits a warning on declarations that depend on the `Classical.choice`
+axiom.
+-/
+register_option linter.detectClassical : Bool := {
+  defValue := true
+  descr := "enable the detectClassical linter"
+}
+
+/--
+The `linter.verbose.detectClassical` option is a flag to make the `detectClassical` linter emit
+a confirmation on declarations that depend *not* on the `Classical.choice` axiom.
+-/
+register_option linter.verbose.detectClassical : Bool := {
+  defValue := false
+  descr := "enable the verbose setting for the detectClassical linter"
+}
+
+namespace DetectClassical
+
+@[inherit_doc Katydid.Std.Linter.linter.detectClassical]
+def detectClassicalLinter : Linter where run := withSetOptionIn fun stx ↦ do
+  unless Linter.getLinterValue linter.detectClassical (← getOptions) do
+    return
+  if (← get).messages.hasErrors then
+    return
+  let d := (stx.getPos?.getD default)
+  let nmsd := (← Mathlib.Linter.getNamesFrom d)
+  let nms := nmsd.filter (! ·.getId.isInternal)
+  let verbose? := Linter.getLinterValue linter.verbose.detectClassical (← getOptions)
+  for constStx in nms do
+    let constName := constStx.getId
+    let axioms ← collectAxioms constName
+    if axioms.isEmpty then
+      if verbose? then
+        logInfoAt constStx m!"'{constName}' does not depend on any axioms"
+      return
+    if !axioms.contains `Classical.choice then
+      if verbose? then
+        logInfoAt constStx
+          m!"'{constName}' is non-classical and depends on axioms: {axioms.toList}"
+    else
+      Linter.logLint linter.detectClassical constStx
+        m!"'{constName}' depends on 'Classical.choice' on axioms: {axioms.toList}"
+
+initialize addLinter detectClassicalLinter
+
+end DetectClassical
+
+end Katydid.Std.Linter

Katydid/Std/Lists.lean

@@ -6,6 +6,7 @@
 import Mathlib.Tactic.Linarith
 import Mathlib.Tactic.SplitIfs
 
+import Katydid.Std.Linter.DetectClassical
 import Katydid.Std.BEq
 import Katydid.Std.Ordering
 import Katydid.Std.Nat

Katydid/Std/NonEmptyList.lean

@@ -1,3 +1,4 @@
+import Katydid.Std.Linter.DetectClassical
 import Katydid.Std.Ordering
 import Katydid.Std.Lists
 

lakefile.lean

@@ -3,8 +3,17 @@ open Lake DSL
 
 package katydid
 
+abbrev packageLinters : Array LeanOption := #[
+  ⟨`weak.linter.detectClassical, true⟩
+]
+
+abbrev packageLeanOptions :=
+  packageLinters
+
 @[default_target]
-lean_lib Katydid
+lean_lib Katydid where
+  leanOptions := packageLeanOptions
+  moreServerOptions := packageLinters
 
 -- dependencies std4, quote4 are obtained transitively through mathlib4
 require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.14.0"