From aa6f22d10237fab0979bc721886f84166df05e2b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Tue, 15 Jul 2025 18:36:03 +0200
Subject: [PATCH] chore: reduce import closure of MPL (#9382)

This PR reduces the import closure of the monadic verification framework
from `Lean.Meta` to only
the submodules actually required.
---
 src/Lean/Elab/Tactic/Do/Attr.lean                 | 2 +-
 src/Lean/Elab/Tactic/Do/LetElim.lean              | 2 +-
 src/Lean/Elab/Tactic/Do/ProofMode/Basic.lean      | 2 +-
 src/Lean/Elab/Tactic/Do/ProofMode/Delab.lean      | 1 +
 src/Lean/Elab/Tactic/Do/ProofMode/Exact.lean      | 1 +
 src/Lean/Elab/Tactic/Do/ProofMode/Focus.lean      | 1 -
 src/Lean/Elab/Tactic/Do/ProofMode/MGoal.lean      | 4 +++-
 src/Lean/Elab/Tactic/Do/ProofMode/Specialize.lean | 1 +
 src/Lean/Elab/Tactic/Do/VCGen.lean                | 1 +
 9 files changed, 10 insertions(+), 5 deletions(-)

diff --git a/src/Lean/Elab/Tactic/Do/Attr.lean b/src/Lean/Elab/Tactic/Do/Attr.lean
index daeb71b199..f1dc83c119 100644
--- a/src/Lean/Elab/Tactic/Do/Attr.lean
+++ b/src/Lean/Elab/Tactic/Do/Attr.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Graf
 -/
 prelude
-import Lean.Meta
+import Lean.Meta.Tactic.Simp
 import Std.Do.Triple.Basic
 import Std.Tactic.Do.Syntax
 
diff --git a/src/Lean/Elab/Tactic/Do/LetElim.lean b/src/Lean/Elab/Tactic/Do/LetElim.lean
index 5774cc289e..05c25e8c61 100644
--- a/src/Lean/Elab/Tactic/Do/LetElim.lean
+++ b/src/Lean/Elab/Tactic/Do/LetElim.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Graf
 -/
 prelude
-import Lean.Meta
+import Lean.Meta.Tactic.Simp
 
 namespace Lean.Elab.Tactic.Do
 
diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/Basic.lean b/src/Lean/Elab/Tactic/Do/ProofMode/Basic.lean
index 6db7085a59..13e7ec420f 100644
--- a/src/Lean/Elab/Tactic/Do/ProofMode/Basic.lean
+++ b/src/Lean/Elab/Tactic/Do/ProofMode/Basic.lean
@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Lars König, Mario Carneiro, Sebastian Graf
 -/
 prelude
-import Lean.Meta
 import Std.Tactic.Do.Syntax
+import Lean.Meta.Basic
 import Lean.Elab.Tactic.Do.ProofMode.MGoal
 
 namespace Lean.Elab.Tactic.Do.ProofMode
diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/Delab.lean b/src/Lean/Elab/Tactic/Do/ProofMode/Delab.lean
index b1f0b3b821..afcd110892 100644
--- a/src/Lean/Elab/Tactic/Do/ProofMode/Delab.lean
+++ b/src/Lean/Elab/Tactic/Do/ProofMode/Delab.lean
@@ -5,6 +5,7 @@ Authors: Lars König, Mario Carneiro, Sebastian Graf
 -/
 prelude
 import Lean.Elab.Tactic.Do.ProofMode.MGoal
+import Lean.PrettyPrinter.Delaborator.Basic
 
 namespace Lean.Elab.Tactic.Do.ProofMode
 open Std.Do
diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/Exact.lean b/src/Lean/Elab/Tactic/Do/ProofMode/Exact.lean
index 01dd1650d5..1ef51b4d85 100644
--- a/src/Lean/Elab/Tactic/Do/ProofMode/Exact.lean
+++ b/src/Lean/Elab/Tactic/Do/ProofMode/Exact.lean
@@ -7,6 +7,7 @@ prelude
 import Std.Tactic.Do.Syntax
 import Lean.Elab.Tactic.Do.ProofMode.Basic
 import Lean.Elab.Tactic.Do.ProofMode.Focus
+import Lean.Elab.Tactic.ElabTerm
 
 namespace Lean.Elab.Tactic.Do.ProofMode
 open Std.Do SPred.Tactic
diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/Focus.lean b/src/Lean/Elab/Tactic/Do/ProofMode/Focus.lean
index 0534e1cfd0..975d67d6ed 100644
--- a/src/Lean/Elab/Tactic/Do/ProofMode/Focus.lean
+++ b/src/Lean/Elab/Tactic/Do/ProofMode/Focus.lean
@@ -5,7 +5,6 @@ Authors: Lars König, Mario Carneiro, Sebastian Graf
 -/
 prelude
 import Lean.Elab.Tactic.Do.ProofMode.MGoal
-import Lean.Meta
 
 namespace Lean.Elab.Tactic.Do.ProofMode
 open Std.Do SPred.Tactic ProofMode
diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/MGoal.lean b/src/Lean/Elab/Tactic/Do/ProofMode/MGoal.lean
index 8207f2a122..41c4363833 100644
--- a/src/Lean/Elab/Tactic/Do/ProofMode/MGoal.lean
+++ b/src/Lean/Elab/Tactic/Do/ProofMode/MGoal.lean
@@ -6,7 +6,9 @@ Authors: Lars König, Mario Carneiro, Sebastian Graf
 prelude
 import Std.Do.SPred.DerivedLaws
 import Std.Tactic.Do.ProofMode
-import Lean.Meta
+import Lean.SubExpr
+import Lean.Meta.Basic
+import Lean.Elab.Tactic.Basic
 
 namespace Lean.Elab.Tactic.Do.ProofMode
 
diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/Specialize.lean b/src/Lean/Elab/Tactic/Do/ProofMode/Specialize.lean
index 735031e8bf..253cc1b39e 100644
--- a/src/Lean/Elab/Tactic/Do/ProofMode/Specialize.lean
+++ b/src/Lean/Elab/Tactic/Do/ProofMode/Specialize.lean
@@ -9,6 +9,7 @@ import Lean.Elab.Tactic.Do.ProofMode.MGoal
 import Lean.Elab.Tactic.Do.ProofMode.Focus
 import Lean.Elab.Tactic.Do.ProofMode.Basic
 import Lean.Elab.Tactic.Do.ProofMode.Pure
+import Lean.Elab.Tactic.ElabTerm
 
 namespace Lean.Elab.Tactic.Do.ProofMode
 open Std.Do SPred.Tactic
diff --git a/src/Lean/Elab/Tactic/Do/VCGen.lean b/src/Lean/Elab/Tactic/Do/VCGen.lean
index 1eb9f7a5e7..c02705271d 100644
--- a/src/Lean/Elab/Tactic/Do/VCGen.lean
+++ b/src/Lean/Elab/Tactic/Do/VCGen.lean
@@ -7,6 +7,7 @@ prelude
 import Init.Guard
 import Std.Do.WP
 import Std.Do.Triple
+import Lean.Meta.Tactic.Split
 import Lean.Elab.Tactic.Simp
 import Lean.Elab.Tactic.Meta
 import Lean.Elab.Tactic.Do.ProofMode.Basic