cannot import non-module when adding new files to Mathlib

Stream: new members

[Alexey Milovanov]

Hi everyone! My name is Alexey, I'm a mathematician mostly working on Kolmogorov complexity. I recently formalized some foundations of Kolmogorov complexity in a Lean repository (https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Foundations.20of.20Kolmogorov.20complexity).

I am now trying to make a PR to Mathlib with a small, foundational part of this project (Bijective Base-2 Numeration). However, I've run into a tricky build issue that I cannot resolve.

Whenever I add any new file to Mathlib, the root Mathlib build fails at the very last step. After extensive debugging, I managed to reproduce this on a completely fresh, clean clone in /tmp.
Environment: WSL2 (Ubuntu), Lean v4.29.0-rc2 (toolchain verified), Lake v5.0.0-src.
Minimal Reproducible Example (in a clean /tmp directory):

Bash

git clone https://github.com/leanprover-community/mathlib4.git clean-test
cd clean-test
lake exe cache get
lake build Mathlib # <-- SUCCESS (all jobs complete)

# Add a dummy file and update the index
echo "import Mathlib.Data.Nat.Basic" > Mathlib/Logic/Equiv/FooTest.lean
git add Mathlib/Logic/Equiv/FooTest.lean
lake exe mk_all

# Rebuild
lake build Mathlib # <-- FAILS

The Error:

Plaintext

error: Mathlib.lean:1:0: cannot import non-module Mathlib.Logic.Equiv.FooTest from module
error: Lean exited with code 1

It seems Lake compiles the new .olean locally without issues, but refuses to treat it as a valid module within the lean_lib target graph during the root build, even when the file is tracked by git.

Is this a known issue with the current RC on WSL, or am I missing a specific step required to register new modules in Mathlib4? Any help would be greatly appreciated!

---

[Vlad Tsyrklevich]

If you look at another file in Mathlib you will see that they all begin with the module keyword which is likely what you're missing