From 2c5ce794ddd648142d3a939994f9f634dee6a61d Mon Sep 17 00:00:00 2001
From: Mario Rugiero <mrugiero@gmail.com>
Date: Wed, 10 Jun 2026 15:22:03 -0300
Subject: [PATCH] test: cover allowedAxioms via lakefile leanOptions in
 consumer

Allow-list Consumer.benign and Consumer.alsoBenign project-wide via
leanOptions in the consumer lakefile; assert they stay silent while
evil is still flagged. Verified load-bearing: without the option all
six warnings fire, and lean rejects the -D name when the plugin is
not loaded.
---
 test/consumer/Consumer.lean      |  8 ++++++--
 test/consumer/Consumer/Defs.lean |  1 +
 test/consumer/lakefile.lean      |  5 +++++
 test/run.sh                      | 19 +++++++++++++++++--
 4 files changed, 29 insertions(+), 4 deletions(-)

diff --git a/test/consumer/Consumer.lean b/test/consumer/Consumer.lean
index 694cab0..73c197b 100644
--- a/test/consumer/Consumer.lean
+++ b/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
diff --git a/test/consumer/Consumer/Defs.lean b/test/consumer/Consumer/Defs.lean
index 621c1dc..82d2459 100644
--- a/test/consumer/Consumer/Defs.lean
+++ b/test/consumer/Consumer/Defs.lean
@@ -4,5 +4,6 @@ namespace Consumer
 
 axiom evil : False
 axiom benign : True
+axiom alsoBenign : True
 
 end Consumer
diff --git a/test/consumer/lakefile.lean b/test/consumer/lakefile.lean
index e8309a6..78d4383 100644
--- a/test/consumer/lakefile.lean
+++ b/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"⟩]
diff --git a/test/run.sh b/test/run.sh
index ec04f88..70c3d73 100755
--- a/test/run.sh
+++ b/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