fix: pass Lean CMake CI options to the Lake build (#8823)

This PR passes Lean options configured via CMake variables onto the Lake
build. For example, this will ensure CI' setting of `warningAsError` via
`LEAN_EXTRA_MAKE_OPTS` reaches Lake.

src/lakefile.toml.in

@@ -25,6 +25,10 @@ leanLibDir = "lib/lean"
 # Destination for static libraries
 nativeLibDir = "lib/lean"
 
+# Additional options derived from the CMake configuration
+# For example, CI will set `-DwarningAsError=true` through this
+moreLeanArgs = [${LEAN_EXTRA_OPTS_TOML}]
+
 [[lean_lib]]
 name = "Init"
 libName = "${LAKE_LIB_PREFIX}Init"