test: cover allowedAxioms via lakefile leanOptions in consumer

test/consumer/Consumer.lean

@@ -1,10 +1,14 @@
 -- NOTE: deliberately NO `import LeanExtensions.AxiomGuard`. The guard is loaded as a plugin via
--- the lakefile `plugins :=`. If the plugin path works, the linter fires on the declaration below
--- (which depends on a non-standard axiom) with no import at all.
+-- the lakefile `plugins :=`. If the plugin path works, the linter fires on `uses_evil` below
+-- (which depends on a non-allowed axiom) with no import at all. `uses_benign`/`uses_benign_also`
+-- depend on axioms allow-listed project-wide via `leanOptions` in the lakefile, so they must stay
+-- silent — exercising the lakefile configuration path of `linter.axiomGuard.allowedAxioms`.
 import Consumer.Defs
 
 namespace Consumer
 
 theorem uses_evil : (1 : Nat) = 2 := evil.elim
+theorem uses_benign : True := benign
+theorem uses_benign_also : True := alsoBenign
 
 end Consumer

test/consumer/Consumer/Defs.lean

@@ -4,5 +4,6 @@ namespace Consumer
 
 axiom evil : False
 axiom benign : True
+axiom alsoBenign : True
 
 end Consumer

test/consumer/lakefile.lean

@@ -19,3 +19,8 @@ target axiomGuardPlugin : Dynlib := do
 @[default_target]
 lean_lib Consumer where
   plugins := #[axiomGuardPlugin]
+  -- Project-wide allow-list for the guard, passed to `lean` as `-D` flags by `lake build`.
+  -- Names must be fully qualified; the value exercises both separators (comma and space).
+  -- This only works under `lake build` (which also passes `--plugin`, registering the option
+  -- before CLI option validation) — a bare `lake env lean` would reject the unknown `-D` name.
+  leanOptions := #[⟨`linter.axiomGuard.allowedAxioms, "Consumer.benign, Consumer.alsoBenign"⟩]

test/run.sh

@@ -55,11 +55,11 @@ note ""
 note "== plugin-consumer path (no import) =="
 # The `plugins :=` wiring is only applied by `lake build` (which passes `--plugin` to lean), NOT
 # by a bare `lake env lean`. So we assert against the build output: force a clean re-elaboration
-# of the consumer module and check the guard message appears even though Consumer.lean has no
+# of the consumer modules and check the guard message appears even though Consumer.lean has no
 # `import LeanExtensions.AxiomGuard`.
 consumer_out="$(
   cd test/consumer || exit 2
-  touch Consumer.lean
+  touch Consumer.lean Consumer/Defs.lean
   lake build 2>&1
 )"
 if printf '%s' "$consumer_out" | grep -q "$GUARD_RE"; then
@@ -68,6 +68,21 @@ else
   bad "consumer: guard did NOT fire via plugin path"
   printf '%s\n' "$consumer_out"
 fi
+# `Consumer.benign`/`Consumer.alsoBenign` are allow-listed via `leanOptions` in the consumer
+# lakefile, so no guard warning may mention them — neither at the `axiom` declaration sites in
+# Defs.lean nor at the use sites in Consumer.lean. `evil` must still be flagged.
+if printf '%s' "$consumer_out" | grep "$GUARD_RE" | grep -qi 'benign'; then
+  bad "consumer: lakefile-allowed axiom was flagged"
+  printf '%s\n' "$consumer_out" | grep "$GUARD_RE"
+else
+  ok "consumer: lakefile leanOptions allow-list silences benign axioms"
+fi
+if printf '%s' "$consumer_out" | grep "$GUARD_RE" | grep -q 'evil'; then
+  ok "consumer: evil still flagged despite allow-list"
+else
+  bad "consumer: evil was NOT flagged with allow-list active"
+  printf '%s\n' "$consumer_out"
+fi
 if ( cd test/consumer && lake build --wfail >/dev/null 2>&1 ); then
   bad "consumer under --wfail (expected failure, got success)"
 else