Imposing the Module System on an Existing Project

Stream: new members

[Kevin Sullivan]

Notes from the rather painful experience of superimposing the new module system on an existing project, in a way that left everything else unchanged.

# Lean 4.27 Module System: Failure Modes and Best Practices

Lessons learned from migrating the Designer (~1064 modules) and CDK (~457 modules) codebases to the Lean 4.27 module system.

## The Module Header

Every `.lean` file must begin with the `module` keyword, followed by imports, followed by `@[expose] public section`:

```lean
module
public import Designer.Language.Types.Tipe
public import Lean.Data.Json

@[expose] public section

namespace CDK.Compiler.Bridges

Rules:
* module must be the first non-comment token in the file
* All imports use public import (not bare import)
* @[expose] public section opens the block where all definitions live
* Re-export aggregator modules have no definitions — just imports and the empty section

-- Re-export aggregator: combines ToJson + FromJson under a single import
module
public import CDK.Realms.SAM.ToJson
public import CDK.Realms.SAM.FromJson

@[expose] public section

---

Failure Mode 1: Private Declarations

Symptom

unknown identifier 'readFileIfExists'

A function that was accessible before migration is now invisible to callers in the same or other modules.

Cause

Inside @[expose] public section, private means truly private — not just file-private as in pre-4.27 Lean. The declaration is invisible to all other public declarations, even within the same section.

Fix

Remove private from all def, theorem, lemma, instance, abbrev, structure, and inductive declarations inside @[expose] public section. If a function was previously private for namespace hygiene, use more specific naming instead.

Watch for the @[inline] private def variant — a bulk sed targeting ^private def will miss it.

Scale

This affected ~240 declarations across 84 files in CDK alone. Automate with:

# Catches most cases
sed -E -i '' 's/^([[:space:]]*)private (def|theorem|lemma|instance|abbrev|structure|inductive)/\1\2/g' file.lean

# Also catch attribute-prefixed cases like @[inline] private def
sed -E -i '' 's/^([[:space:]]*@\[[^\]]*\]) private (def|theorem|lemma|instance)/\1 \2/g' file.lean

---

Failure Mode 2: Same-Package Native IR Missing

Symptom

Could not find native implementation of external declaration
  'lp_CDK_Compiler_Bridges_PythonV2_Data_PyVal_print._closed1'

The prefix matches your own package (here lp_CDK_).

Cause

When module A defines a function with @[expose] and module B (same package) calls that function at compile time (in #eval, #guard, or @[reducible] contexts), B needs the native compiled code. In 4.27, public import provides the type signatures but not necessarily the native IR.

Fix

Add import all for the module that defines the missing function, alongside the existing public import:

module
public import CDK.Compiler.Bridges.PythonV2.Data.PyVal
import all CDK.Compiler.Bridges.PythonV2.Data.PyVal   -- provides native IR

@[expose] public section

import all forces Lean to link the full native implementation of every @[expose] declaration from that module.

When You Need It

• Any file that calls @[expose] functions at compile time (#eval, #guard)
• Any file that uses @[expose] functions in positions requiring reduction (instance synthesis, simp, decide)
• Test files almost always need it

---

Failure Mode 3: Cross-Package Native IR Missing

Symptom

Could not find native implementation of external declaration
  'lp_Designer_Utils_Json_mkObjOmitNull._closed1'

The prefix is a different package (here lp_Designer_ from a CDK file).

Cause

import all only works within a single package. If CDK code calls a Designer @[expose] function at compile time, there is no way to link the native IR — the Designer shared library isn't available to CDK's compilation.

Fix Options

Option A (recommended): Move compile-time code to the defining package. If the #eval or #guard only tests Designer types, put those tests in the Designer test suite, not CDK.
Option B: Remove inline tests from core files. #eval and #guard in non-test files are the usual trigger. They produce no definitions — they're purely compile-time assertions. Move them to same-package test files where import all can provide the necessary native IR, or to the upstream package's test suite.
Option C: precompileModules = true in lakefile.toml. This compiles the upstream package to a shared library (.so/.dylib), making its native IR available cross-package. However, this changes build semantics and can slow incremental builds significantly.

What Does NOT Work

• import all Designer.Some.Module from CDK — this has no effect cross-package
• Adding more public import statements — these provide types, not native code

---

Failure Mode 4: Name Shadowing After Private Removal

Symptom

application type mismatch
  ⟦Sub⟧
has type
  Sub : Type → Type
but is expected to have type
  ...

A definition that previously had a unique name (because private scoped it) now collides with a Lean builtin or Mathlib name.

Cause

Removing private from def Sub exposes it to the global namespace, where Lean's builtin Sub : Type → Type (subtraction typeclass) takes priority. The local definition becomes shadowed.

Fix

Rename the definition to something that won't collide:

-- Before (fails: clashes with builtin Sub)
def Sub := ⟪.interface stdName⟫
-- After
def seqSub := ⟪.interface stdName⟫

High-Risk Names

Watch for these Lean builtins that commonly shadow user definitions: Sub, Add, Mul, Neg, Inv, Div, Mod, And, Or, Not, True, False, Zero, One, List, Option, Prod, Sum, Fin, Nat, Int.

---

Failure Mode 5: Inline Tests Blocking Compilation

Symptom

A core (non-test) file fails to build because of a #eval or #guard deep in the file, even though all the actual definitions are fine.

Cause

#eval and #guard execute at compile time. If they transitively call any function whose native IR is unavailable (see Failure Modes 2 and 3), the entire file fails to build — taking all downstream dependents with it.

Fix

Keep #eval and #guard exclusively in test files (Test/ directory). Core files should contain only definitions, instances, and theorems.

This is good practice regardless of the module system: inline tests create fragile compilation dependencies and make it harder to isolate build failures.

Identifying Inline Tests

# Find all #eval and #guard in non-test files
grep -rn '#eval\|#guard' CDK/CDK/ --include='*.lean' | grep -v '/Test/' | grep -v '/Evolving/'

GiveG

Best Practices Summary

File Structure

module                                    -- always first
public import Some.Module                 -- all imports are public
import all Some.Module                    -- only when native IR needed

@[expose] public section                  -- opens the public block

namespace My.Namespace
-- definitions here, no private keyword
end My.Namespace

Decision Tree for import all

1. Does this file use #eval or #guard? → Likely needs import all
2. Does the target module live in the same package? → import all will work
3. Does the target module live in a different package? → import all won't help; move the test or use precompileModules

Migration Checklist

• Add module as first token in every .lean file
• Convert all import to public import
• Add @[expose] public section after imports
• Remove all private from declarations inside @[expose] public section
• Scan for name collisions with Lean builtins after private removal
• Move all #eval/#guard from core files to test files
• Add import all in test files that call @[expose] functions
• Verify no cross-package #eval/#guard remain in core files
• Run lake clean && lake build as final verification

Automation

The modularize.py script handles the bulk mechanical transformation (adding module, converting imports, wrapping in @[expose] public section). The failure modes above are what it cannot handle — they require semantic understanding of the code.