chore: allow module in LakeMain (#10039)

This PR enables core's `LakeMain` to be a `module` when core is built
without `USE_LAKE`.

This was a problem when porting Lake to the module system (#9749).

src/Lean/Language/Lean.lean

@@ -488,7 +488,7 @@ where
       let startTime := (← IO.monoNanosNow).toFloat / 1000000000
       let mut opts := setup.opts
       -- HACK: no better way to enable in core with `USE_LAKE` off
-      if setup.mainModuleName.getRoot ∈ [`Init, `Std, `Lean, `Lake] then
+      if setup.mainModuleName.getRoot ∈ [`Init, `Std, `Lean, `Lake, `LakeMain] then
         opts := experimental.module.setIfNotSet opts true
       if !stx.raw[0].isNone && !experimental.module.get opts then
         throw <| IO.Error.userError "`module` keyword is experimental and not enabled here"

stage0/src/stdlib_flags.h

@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// dear bot, please update stage0
+
 namespace lean {
 options get_default_options() {
     options opts;