feat(library/documentation, frontends/lean): add /-! -/ doc string module block

library/init/meta/tactic.lean

@@ -348,6 +348,7 @@ meta constant add_decl : declaration → tactic unit
 /- (doc_string env d k) return the doc string for d (if available) -/
 meta constant doc_string : name → tactic string
 meta constant add_doc_string : name → string → tactic unit
+meta constant module_doc_strings : tactic (list (option name × string))
 /- (set_basic_attribute_core attr_name c_name persistent prio) 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_core : name → name → bool → option nat → tactic unit

src/frontends/lean/parser.cpp

@@ -8,8 +8,7 @@ Author: Leonardo de Moura
 #include <string>
 #include <limits>
 #include <vector>
-#include <util/utf8.h>
-#include <library/export_decl.h>
+#include "util/utf8.h"
 #include "util/interrupt.h"
 #include "util/sstream.h"
 #include "util/flet.h"
@@ -21,6 +20,7 @@ Author: Leonardo de Moura
 #include "kernel/abstract.h"
 #include "kernel/instantiate.h"
 #include "kernel/error_msgs.h"
+#include "library/export_decl.h"
 #include "library/trace.h"
 #include "library/exception.h"
 #include "library/aliases.h"
@@ -40,12 +40,13 @@ Author: Leonardo de Moura
 #include "library/num.h"
 #include "library/string.h"
 #include "library/sorry.h"
+#include "library/documentation.h"
 #include "library/pp_options.h"
 #include "library/noncomputable.h"
 #include "library/scope_pos_info_provider.h"
 #include "library/type_context.h"
-#include "library/equations_compiler/equations.h"
 #include "library/pattern_attribute.h"
+#include "library/equations_compiler/equations.h"
 #include "frontends/lean/tokens.h"
 #include "frontends/lean/builtin_exprs.h"
 #include "frontends/lean/parser.h"
@@ -2075,8 +2076,8 @@ void parser::parse_doc_block() {
 }
 
 void parser::parse_mod_doc_block() {
+    m_env = add_module_doc_string(m_env, m_scanner.get_str_val());
     next();
-    // TODO(Leo): save doc string
 }
 
 void parser::check_no_doc_string() {

src/library/documentation.cpp

@@ -13,7 +13,10 @@ Author: Leonardo de Moura
 
 namespace lean {
 struct documentation_ext : public environment_extension {
-    name_map<std::string> m_doc_strings;
+    /** Doc string for the current module being processed. It does not include imported doc strings. */
+    list<doc_entry>       m_module_doc;
+    /** 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;
 };
 
 struct documentation_ext_reg {
@@ -98,25 +101,39 @@ static std::string process_doc(std::string s) {
     return unindent(s);
 }
 
+environment add_module_doc_string(environment const & env, std::string doc) {
+    doc = process_doc(doc);
+    auto ext = get_extension(env);
+    ext.m_module_doc = cons(doc_entry(doc), ext.m_module_doc);
+    return update(env, ext);
+}
+
 environment add_doc_string(environment const & env, name const & n, std::string doc) {
     doc = process_doc(doc);
     auto ext = get_extension(env);
-    if (ext.m_doc_strings.contains(n)) {
+    if (ext.m_doc_string_map.contains(n)) {
         throw exception(sstream() << "environment already contains a doc string for '" << n << "'");
     }
-    ext.m_doc_strings.insert(n, doc);
+    ext.m_doc_string_map.insert(n, doc);
+    ext.m_module_doc = cons(doc_entry(n, doc), ext.m_module_doc);
     auto new_env = update(env, ext);
     return module::add(new_env, *g_doc_key, [=](environment const &, serializer & s) { s << n << doc; });
 }
 
 optional<std::string> get_doc_string(environment const & env, name const & n) {
     auto ext = get_extension(env);
-    if (auto r = ext.m_doc_strings.find(n))
+    if (auto r = ext.m_doc_string_map.find(n))
         return optional<std::string>(*r);
     else
         return optional<std::string>();
 }
 
+void get_module_doc_strings(environment const & env, buffer<doc_entry> & result) {
+    auto ext = get_extension(env);
+    to_buffer(ext.m_module_doc, result);
+    std::reverse(result.begin(), result.end());
+}
+
 static void documentation_reader(deserializer & d, shared_environment & senv,
                                  std::function<void(asynch_update_fn const &)> &,
                                  std::function<void(delayed_update_fn const &)> &) {
@@ -124,7 +141,7 @@ static void documentation_reader(deserializer & d, shared_environment & senv,
     d >> n >> doc;
     senv.update([=](environment const & env) -> environment {
             auto ext = get_extension(env);
-            ext.m_doc_strings.insert(n, doc);
+            ext.m_doc_string_map.insert(n, doc);
             return update(env, ext);
         });
 }

src/library/documentation.h

@@ -8,8 +8,19 @@ Author: Leonardo de Moura
 #include <string>
 #include "kernel/environment.h"
 namespace lean {
+class doc_entry {
+    optional<name> m_decl_name;
+    std::string    m_doc;
+public:
+    doc_entry(std::string const & doc):m_doc(doc) {}
+    doc_entry(name const & decl_name, std::string const & doc):m_decl_name(decl_name), m_doc(doc) {}
+    optional<name> const & get_decl_name() const { return m_decl_name; }
+    std::string const & get_doc() const { return m_doc; }
+};
+environment add_module_doc_string(environment const & env, std::string doc);
 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<doc_entry> & result);
 void initialize_documentation();
 void finalize_documentation();
 }

src/library/tactic/tactic_state.cpp

@@ -641,6 +641,27 @@ 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 name × string)) */
+vm_obj tactic_module_doc_strings(vm_obj const & _s) {
+    tactic_state const & s  = to_tactic_state(_s);
+    buffer<doc_entry> entries;
+    get_module_doc_strings(s.env(), entries);
+    unsigned i = entries.size();
+    vm_obj r   = mk_vm_simple(0);
+    while (i > 0) {
+        --i;
+        vm_obj decl_name;
+        if (auto d = entries[i].get_decl_name())
+            decl_name = mk_vm_some(to_obj(*d));
+        else
+            decl_name = mk_vm_none();
+        vm_obj doc = to_obj(entries[i].get_doc());
+        vm_obj e   = mk_vm_pair(decl_name, doc);
+        r          = mk_vm_constructor(1, e, r);
+    }
+    return mk_tactic_success(r, s);
+}
+
 void initialize_tactic_state() {
     DECLARE_VM_BUILTIN(name({"tactic_state", "env"}),            tactic_state_env);
     DECLARE_VM_BUILTIN(name({"tactic_state", "format_expr"}),    tactic_state_format_expr);
@@ -675,6 +696,7 @@ void initialize_tactic_state() {
     DECLARE_VM_BUILTIN(name({"tactic", "add_decl"}),             tactic_add_decl);
     DECLARE_VM_BUILTIN(name({"tactic", "doc_string"}),           tactic_doc_string);
     DECLARE_VM_BUILTIN(name({"tactic", "add_doc_string"}),       tactic_add_doc_string);
+    DECLARE_VM_BUILTIN(name({"tactic", "module_doc_strings"}),   tactic_module_doc_strings);
     DECLARE_VM_BUILTIN(name({"tactic", "opened_namespaces"}),    tactic_opened_namespaces);
     g_pp_instantiate_goal_mvars = new name{"pp", "instantiate_goal_mvars"};
     register_bool_option(*g_pp_instantiate_goal_mvars, LEAN_DEFAULT_PP_INSTANTIATE_GOAL_MVARS,

tests/lean/run/doc_string3.lean

@@ -0,0 +1,26 @@
+/-!
+Documentation header for test module
+-/
+
+
+/-- Documentation for x -/
+def x := 10
+
+namespace foo
+/-!
+  Another block of documentation
+  for this example.
+-/
+
+/-- Documentation for y -/
+def y := 20
+
+end foo
+
+/-!
+  Documentation footer
+  testing
+-/
+
+open tactic
+run_command module_doc_strings >>= trace