feat(tactic): expose module docstrings as list

library/init/meta/tactic.lean

@@ -543,7 +543,7 @@ It updates the environment in the tactic_state, and returns an expression of the
 where l_i's and a_j's are the collected dependencies.
 -/
 meta constant add_aux_decl (c : name) (type : expr) (val : expr) (is_lemma : bool) : tactic expr
-meta constant module_doc_strings : tactic (list (option string × string))
+meta constant module_doc_strings : tactic (list (option string × (list (pos × string))))
 /-- Set attribute `attr_name` for constant `c_name` with the given priority.
    If the priority is none, then use default -/
 meta constant set_basic_attribute (attr_name : name) (c_name : name) (persistent := ff) (prio : option nat := none) : tactic unit

src/frontends/lean/parser.cpp

@@ -2402,7 +2402,7 @@ std::string parser::parse_doc_block() {
 }
 
 void parser::parse_mod_doc_block() {
-    m_env = add_module_doc_string(m_env, m_scanner.get_str_val());
+    m_env = add_module_doc_string(m_env, m_scanner.get_str_val(), m_scanner.get_pos_info() );
     next();
 }
 

src/library/documentation.cpp

@@ -14,8 +14,8 @@ Author: Leonardo de Moura
 
 namespace lean {
 struct documentation_ext : public environment_extension {
-    /** Doc string for the current module being processed. It does not include imported doc strings. */
-    optional<std::string> m_module_doc;
+    /** Doc strings for the current module being processed. It does not include imported doc strings. */
+    std::vector<std::pair<pos_info, std::string>> m_module_docs;
     /** Doc strings for declarations (including imported ones). We store doc_strings for declarations in the .olean files. */
     name_map<std::string> m_doc_string_map;
 };
@@ -167,16 +167,12 @@ static std::string process_doc(std::string s) {
     return add_lean_suffix_to_code_blocks(s);
 }
 
-environment add_module_doc_string(environment const & env, std::string doc) {
+environment add_module_doc_string(environment const & env, std::string doc, pos_info pos) {
     doc = process_doc(doc);
     auto ext = get_extension(env);
-    if (ext.m_module_doc) {
-        *ext.m_module_doc += "\n" + doc;
-    } else {
-        ext.m_module_doc = doc;
-    }
+    ext.m_module_docs.emplace_back(pos, doc);
     auto new_env = update(env, ext);
-    return module::add_doc_string(new_env, doc);
+    return module::add_doc_string(new_env, doc, pos);
 }
 
 environment add_doc_string(environment const & env, name const & n, std::string doc) {
@@ -204,9 +200,7 @@ void get_module_doc_strings(environment const & env, buffer<mod_doc_entry> & res
     for (auto const & pr : mod_docs) {
         result.push_back({ optional<std::string>{ pr.first }, pr.second });
     }
-    if (ext.m_module_doc) {
-        result.push_back({ {}, *ext.m_module_doc });
-    }
+    result.push_back({ {}, ext.m_module_docs });
 }
 
 void initialize_documentation() {

src/library/documentation.h

@@ -7,12 +7,14 @@ Author: Leonardo de Moura
 #pragma once
 #include <string>
 #include "kernel/environment.h"
+#include "util/message_definitions.h"
+
 namespace lean {
 struct mod_doc_entry {
     optional<std::string> m_mod_name;
-    std::string           m_doc;
+    std::vector<std::pair<pos_info, std::string>> m_docs;
 };
-environment add_module_doc_string(environment const & env, std::string doc);
+environment add_module_doc_string(environment const & env, std::string doc, pos_info pos);
 environment add_doc_string(environment const & env, name const & n, std::string);
 optional<std::string> get_doc_string(environment const & env, name const & n);
 void get_module_doc_strings(environment const & env, buffer<mod_doc_entry> & result);

src/library/module.cpp

@@ -90,7 +90,7 @@ struct module_ext : public environment_extension {
      * of module different from that of a source file, so we use file names to index
      * the docstring map. */
     // TODO(Vtec234): lean::rb_map misbehaves here for some reason
-    std::map<std::string, std::string> m_module_docs;
+    std::unordered_map<std::string, std::vector<std::pair<pos_info, std::string>>> m_module_docs;
     // Map from declaration name to olean file where it was defined
     name_map<std::string>     m_decl2olean;
     name_map<pos_info>        m_decl2pos_info;
@@ -425,23 +425,25 @@ struct mod_doc_modification : public modification {
     LEAN_MODIFICATION("mod_doc")
 
     std::string m_doc;
+    pos_info m_pos;
 
     mod_doc_modification() {}
-    /** A docstring for a declaration in the module. */
-    mod_doc_modification(std::string const & doc) : m_doc(doc) {}
+    /** A module-level docstring. */
+    mod_doc_modification(std::string const & doc, pos_info pos) : m_doc(doc), m_pos(pos) {}
 
     void perform(environment & env) const override {
         // No-op. See `import_module` for actual action
     }
 
     void serialize(serializer & s) const override {
-        s << m_doc;
+        s << m_doc << m_pos;
     }
 
     static std::shared_ptr<modification const> deserialize(deserializer & d) {
         std::string doc;
-        d >> doc;
-        return std::make_shared<mod_doc_modification>(doc);
+        pos_info pos;
+        d >> doc >> pos;
+        return std::make_shared<mod_doc_modification>(doc, pos);
     }
 };
 
@@ -535,11 +537,11 @@ environment add(environment const & env, certified_declaration const & d) {
     return add_decl_pos_info(new_env, _d.get_name());
 }
 
-environment add_doc_string(environment const & env, std::string const & doc) {
-    return add(env, std::make_shared<mod_doc_modification>(doc));
+environment add_doc_string(environment const & env, std::string const & doc, pos_info pos) {
+    return add(env, std::make_shared<mod_doc_modification>(doc, pos));
 }
 
-std::map<std::string, std::string> const & get_doc_strings(environment const & env) {
+std::unordered_map<std::string, std::vector<std::pair<pos_info, std::string>>> const & get_doc_strings(environment const & env) {
     return get_extension(env).m_module_docs;
 }
 
@@ -732,11 +734,7 @@ void import_module(modification_list const & modifications, std::string const &
             env = add_decl_olean(env, im->m_decl.get_decl().m_name, file_name);
         } else if (auto mdm = dynamic_cast<mod_doc_modification const *>(m.get())) {
             auto ext = get_extension(env);
-            if (ext.m_module_docs.count(file_name) != 0) {
-                ext.m_module_docs[file_name] += "\n" + mdm->m_doc;
-            } else {
-                ext.m_module_docs[file_name] = mdm->m_doc;
-            }
+            ext.m_module_docs[file_name].emplace_back(mdm->m_pos, mdm->m_doc);
             env = update(env, ext);
         }
     }

src/library/module.h

@@ -5,11 +5,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include <unordered_map>
 #include <string>
 #include <iostream>
 #include <utility>
 #include <vector>
-#include <map>
 #include "util/serializer.h"
 #include "util/optional.h"
 #include "kernel/pos_info_provider.h"
@@ -145,10 +145,10 @@ environment add_and_perform(environment const & env, std::shared_ptr<modificatio
 environment add(environment const & env, certified_declaration const & d);
 
 /** \brief Adds a module-level doc to the current module. */
-environment add_doc_string(environment const & env, std::string const & doc);
+environment add_doc_string(environment const & env, std::string const & doc, pos_info pos);
 
 /** \brief Returns the map of module-level docs indexed by source file name. */
-std::map<std::string, std::string> const & get_doc_strings(environment const & env);
+std::unordered_map<std::string, std::vector<std::pair<pos_info, std::string>>> const & get_doc_strings(environment const & env);
 
 /** \brief Return true iff \c n is a definition added to the current module using #module::add */
 bool is_definition(environment const & env, name const & n);

src/library/tactic/tactic_state.cpp

@@ -758,7 +758,7 @@ vm_obj tactic_add_doc_string(vm_obj const & n, vm_obj const & doc, vm_obj const
     }
 }
 
-/* meta constant module_doc_strings : tactic (list (option string × string)) */
+/* meta constant module_doc_strings : tactic (list (option string × (list (pos × string)))) */
 vm_obj tactic_module_doc_strings(vm_obj const & _s) {
     tactic_state const & s  = tactic::to_state(_s);
     buffer<mod_doc_entry> entries;
@@ -772,8 +772,18 @@ vm_obj tactic_module_doc_strings(vm_obj const & _s) {
             decl_name = mk_vm_some(to_obj(*d));
         else
             decl_name = mk_vm_none();
-        vm_obj doc = to_obj(entries[i].m_doc);
-        vm_obj e   = mk_vm_pair(decl_name, doc);
+        vm_obj lst = mk_vm_simple(0);
+        unsigned j = entries[i].m_docs.size();
+        while (j > 0) {
+            --j;
+            auto const& doc = entries[i].m_docs[j];
+            vm_obj line = mk_vm_nat(doc.first.first);
+            vm_obj column = mk_vm_nat(doc.first.second);
+            vm_obj pos = mk_vm_constructor(0, line, column); // pos_info
+            vm_obj doc_obj = mk_vm_pair(pos, to_obj(doc.second));
+            lst = mk_vm_constructor(1, doc_obj, lst);
+        }
+        vm_obj e   = mk_vm_pair(decl_name, lst);
         r          = mk_vm_constructor(1, e, r);
     }
     return tactic::mk_success(r, s);

tests/lean/doc_strings.lean.expected.out

@@ -1,5 +1,4 @@
 Makes foo.
 Makes foo of foo.
 Doesn't make foo.
-[(none, This module has a doc..
-..or two.)]
+[(none, [(⟨1, 0⟩, This module has a doc..), (⟨2, 0⟩, ..or two.)])]