chore(build): silence Lake's module-system warning with allowNonModules

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" ++

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