Keep tactic modules out of the executable's import closure

DESIGN.md

@@ -389,5 +389,6 @@ for the equivalence/simulation results above.
 ## Dependencies
 
 - Lean toolchain: `leanprover/lean4:v4.31.0` (see `lean-toolchain`).
-- [Batteries](https://github.com/leanprover-community/batteries), pinned to the matching tag
-  (only for the `lake lint` driver and the `nolint` attribute — no Mathlib).
+- [Batteries](https://github.com/leanprover-community/batteries), pinned to the matching tag —
+  only as the `lake lint` driver; no library module imports it (and none imports Mathlib or any
+  tactic-framework module, keeping the elaborator out of downstream executables).

YulSemantics/Basic.lean

@@ -1,16 +1,15 @@
-import Std.Tactic.BVDecide
-
 /-!
 # YulSemantics.Basic
 
-Confirms the toolchain is wired up and that the EVM word type `BitVec 256`
-(see `DESIGN.md` §4) is available with its bitvector automation.
+Defines the EVM word type `BitVec 256` (see `DESIGN.md` §4).
 
-This project does **not** depend on Mathlib. Every Lean module's `initialize_*` calls the
-initializer of each module it imports, so a bare `import Mathlib` anywhere in a downstream
-executable's import closure is a genuine symbol reference that keeps all ~8200 Mathlib object
-files alive at link time. `bv_decide` comes from `Std` (core); the only external dependency is
-Batteries, kept for the `lake lint` driver and the `nolint` attribute.
+This project does **not** depend on Mathlib — and, deliberately, no library module imports a
+*tactic* module (`Std.Tactic.*`, `Batteries.Tactic.*`) either. Every Lean module's `initialize_*`
+calls the initializer of each module it imports, so importing a tactic framework anywhere in an
+executable's import closure is a genuine symbol reference that links the whole elaborator
+(`libLean`) into the binary. Proof automation runs at proof-checking time; it does not need to be
+in the import graph. The only external dependency is Batteries, kept solely as the `lake lint`
+driver — nothing imports it.
 
 Module map:
 * `YulSemantics.Ast`     — AST + control-flow `Outcome`
@@ -25,7 +24,4 @@ namespace YulSemantics
 /-- The EVM-dialect value type: a 256-bit machine word (see `DESIGN.md` §4). -/
 abbrev Word := BitVec 256
 
-/-- Sanity check that `bv_decide`-style automation is available on `Word`. -/
-example (x : Word) : x + 0 = x := by bv_decide
-
 end YulSemantics

YulSemantics/Dialect.lean

@@ -1,5 +1,4 @@
 import YulSemantics.Ast
-import Batteries.Tactic.Lint  -- for the `nolint` attribute and the `unusedArguments` linter
 
 /-!
 # YulSemantics.Dialect
@@ -82,10 +81,15 @@ structure Effects where
   writes : Bool
   /-- The built-in may halt execution instead of returning. -/
   halts  : Bool
-  deriving Repr, DecidableEq, Inhabited
-
--- The `prec` argument of the auto-derived pretty-printer is genuinely unused for this plain record.
-attribute [nolint unusedArguments] instReprEffects.repr
+  deriving DecidableEq, Inhabited
+
+-- Handwritten (not derived): the derived instance's unused `prec` argument trips the
+-- `unusedArguments` linter, and `@[nolint]` would drag `Batteries.Tactic.Lint` — and with it the
+-- whole elaborator — into every downstream executable (see `YulSemantics.Basic`).
+instance : Repr Effects where
+  reprPrec e _ :=
+    f!"\{ deterministic := {repr e.deterministic}, reads := {repr e.reads}, " ++
+    f!"writes := {repr e.writes}, halts := {repr e.halts} }"
 
 namespace Effects
 

YulSemantics/Dialect/EVMExec.lean

@@ -98,10 +98,14 @@ structure LogEntry where
   topics : List U256
   /-- The logged memory slice. -/
   data   : List UInt8
-  deriving Repr, DecidableEq, Inhabited
-
--- The `prec` argument of the auto-derived pretty-printer is genuinely unused for this plain record.
-attribute [nolint unusedArguments] instReprLogEntry.repr
+  deriving DecidableEq, Inhabited
+
+-- Handwritten (not derived): the derived instance's unused `prec` argument trips the
+-- `unusedArguments` linter, and `@[nolint]` would drag `Batteries.Tactic.Lint` — and with it the
+-- whole elaborator — into every downstream executable (see `YulSemantics.Basic`).
+instance : Repr LogEntry where
+  reprPrec l _ :=
+    f!"\{ address := {repr l.address}, topics := {repr l.topics}, data := {repr l.data} }"
 
 /-- The (immutable) execution environment: transaction/block context, input data, and abstract
 read-only views of the world state. Addresses are represented as words. -/

lakefile.toml

@@ -11,8 +11,8 @@ lintDriver = "batteries/runLinter"
 [leanOptions]
 warningAsError = true
 
-# Batteries (not Mathlib!) is the only dependency, kept for the `runLinter` driver above and the
-# `nolint` attribute (`YulSemantics.Dialect` imports `Batteries.Tactic.Lint`).
+# Batteries (not Mathlib!) is the only dependency, kept solely for the `runLinter` driver above.
+# No library module imports it, so none of it is linked into downstream executables.
 [[require]]
 name = "batteries"
 scope = "leanprover-community"