fix(library/messages,library/init/lean/message): wrap message_log in structure, reverse in the end

library/init/lean/message.lean

@@ -23,15 +23,23 @@ structure message :=
 (caption  : string           := "")
 (text     : string)
 
-def message_log := list message
+structure message_log :=
+-- messages are stored in reverse for efficient append
+(rev_list : list message)
 
 namespace message_log
-def add : message → message_log → message_log :=
-list.cons
+def empty : message_log :=
+⟨[]⟩
+
+def add (msg : message) (log : message_log) : message_log :=
+⟨msg :: log.rev_list⟩
 
 def has_errors (log : message_log) : bool :=
-log.any $ λ m, match m.severity with
+log.rev_list.any $ λ m, match m.severity with
 | message_severity.error := tt
 | _                      := ff
+
+def to_list (log : message_log) : list message :=
+log.rev_list.reverse
 end message_log
 end lean

library/init/lean/parser/basic.lean

@@ -163,7 +163,7 @@ m (syntax × message_log) :=
 do r ← ((r.run cfg).run st).parse_with_eoi s,
 pure $ match r with
 | except.ok (a, st) := (a, st.messages)
-| except.error msg  := (msg.custom, [message_of_parsec_message cfg msg])
+| except.error msg  := (msg.custom, message_log.empty.add (message_of_parsec_message cfg msg))
 end
 
 open monad_parsec
@@ -178,11 +178,11 @@ do cfg ← read,
 def eoi : syntax_node_kind := ⟨`lean.parser.parser.eoi⟩
 
 protected def parse [monad m] (cfg : parser_config) (s : string) (r : parser_t m syntax) [parser.has_tokens r] :
-  m (syntax × list message) :=
+  m (syntax × message_log) :=
 -- the only hardcoded tokens, because they are never directly mentioned by a `parser`
 let builtin_tokens : list token_config := [⟨"/-", 0, none⟩, ⟨"--", 0, none⟩] in
 let trie := (tokens r ++ builtin_tokens).foldl (λ t cfg, trie.insert t cfg.prefix cfg) trie.mk in
-parser.run cfg ⟨trie, [], s.mk_iterator⟩ s $ do
+parser.run cfg ⟨trie, message_log.empty, s.mk_iterator⟩ s $ do
   stx ← catch r $ λ (msg : parsec.message _), do {
     modify $ λ st, {st with token_start := msg.it},
     parser.log_message msg,

src/frontends/lean/definition_cmds.cpp

@@ -600,7 +600,7 @@ environment single_definition_cmd_core(parser & p, decl_cmd_kind kind, cmd_meta
 
         // If we have already logged an error during elaboration, don't
         // bother showing the less helpful kernel exception
-        if (!has_errors(*global_message_log()))
+        if (!global_message_log()->has_errors())
             p.mk_message(header_pos, ERROR).set_exception(ex).report();
         // As a last resort, try replacing the definition body with `sorry`.
         // If that doesn't work either, just silently give up since we have

src/library/messages.cpp

@@ -33,15 +33,7 @@ std::ostream & operator<<(std::ostream & out, message const & msg) {
 
 void report_message(message const & msg0) {
     lean_assert(global_message_log());
-    *global_message_log() = cons(msg0, *global_message_log());
-}
-
-bool has_errors(message_log const & l) {
-    for (auto const & m : l) {
-        if (m.get_severity() == ERROR)
-            return true;
-    }
-    return false;
+    global_message_log()->add(msg0);
 }
 
 LEAN_THREAD_PTR(message_log, g_message_log);
@@ -52,4 +44,26 @@ scope_message_log::scope_message_log(message_log * l) :
 message_log * global_message_log() {
     return g_message_log;
 }
+
+bool message_log::has_errors() const {
+    for (auto const & m : m_rev_list) {
+        if (m.is_error()) {
+            return true;
+        }
+    }
+    return false;
+}
+
+void message_log::add(message const & m) {
+    m_rev_list = cons(m, m_rev_list);
+}
+
+buffer<message> message_log::to_buffer() const {
+    buffer<message> buf;
+    for (auto const & m : m_rev_list) {
+        buf.push_back(m);
+    }
+    std::reverse(buf.begin(), buf.end());
+    return buf;
+}
 }

src/library/messages.h

@@ -78,11 +78,17 @@ std::ostream & operator<<(std::ostream &, message const &);
 void report_message(message const &);
 
 /*
-def message_log := list message
+structure message_log :=
+-- messages are stored in reverse for efficient append
+(rev_list : list message)
 */
-using message_log = list_ref<message>;
-
-bool has_errors(message_log const &);
+class message_log {
+    list_ref<message> m_rev_list;
+public:
+    bool has_errors() const;
+    void add(message const &);
+    buffer<message> to_buffer() const;
+};
 
 struct scope_message_log : flet<message_log *> {
     scope_message_log(message_log *);

src/library/module_mgr.cpp

@@ -83,7 +83,7 @@ static void compile_olean(std::shared_ptr<module_info> const & mod) {
         if (dep.m_mod_info)
             compile_olean(dep.m_mod_info);
 
-    if (mod->m_source != module_src::LEAN || has_errors(mod->m_log))
+    if (mod->m_source != module_src::LEAN || mod->m_log.has_errors())
         return;
     auto res = mod->m_result;
 

src/shell/lean.cpp

@@ -520,13 +520,13 @@ int main(int argc, char ** argv) {
         for (auto & mod : mods) {
             if (test_suite) {
                 std::ofstream out(mod.m_id + ".test_suite.out");
-                for (auto const & msg : mod.m_mod_info->m_log) {
+                for (auto const & msg : mod.m_mod_info->m_log.to_buffer()) {
                     out << msg;
                 }
             }
             if (test_suite) {
                 std::ofstream status(mod.m_id + ".status");
-                status << (!has_errors(mod.m_mod_info->m_log) ? 0 : 1);
+                status << (!mod.m_mod_info->m_log.has_errors() ? 0 : 1);
             }
         }
 
@@ -535,7 +535,7 @@ int main(int argc, char ** argv) {
         bool ok = true;
         if (!test_suite) {
             for (auto & mod : mods) {
-                for (auto const & msg : mod.m_mod_info->m_log) {
+                for (auto const & msg : mod.m_mod_info->m_log.to_buffer()) {
                     if (json_output) {
 #if defined(LEAN_JSON)
                         print_json(std::cout, msg);
@@ -544,7 +544,7 @@ int main(int argc, char ** argv) {
                         std::cout << msg;
                     }
                 }
-                if (has_errors(mod.m_mod_info->m_log))
+                if (mod.m_mod_info->m_log.has_errors())
                     ok = false;
             }
         }

tests/lean/parser1.lean

@@ -3,23 +3,23 @@ open lean
 open lean.parser
 open lean.parser.syntax_node_kind.has_view
 
-def show_result (p : syntax × list lean.message) (s : string) : eio unit :=
-let (stx, errors) := p in
+def show_result (p : syntax × message_log) (s : string) : eio unit :=
+let (stx, msgs) := p in
 when (stx.reprint ≠ s) (
   io.println "reprint fail:" *>
   io.println stx.reprint
 ) *>
-match errors with
+match msgs.to_list with
 | [] := do
   io.println "result: ",
   io.println (to_string stx)
-| _ := do
-  errors.mfor $ λ e, io.println e.text,
+| msgs := do
+  msgs.mfor $ λ e, io.println e.text,
   io.println "partial syntax tree:",
   io.println (to_string stx)
 
-def parse_module (s : string) : syntax × list lean.message :=
-coroutine.finish (λ cmd, ()) (parser.parse ⟨⟩ s module.parser) ()
+def parse_module (s : string) : syntax × message_log :=
+coroutine.finish (λ cmd, ()) (parser.parse ⟨"<unknown>"⟩ s module.parser) ()
 
 def show_parse (s : string) : eio unit :=
 show_result (parse_module s) s
@@ -54,7 +54,7 @@ end b"
 
 -- expansion example
 #eval (do {
-  (stx, []) ← pure $ parse_module "prefix `+`:10 := _",
+  (stx, ⟨[]⟩) ← pure $ parse_module "prefix `+`:10 := _",
   some {root := stx, ..} ← pure $ parser.parse.view stx,
   some {commands := [stx], ..} ← pure $ view module stx,
   some stx ← pure $ mixfix.expand stx | throw "expand fail",
@@ -66,7 +66,7 @@ end b"
 #eval do
   s ← io.fs.read_file "../../library/init/core.lean",
   let s := (s.mk_iterator.nextn 1700).prev_to_string,
-  let k := parser.parse ⟨⟩ s module.parser,
+  let k := parser.parse ⟨"foo"⟩ s module.parser,
   io.prim.iterate_eio k $ λ k, match k.resume () with
     | coroutine_result_core.done p := show_result p s *> pure (sum.inr ())
     | coroutine_result_core.yielded cmd k := do {

tests/lean/parser1.lean.expected.out

@@ -62,10 +62,10 @@ partial syntax tree:
   []
   [(lean.parser.open "open" [(lean.parser.open_spec me [] [] [] [])])])
  (lean.parser.parser.eoi "")]
-error at line 1, column 9:
-expected identifier
 error at line 1, column 5:
 expected identifier
+error at line 1, column 9:
+expected identifier
 partial syntax tree:
 [(lean.parser.module
   []
@@ -150,12 +150,12 @@ result:
  ":="
  (lean.parser.hole "_"))
 notation`+`:10 b:10 :=_
-error at line 85, column 0:
-expected command
-error at line 11, column 26:
-expected "_"
 error at line 10, column 19:
 expected "_"
+error at line 11, column 26:
+expected "_"
+error at line 85, column 0:
+expected command
 partial syntax tree:
 [(lean.parser.module
   [(lean.parser.prelude "prelude")]