fix: set mainModuleName in the new frontend

src/Lean/Elab/Frontend.lean

@@ -80,12 +80,12 @@ let (env, messages) ← process input env opts fileName
 pure (env, messages.toList)
 
 @[export lean_run_frontend]
-def runFrontend (env : Environment) (input : String) (opts : Options) (fileName : String) : IO (Environment × List Message) := do
+def runFrontend (input : String) (opts : Options) (fileName : String) (mainModuleName : Name) : IO (Environment × List Message) := do
 let inputCtx := Parser.mkInputContext input fileName
-match Parser.parseHeader env inputCtx with
-| (header, parserState, messages) =>
-  let (env, messages) ← processHeader header messages inputCtx
-  let cmdState ← IO.processCommands inputCtx parserState (Command.mkState env messages opts)
-  pure (cmdState.env, cmdState.messages.toList)
+let (header, parserState, messages) ← Parser.parseHeader inputCtx
+let (env, messages) ← processHeader header messages inputCtx
+let env := env.setMainModule mainModuleName
+let cmdState ← IO.processCommands inputCtx parserState (Command.mkState env messages opts)
+pure (cmdState.env, cmdState.messages.toList)
 
 end Lean.Elab

src/Lean/Elab/Import.lean

@@ -26,12 +26,10 @@ catch e =>
   pure (env, messages.add { fileName := inputCtx.fileName, data := toString e, pos := pos })
 
 def parseImports (input : String) (fileName : Option String := none) : IO (List Import × Position × MessageLog) := do
-let env ← mkEmptyEnvironment
 let fileName := fileName.getD "<input>"
 let inputCtx := Parser.mkInputContext input fileName
-match Parser.parseHeader env inputCtx with
-| (header, parserState, messages) =>
-  pure (headerToImports header, inputCtx.fileMap.toPosition parserState.pos, messages)
+let (header, parserState, messages) ← Parser.parseHeader inputCtx
+pure (headerToImports header, inputCtx.fileMap.toPosition parserState.pos, messages)
 
 @[export lean_parse_imports]
 def parseImportsExport (input : String) (fileName : Option String) : IO (List Import × Position × List Message) := do

src/Lean/Parser/Module.lean

@@ -39,8 +39,9 @@ private def mkErrorMessage (c : ParserContext) (pos : String.Pos) (errorMsg : St
 let pos := c.fileMap.toPosition pos;
 { fileName := c.fileName, pos := pos, data := errorMsg }
 
-def parseHeader (env : Environment) (inputCtx : InputContext) : Syntax × ModuleParserState × MessageLog :=
-let ctx := mkParserContext env inputCtx;
+def parseHeader (inputCtx : InputContext) : IO (Syntax × ModuleParserState × MessageLog) := do
+dummyEnv ← mkEmptyEnvironment;
+let ctx := mkParserContext dummyEnv inputCtx;
 let ctx := Module.updateTokens ctx;
 let s   := mkParserState ctx.input;
 let s   := whitespace ctx s;
@@ -49,9 +50,9 @@ let stx := s.stxStack.back;
 match s.errorMsg with
 | some errorMsg =>
   let msg := mkErrorMessage ctx s.pos (toString errorMsg);
-  (stx, { pos := s.pos, recovering := true }, { : MessageLog }.add msg)
+  pure (stx, { pos := s.pos, recovering := true }, { : MessageLog }.add msg)
 | none =>
-  (stx, { pos := s.pos }, {})
+  pure (stx, { pos := s.pos }, {})
 
 private def mkEOI (pos : String.Pos) : Syntax :=
 let atom := mkAtom { pos := pos, trailing := "".toSubstring, leading := "".toSubstring } "";
@@ -117,7 +118,7 @@ private partial def testModuleParserAux (env : Environment) (inputCtx : InputCon
 def testModuleParser (env : Environment) (input : String) (fileName := "<input>") (displayStx := false) : IO Bool :=
 timeit (fileName ++ " parser") $ do
   let inputCtx           := mkInputContext input fileName;
-  let (stx, s, messages) := parseHeader env inputCtx;
+  (stx, s, messages) ← parseHeader inputCtx;
   when displayStx (IO.println stx);
   testModuleParserAux env inputCtx displayStx s messages
 
@@ -137,7 +138,7 @@ partial def parseModuleAux (env : Environment) (inputCtx : InputContext) : Modul
 def parseModule (env : Environment) (fname contents : String) : IO Syntax := do
 fname ← IO.realPath fname;
 let inputCtx := mkInputContext contents fname;
-let (header, state, messages) := parseHeader env inputCtx;
+(header, state, messages) ← parseHeader inputCtx;
 cmds ← parseModuleAux env inputCtx state messages #[];
 let stx := Syntax.node `Lean.Parser.Module.module #[header, mkListNode cmds];
 pure stx.updateLeading

src/Lean/Server/Snapshots.lean

@@ -59,8 +59,7 @@ end Snapshot
 
 def compileHeader (contents : String) (opts : Options := {}) : IO Snapshot := do
 let inputCtx := Parser.mkInputContext contents "<input>";
-emptyEnv ← mkEmptyEnvironment;
-let (headerStx, headerParserState, msgLog) := Parser.parseHeader emptyEnv inputCtx;
+(headerStx, headerParserState, msgLog) ← Parser.parseHeader inputCtx;
 (headerEnv, msgLog) ← Elab.processHeader headerStx msgLog inputCtx;
 pure { beginPos := 0,
        mpState := headerParserState,

src/shell/lean.cpp

@@ -345,9 +345,10 @@ bool test_module_parser(environment const & env, std::string const & input, std:
 }
 
 typedef list_ref<object_ref> messages;
-extern "C" object * lean_run_frontend(object * env, object * input, object * opts, object * filename, object * w);
-pair_ref<environment, messages> run_new_frontend(environment const & env, std::string const & input, options const & opts, std::string const & file_name) {
-    return get_io_result<pair_ref<environment, messages>>(lean_run_frontend(env.to_obj_arg(), mk_string(input), opts.to_obj_arg(), mk_string(file_name), io_mk_world()));
+extern "C" object * lean_run_frontend(object * input, object * opts, object * filename, object * main_module_name, object * w);
+pair_ref<environment, messages> run_new_frontend(std::string const & input, options const & opts, std::string const & file_name, name const & main_module_name) {
+    return get_io_result<pair_ref<environment, messages>>(
+        lean_run_frontend(mk_string(input), opts.to_obj_arg(), mk_string(file_name), main_module_name.to_obj_arg(), io_mk_world()));
 }
 
 extern "C" object* lean_init_search_path(object* opt_path, object* w);
@@ -634,7 +635,9 @@ int main(int argc, char ** argv) {
 
         bool ok = true;
         if (new_frontend) {
-            pair_ref<environment, messages> r = run_new_frontend(env, contents, opts, mod_fn);
+            if (!main_module_name)
+                main_module_name = name("_stdin");
+            pair_ref<environment, messages> r = run_new_frontend(contents, opts, mod_fn, *main_module_name);
             env = r.fst();
             buffer<message> cpp_msgs;
             // HACK: convert Lean Message into C++ message