chore: disable #print axioms under the module system (#8174)

No need for extra tracking to enable it considering how easy it is to
opt out

src/Lean/AddDecl.lean

@@ -148,12 +148,6 @@ where
           let env ← (← getEnv).addDeclAux (← getOptions) decl (← read).cancelTk?
             |> ofExceptKernelException
           setEnv env
-          if env.header.isModule then
-            -- Under the module system, must record axioms in environment extension now when we
-            -- still have access to the declaration's body. We could skip this for non-opaque decls
-            -- but for them, registering simply acts as a cache.
-            for n in decl.getTopLevelNames do
-              registerAxiomsForDecl n
         catch ex =>
           -- avoid follow-up errors by (trying to) add broken decl as axiom
           addAsAxiom

src/Lean/Elab/Print.lean

@@ -198,6 +198,10 @@ private def printAxiomsOf (constName : Name) : CommandElabM Unit := do
 
 @[builtin_command_elab «printAxioms»] def elabPrintAxioms : CommandElab
   | `(#print%$tk axioms $id) => withRef tk do
+    if (← getEnv).header.isModule then
+      throwError "cannot use `#print axioms` in a `module`; consider temporarily removing the \
+        `module` header or placing the command in a separate file"
+
     let cs ← liftCoreM <| realizeGlobalConstWithInfos id
     cs.forM printAxiomsOf
   | _ => throwUnsupportedSyntax

src/Lean/Util/CollectAxioms.lean

@@ -4,12 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import Lean.CoreM
+import Lean.MonadEnv
+import Lean.Util.FoldConsts
 
 namespace Lean
 
-private builtin_initialize exportedAxiomsExt : MapDeclarationExtension (Array Name) ← mkMapDeclarationExtension
-
 namespace CollectAxioms
 
 structure State where
@@ -18,19 +17,12 @@ structure State where
 
 abbrev M := ReaderT Environment $ StateM State
 
-private partial def collect (c : Name) : M Unit := do
+partial def collect (c : Name) : M Unit := do
   let collectExpr (e : Expr) : M Unit := e.getUsedConstants.forM collect
   let s ← get
   unless s.visited.contains c do
     modify fun s => { s with visited := s.visited.insert c }
     let env ← read
-    if let some axioms := exportedAxiomsExt.find? env c then
-      for ax in axioms do
-        if ax == c then
-          modify fun s => { s with axioms := s.axioms.push c }
-        else
-          collect ax
-      return
     -- We should take the constant from the kernel env, which may differ from the one in the elab
     -- env in case of (async) errors.
     match env.checked.get.find? c with
@@ -51,12 +43,4 @@ def collectAxioms [Monad m] [MonadEnv m] (constName : Name) : m (Array Name) :=
   let (_, s) := ((CollectAxioms.collect constName).run env).run {}
   pure s.axioms
 
-/--
-Registers axioms used by the declaration in an environment extension so they can be retrieved even
-if some parts of the declaration's become inaccessible.
--/
-def registerAxiomsForDecl (n : Name) : CoreM Unit := do
-  let axioms ← collectAxioms n
-  modifyEnv (exportedAxiomsExt.addEntry · (n, axioms))
-
 end Lean