From 6eceeed59aef6dd58a5749aa2e164333b43c1580 Mon Sep 17 00:00:00 2001
From: Alexandre Rademaker <arademaker@gmail.com>
Date: Sun, 18 Oct 2026 21:01:17 -0300
Subject: [PATCH] chore(build): silence Lake's module-system warning with
 allowNonModules

Mathlib sets requiresModuleSystem, so Lake warns on every Mathlib
import from a file without a `module` header. The chapters stay out
of the module system on purpose; declare that in CSwL's lakefile and
in the lakefile of the generated per-variant projects. Adopting the
module system is tracked in #38.

This change was prepared with the assistance of Claude Code (Anthropic);
all edits were reviewed by the author.
---
 CSwLMeta/Save/Project.lean |  7 ++++++-
 lakefile.toml              | 11 +++++++++++
 2 files changed, 17 insertions(+), 1 deletion(-)

diff --git a/CSwLMeta/Save/Project.lean b/CSwLMeta/Save/Project.lean
index a4347d6..1f22ed5 100644
--- a/CSwLMeta/Save/Project.lean
+++ b/CSwLMeta/Save/Project.lean
@@ -101,7 +101,11 @@ revision the book is compiled with -- read from `CSwL`'s own
 besides `vol` -- today, at most, `"CSwLCompat"` when some extracted chapter
 imports the support module (see `bundleCompatSeed`). It does not go into
 `defaultTargets`: as in `sf-in-lean`, it is pulled in transitively by the
-`import` of the chapter that uses it. -/
+`import` of the chapter that uses it.
+
+`allowNonModules` silences the warning Lake emits for every `import
+Mathlib...` in a file without a `module` header; see the comment on the same
+option in `CSwL`'s own `lakefile.toml`. -/
 private def lakefileTemplate (vol : String) (v : Variant)
     (pkgRequires : Array (String × String × String))
     (extraLibs : Array String) : String :=
@@ -116,6 +120,7 @@ private def lakefileTemplate (vol : String) (v : Variant)
   "name = \"" ++ vol.toLower ++ "-extracted\"\n" ++
   "version = \"0.1.0\"\n" ++
   "defaultTargets = [\"" ++ vol ++ "\"]\n" ++
+  "allowNonModules = true\n" ++
   reqs ++
   "\n[[lean_lib]]\n" ++
   "name = \"" ++ vol ++ "\"\n" ++
diff --git a/lakefile.toml b/lakefile.toml
index cfbdd9e..924ccc3 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -14,6 +14,17 @@ defaultTargets = ["cswl", "CSwLCompat"]
 # explicitly).
 leanOptions = {doc.verso = true}
 
+# Mathlib (and so `cslib`) sets `requiresModuleSystem`: Lake then warns, for
+# every `import Mathlib...` in a file without a `module` header, "consider
+# adding `module` to the start of this file". The chapters deliberately stay
+# out of the module system -- its visibility rules (private by default,
+# `public`/`@[expose]`, definitions that `rfl` cannot unfold across files)
+# would be one more thing to present before any Lean code. This option
+# declares that mixing on purpose and silences the warning, for every
+# library of the package. Whether to adopt the module system instead is
+# https://github.com/cslib-community/CSwL/issues/38.
+allowNonModules = true
+
 [[lean_lib]]
 name = "CSwL"
 # `doc.verso.suggestions` turns off the linter that, for every inline