feat(library,frontends/lean): add basic doc string support

library/init/meta/tactic.lean

@@ -345,6 +345,9 @@ meta constant generalize_core : transparency → expr → name → tactic unit
 meta constant instantiate_mvars : expr → tactic expr
 /- Add the given declaration to the environment -/
 meta constant add_decl : declaration → tactic unit
+/- (doc_string env d) return the doc string for d (if available) -/
+meta constant doc_string : name → tactic string
+meta constant add_doc_string : name → string → tactic unit
 /- (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/builtin_cmds.cpp

@@ -28,6 +28,7 @@ Author: Leonardo de Moura
 #include "library/type_context.h"
 #include "library/reducible.h"
 #include "library/typed_expr.h"
+#include "library/documentation.h"
 #include "library/vm/vm.h"
 #include "library/vm/vm_string.h"
 #include "library/compiler/vm_compiler.h"
@@ -107,6 +108,9 @@ environment namespace_cmd(parser & p) {
     unsigned old_export_decls_sz = length(get_active_export_decls(p.env()));
     environment env = push_scope(p.env(), p.ios(), scope_kind::Namespace, n);
     env = activate_export_decls(env, get_namespace(env));
+    if (auto doc = p.get_doc_string()) {
+        env = add_doc_string(env, get_namespace(env), *doc);
+    }
     return replay_export_decls_core(env, p.ios(), old_export_decls_sz);
 }
 

src/frontends/lean/decl_cmds.cpp

@@ -22,6 +22,7 @@ Author: Leonardo de Moura
 #include "library/locals.h"
 #include "library/explicit.h"
 #include "library/unfold_macros.h"
+#include "library/documentation.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/decl_util.h"
 #include "frontends/lean/util.h"
@@ -125,6 +126,8 @@ static environment declare_var(parser & p, environment env,
             bool is_trusted = !modifiers.m_is_meta;
             env = module::add(env, check(env, mk_constant_assumption(full_n, ls, new_type, is_trusted)));
         }
+        if (auto doc = p.get_doc_string())
+            env = add_doc_string(env, full_n, *doc);
         if (!ns.is_anonymous()) {
             if (modifiers.m_is_protected)
                 env = add_expr_alias(env, get_protected_shortest_name(full_n), full_n);

src/frontends/lean/definition_cmds.cpp

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include <string>
 #include "util/timeit.h"
 #include "kernel/type_checker.h"
 #include "kernel/declaration.h"
@@ -19,6 +20,7 @@ Author: Leonardo de Moura
 #include "library/unfold_macros.h"
 #include "library/noncomputable.h"
 #include "library/module.h"
+#include "library/documentation.h"
 #include "library/scope_pos_info_provider.h"
 #include "library/replace_visitor.h"
 #include "library/equations_compiler/equations.h"
@@ -318,7 +320,8 @@ static expr fix_rec_fn_name(expr const & e, name const & c_name, name const & c_
 static pair<environment, name>
 declare_definition(parser & p, environment const & env, def_cmd_kind kind, buffer<name> const & lp_names,
                    name const & c_name, expr const & type, expr const & _val,
-                   decl_modifiers const & modifiers, decl_attributes attrs, pos_info const & pos) {
+                   decl_modifiers const & modifiers, decl_attributes attrs, optional<std::string> const & doc_string,
+                   pos_info const & pos) {
     auto env_n = mk_real_name(env, c_name, modifiers.m_is_private, pos);
     environment new_env = env_n.first;
     name c_real_name    = env_n.second;
@@ -349,6 +352,9 @@ declare_definition(parser & p, environment const & env, def_cmd_kind kind, buffe
 
     new_env = attrs.apply(new_env, p.ios(), c_real_name);
     new_env = compile_decl(p, new_env, kind, modifiers.m_is_noncomputable, c_name, c_real_name, pos);
+    if (doc_string) {
+        new_env = add_doc_string(new_env, c_real_name, *doc_string);
+    }
     return mk_pair(new_env, c_real_name);
 }
 
@@ -554,6 +560,7 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif
     buffer<expr> params;
     expr fn, val;
     auto header_pos = p.pos();
+    optional<std::string> doc_string = p.get_doc_string();
     module::scope_pos_info scope_pos(header_pos);
     declaration_info_scope scope(p, kind, modifiers);
     bool is_example  = (kind == def_cmd_kind::Example);
@@ -582,7 +589,7 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif
         }
         finalize_definition(elab, new_params, type, val, lp_names);
         name c_name = mlocal_name(fn);
-        auto env_n  = declare_definition(p, elab.env(), kind, lp_names, c_name, type, val, modifiers, attrs, header_pos);
+        auto env_n  = declare_definition(p, elab.env(), kind, lp_names, c_name, type, val, modifiers, attrs, doc_string, header_pos);
         if (kind == Example) return p.env();
         environment new_env = env_n.first;
         name c_real_name    = env_n.second;

src/frontends/lean/inductive_cmds.cpp

@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Daniel Selsam, Leonardo de Moura
 */
 #include <algorithm>
-#include <library/attribute_manager.h>
+#include <string>
 #include "util/sstream.h"
 #include "util/name_map.h"
 #include "util/fresh_name.h"
@@ -17,6 +17,7 @@ Authors: Daniel Selsam, Leonardo de Moura
 #include "kernel/free_vars.h"
 #include "library/scoped_ext.h"
 #include "library/locals.h"
+#include "library/attribute_manager.h"
 #include "library/deep_copy.h"
 #include "library/placeholder.h"
 #include "library/aliases.h"
@@ -27,6 +28,7 @@ Authors: Daniel Selsam, Leonardo de Moura
 #include "library/trace.h"
 #include "library/app_builder.h"
 #include "library/type_context.h"
+#include "library/documentation.h"
 #include "library/inductive_compiler/add_decl.h"
 #include "frontends/lean/decl_cmds.h"
 #include "frontends/lean/decl_util.h"
@@ -72,6 +74,7 @@ class inductive_cmd_fn {
     level                           m_u; // temporary auxiliary global universe used for inferring the result
                                          // universe of an inductive datatype declaration.
     bool                            m_infer_result_universe{false};
+    optional<std::string>           m_doc_string;
 
     [[ noreturn ]] void throw_error(char const * error_msg) const { throw parser_error(error_msg, m_pos); }
     [[ noreturn ]] void throw_error(sstream const & strm) const { throw parser_error(strm, m_pos); }
@@ -480,13 +483,20 @@ public:
         m_env = m_env.add_universe(tmp_global_univ_name());
         m_u = mk_global_univ(tmp_global_univ_name());
         check_attrs(m_attrs);
+        m_doc_string = p.get_doc_string();
     }
 
     void post_process(buffer<expr> const & new_params, buffer<expr> const & new_inds, buffer<buffer<expr> > const & new_intro_rules) {
         add_aliases(new_params, new_inds, new_intro_rules);
         add_namespaces(new_inds);
-        for (expr const & ind : new_inds)
+        for (expr const & ind : new_inds) {
             m_env = m_attrs.apply(m_env, m_p.ios(), mlocal_name(ind));
+            /* TODO(Leo): add support for doc-strings in mutual inductive definitions.
+               We are currently using the same doc string for all elements.
+            */
+            if (m_doc_string)
+                m_env = add_doc_string(m_env, mlocal_name(ind), *m_doc_string);
+        }
         if (!m_mut_attrs.empty()) {
             lean_assert(new_inds.size() == m_mut_attrs.size());
             for (unsigned i = 0; i < new_inds.size(); ++i)

src/frontends/lean/parser.cpp

@@ -1944,7 +1944,8 @@ unsigned parser::curr_lbp() const {
         else
             return get_token_info().expr_precedence();
     case scanner::token_kind::CommandKeyword: case scanner::token_kind::Eof:
-    case scanner::token_kind::QuotedSymbol:
+    case scanner::token_kind::QuotedSymbol:   case scanner::token_kind::DocBlock:
+    case scanner::token_kind::ModDocBlock:
         return 0;
     case scanner::token_kind::Identifier:     case scanner::token_kind::Numeral:
     case scanner::token_kind::Decimal:        case scanner::token_kind::String:
@@ -2028,11 +2029,22 @@ public:
     virtual optional<expr> is_stuck(expr const & e) override { return ctx().is_stuck(e); }
 };
 
+static name_set * g_documentable_cmds = nullptr;
+
+static bool support_docummentation(name const & n) {
+    return g_documentable_cmds->contains(n);
+}
+
 void parser::parse_command() {
     lean_assert(curr() == scanner::token_kind::CommandKeyword);
     m_last_cmd_pos = pos();
     name cmd_name = get_token_info().value();
     m_cmd_token = get_token_info().token();
+    if (m_doc_string && !support_docummentation(cmd_name)) {
+        next();
+        reset_doc_string();
+        throw parser_error(sstream() << "command '" << cmd_name << "' does not support doc string", m_last_cmd_pos);
+    }
     if (auto it = cmds().find(cmd_name)) {
         lazy_type_context tc(m_env, get_options());
         scope_global_ios scope1(m_ios);
@@ -2049,10 +2061,35 @@ void parser::parse_command() {
             m_env = it->get_fn()(*this);
         }
     } else {
+        reset_doc_string();
         auto p = pos();
         next();
         throw parser_error(sstream() << "unknown command '" << cmd_name << "'", p);
     }
+    reset_doc_string();
+}
+
+void parser::parse_doc_block() {
+    m_doc_string = m_scanner.get_str_val();
+    next();
+}
+
+void parser::parse_mod_doc_block() {
+    next();
+    // TODO(Leo): save doc string
+}
+
+void parser::check_no_doc_string() {
+    if (m_doc_string) {
+        auto p = pos();
+        next();
+        reset_doc_string();
+        throw parser_error("invalid occurrence of doc string immediately before current position", p);
+    }
+}
+
+void parser::reset_doc_string() {
+    m_doc_string = optional<std::string>();
 }
 
 static optional<std::string> try_file(std::string const & base, optional<unsigned> const & k, name const & f, char const * ext) {
@@ -2174,15 +2211,27 @@ bool parser::parse_commands() {
                     check_interrupted();
                     switch (curr()) {
                     case scanner::token_kind::CommandKeyword:
-                        if (curr_is_token(get_end_tk()))
+                        if (curr_is_token(get_end_tk())) {
+                            check_no_doc_string();
                             save_snapshot();
+                        }
                         parse_command();
                         save_snapshot();
                         break;
+                    case scanner::token_kind::DocBlock:
+                        check_no_doc_string();
+                        parse_doc_block();
+                        break;
+                    case scanner::token_kind::ModDocBlock:
+                        check_no_doc_string();
+                        parse_mod_doc_block();
+                        break;
                     case scanner::token_kind::Eof:
+                        check_no_doc_string();
                         done = true;
                         break;
                     case scanner::token_kind::Keyword:
+                        check_no_doc_string();
                         if (curr_is_token(get_period_tk())) {
                             next();
                             break;
@@ -2306,6 +2355,20 @@ void initialize_parser() {
                          "(lean parser) import modules in parallel");
     g_tmp_prefix = new name(name::mk_internal_unique_name());
     g_anonymous_inst_name_prefix = new name("_inst");
+    g_documentable_cmds = new name_set();
+
+    g_documentable_cmds->insert("namespace");
+    g_documentable_cmds->insert("definition");
+    g_documentable_cmds->insert("theorem");
+    g_documentable_cmds->insert("constant");
+    g_documentable_cmds->insert("axiom");
+    g_documentable_cmds->insert("meta");
+    g_documentable_cmds->insert("mutual");
+    g_documentable_cmds->insert("@[");
+    g_documentable_cmds->insert("protected");
+    g_documentable_cmds->insert("class");
+    g_documentable_cmds->insert("inductive");
+    g_documentable_cmds->insert("structure");
 }
 
 void finalize_parser() {
@@ -2313,5 +2376,6 @@ void finalize_parser() {
     delete g_tmp_prefix;
     delete g_parser_show_errors;
     delete g_parser_parallel_import;
+    delete g_documentable_cmds;
 }
 }

src/frontends/lean/parser.h

@@ -147,6 +147,9 @@ class parser : public abstract_parser {
     // noncomputable definitions not tagged as noncomputable.
     bool                   m_ignore_noncomputable;
 
+    // Docgen
+    optional<std::string>  m_doc_string;
+
     void throw_parser_exception(char const * msg, pos_info p);
     void throw_nested_exception(throwable const & ex, pos_info p);
 
@@ -167,6 +170,10 @@ class parser : public abstract_parser {
 
     void parse_imports();
     void check_modules_up_to_date();
+    void parse_doc_block();
+    void parse_mod_doc_block();
+    void check_no_doc_string();
+    void reset_doc_string();
     void parse_command();
     bool parse_commands();
     unsigned curr_lbp_core() const;
@@ -266,6 +273,8 @@ public:
     pos_info cmd_pos() const { return m_last_cmd_pos; }
     name const & get_cmd_token() const { return m_cmd_token; }
 
+    optional<std::string> get_doc_string() const { return m_doc_string; }
+
     expr mk_app(expr fn, expr arg, pos_info const & p);
     expr mk_app(expr fn, buffer<expr> const & args, pos_info const & p);
     expr mk_app(std::initializer_list<expr> const & args, pos_info const & p);

src/frontends/lean/scanner.cpp

@@ -351,6 +351,32 @@ void scanner::read_single_line_comment() {
     }
 }
 
+void scanner::read_doc_block_core() {
+    m_buffer.clear();
+    while (true) {
+        check_not_eof("unexpected end of documentation block");
+        char c = curr();
+        next();
+        if (c == '-') {
+            if (curr() == '/') {
+                next();
+                return;
+            }
+        }
+        m_buffer += c;
+    }
+}
+
+auto scanner::read_doc_block() -> token_kind {
+    read_doc_block_core();
+    return token_kind::DocBlock;
+}
+
+auto scanner::read_mod_doc_block() -> token_kind {
+    read_doc_block_core();
+    return token_kind::ModDocBlock;
+}
+
 void scanner::read_comment_block() {
     unsigned nesting = 1;
     while (true) {
@@ -537,17 +563,23 @@ auto scanner::read_key_cmd_id() -> token_kind {
 
 static name * g_begin_comment_tk        = nullptr;
 static name * g_begin_comment_block_tk  = nullptr;
+static name * g_begin_doc_block_tk      = nullptr;
+static name * g_begin_mod_doc_block_tk  = nullptr;
 static name * g_pound_tk                = nullptr;
 
 void initialize_scanner() {
     g_begin_comment_tk       = new name("--");
     g_begin_comment_block_tk = new name("/-");
+    g_begin_doc_block_tk     = new name("/--");
+    g_begin_mod_doc_block_tk = new name("/-!");
     g_pound_tk               = new name("#");
 }
 
 void finalize_scanner() {
     delete g_begin_comment_tk;
     delete g_begin_comment_block_tk;
+    delete g_begin_doc_block_tk;
+    delete g_begin_mod_doc_block_tk;
     delete g_pound_tk;
 }
 
@@ -577,12 +609,16 @@ auto scanner::scan(environment const & env) -> token_kind {
             } else {
                 token_kind k = read_key_cmd_id();
                 if (k == token_kind::Keyword) {
-                    // We treat '(--', '(*', '--' as "keyword".
+                    // We treat '/-', '/--', '/-!', '--' as "keyword".
                     name const & n = m_token_info.value();
                     if (n == *g_begin_comment_tk)
                         read_single_line_comment();
                     else if (n == *g_begin_comment_block_tk)
                         read_comment_block();
+                    else if (n == *g_begin_doc_block_tk)
+                        return read_doc_block();
+                    else if (n == *g_begin_mod_doc_block_tk)
+                        return read_mod_doc_block();
                     else if (n == *g_pound_tk && curr() == '"')
                         return read_char();
                     else

src/frontends/lean/scanner.h

@@ -24,7 +24,9 @@ namespace lean {
 */
 class scanner {
 public:
-    enum class token_kind {Keyword, CommandKeyword, Identifier, Numeral, Decimal, String, Char, QuotedSymbol, Eof};
+    enum class token_kind {Keyword, CommandKeyword, Identifier, Numeral, Decimal,
+                           String, Char, QuotedSymbol,
+                           DocBlock, ModDocBlock, Eof};
 protected:
     token_table const * m_tokens;
     std::istream &      m_stream;
@@ -76,6 +78,9 @@ protected:
     token_kind read_number();
     token_kind read_key_cmd_id();
     token_kind read_quoted_symbol();
+    void read_doc_block_core();
+    token_kind read_doc_block();
+    token_kind read_mod_doc_block();
 
 public:
     scanner(std::istream & strm, char const * strm_name = nullptr);

src/frontends/lean/structure_cmd.cpp

@@ -38,6 +38,7 @@ Author: Leonardo de Moura
 #include "library/kernel_serializer.h"
 #include "library/type_context.h"
 #include "library/app_builder.h"
+#include "library/documentation.h"
 #include "library/compiler/vm_compiler.h"
 #include "library/constructions/rec_on.h"
 #include "library/constructions/induction_on.h"
@@ -84,6 +85,7 @@ struct structure_cmd_fn {
     name                        m_namespace;
     name                        m_name;
     name                        m_given_name;
+    optional<std::string>       m_doc_string;
     pos_info                    m_name_pos;
     buffer<name>                m_level_names;
     decl_attributes             m_attrs;
@@ -117,6 +119,7 @@ struct structure_cmd_fn {
         m_infer_result_universe    = false;
         m_inductive_predicate      = false;
         m_prio                     = get_default_priority(p.get_options());
+        m_doc_string               = p.get_doc_string();
     }
 
     void check_attrs(decl_attributes const & attrs, pos_info const & pos) const {
@@ -838,6 +841,11 @@ struct structure_cmd_fn {
         add_alias(no_confusion_name);
     }
 
+    void add_doc_string() {
+        if (m_doc_string)
+            m_env = ::lean::add_doc_string(m_env, m_name, *m_doc_string);
+    }
+
     environment operator()() {
         process_header();
         module::scope_pos_info scope(m_name_pos);
@@ -871,6 +879,7 @@ struct structure_cmd_fn {
         declare_projections();
         declare_auxiliary();
         declare_coercions();
+        add_doc_string();
         if (!m_inductive_predicate) {
             declare_no_confustion();
         }

src/frontends/lean/token_table.cpp

@@ -89,7 +89,7 @@ void init_token_table(token_table & t) {
          {"⊢", 0}, {"⟨", g_max_prec}, {"⟩", 0}, {"^", 0}, {"↑", 0}, {"▸", 0},
          {"//", 0}, {"|", 0}, {"!", g_max_prec}, {"?", 0},  {"with", 0}, {"without", 0}, {"...", 0}, {",", 0},
          {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {"as", 0}, {":=", 0}, {"--", 0}, {"#", g_max_prec},
-         {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"using", 0},
+         {"(*", 0}, {"/-", 0}, {"/--", 0}, {"/-!", 0}, {"begin", g_max_prec}, {"using", 0},
          {"@@", g_max_prec}, {"@", g_max_prec},
          {"sorry", g_max_prec}, {"+", g_plus_prec}, {"->", g_arrow_prec}, {"<-", 0},
          {"?(", g_max_prec}, {"⌞", g_max_prec}, {"⌟", 0}, {"match", 0},
@@ -104,7 +104,7 @@ void init_token_table(token_table & t) {
          "variables", "parameter", "parameters", "constant", "constants",
          "evaluate", "check", "eval", "vm_eval", "using_well_founded", "[whnf]",
          "print", "end", "namespace", "section", "prelude", "help",
-         "import", "inductive", "record", "structure", "class", "universe", "universes", "local",
+         "import", "inductive", "structure", "class", "universe", "universes", "local",
          "precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation",
          "exit", "set_option", "open", "export", "override", "@[",
          "attribute", "persistent", "instance", "include", "omit", "init_quotient",

src/library/CMakeLists.txt

@@ -16,4 +16,4 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
   mpq_macro.cpp arith_instance_manager.cpp replace_visitor_with_tc.cpp
   aux_definition.cpp inverse.cpp library_system.cpp pattern_attribute.cpp choice.cpp
   locals.cpp normalize.cpp discr_tree.cpp
-  messages.cpp message_builder.cpp comp_val.cpp)
+  messages.cpp message_builder.cpp comp_val.cpp documentation.cpp)

src/library/documentation.cpp

@@ -0,0 +1,74 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <string>
+#include "util/sstream.h"
+#include "library/module.h"
+
+namespace lean {
+struct documentation_ext : public environment_extension {
+    name_map<std::string> m_doc_strings;  // map: declaration/namespace -> doc string
+};
+
+struct documentation_ext_reg {
+    unsigned m_ext_id;
+    documentation_ext_reg() { m_ext_id = environment::register_extension(std::make_shared<documentation_ext>()); }
+};
+
+static documentation_ext_reg * g_ext = nullptr;
+static documentation_ext const & get_extension(environment const & env) {
+    return static_cast<documentation_ext const &>(env.get_extension(g_ext->m_ext_id));
+}
+static environment update(environment const & env, documentation_ext const & ext) {
+    return env.update(g_ext->m_ext_id, std::make_shared<documentation_ext>(ext));
+}
+
+static name * g_documentation = nullptr;
+static std::string * g_doc_key = nullptr;
+
+environment add_doc_string(environment const & env, name const & n, std::string const & doc) {
+    auto ext = get_extension(env);
+    if (ext.m_doc_strings.contains(n)) {
+        throw exception(sstream() << "environment already contains a doc string for '" << n << "'");
+    }
+    ext.m_doc_strings.insert(n, 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))
+        return optional<std::string>(*r);
+    else
+        return optional<std::string>();
+}
+
+static void documentation_reader(deserializer & d, shared_environment & senv,
+                                 std::function<void(asynch_update_fn const &)> &,
+                                 std::function<void(delayed_update_fn const &)> &) {
+    name n; std::string doc;
+    d >> n >> doc;
+    senv.update([=](environment const & env) -> environment {
+            auto ext = get_extension(env);
+            ext.m_doc_strings.insert(n, doc);
+            return update(env, ext);
+        });
+}
+
+void initialize_documentation() {
+    g_ext     = new documentation_ext_reg();
+    g_documentation = new name("documentation");
+    g_doc_key = new std::string("doc");
+    register_module_object_reader(*g_doc_key, documentation_reader);
+}
+
+void finalize_documentation() {
+    delete g_doc_key;
+    delete g_documentation;
+    delete g_ext;
+}
+}

src/library/documentation.h

@@ -0,0 +1,15 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include <string>
+#include "kernel/environment.h"
+namespace lean {
+environment add_doc_string(environment const & env, name const & n, std::string const & doc);
+optional<std::string> get_doc_string(environment const & env, name const & n);
+void initialize_documentation();
+void finalize_documentation();
+}

src/library/init_module.cpp

@@ -48,6 +48,7 @@ Author: Leonardo de Moura
 #include "library/inverse.h"
 #include "library/pattern_attribute.h"
 #include "library/comp_val.h"
+#include "library/documentation.h"
 
 namespace lean {
 void initialize_library_core_module() {
@@ -106,9 +107,11 @@ void initialize_library_module() {
     initialize_inverse();
     initialize_pattern_attribute();
     initialize_comp_val();
+    initialize_documentation();
 }
 
 void finalize_library_module() {
+    finalize_documentation();
     finalize_comp_val();
     finalize_pattern_attribute();
     finalize_inverse();

src/library/tactic/tactic_state.cpp

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include <string>
 #include "util/fresh_name.h"
 #include "util/sexpr/option_declarations.h"
 #include "kernel/type_checker.h"
@@ -15,10 +16,12 @@ Author: Leonardo de Moura
 #include "library/util.h"
 #include "library/cache_helper.h"
 #include "library/module.h"
+#include "library/documentation.h"
 #include "library/scoped_ext.h"
 #include "library/vm/vm_environment.h"
 #include "library/vm/vm_exceptional.h"
 #include "library/vm/vm_format.h"
+#include "library/vm/vm_string.h"
 #include "library/vm/vm_options.h"
 #include "library/vm/vm_name.h"
 #include "library/vm/vm_nat.h"
@@ -619,6 +622,25 @@ vm_obj tactic_opened_namespaces(vm_obj const & s) {
     return mk_tactic_success(to_obj(get_namespaces(env)), to_tactic_state(s));
 }
 
+vm_obj tactic_doc_string(vm_obj const & n, vm_obj const & _s) {
+    tactic_state const & s  = to_tactic_state(_s);
+    if (optional<std::string> doc = get_doc_string(s.env(), to_name(n))) {
+        return mk_tactic_success(to_obj(*doc), s);
+    } else {
+        return mk_tactic_exception(sstream() << "no doc string for '" << n << "'", s);
+    }
+}
+
+vm_obj tactic_add_doc_string(vm_obj const & n, vm_obj const & doc, vm_obj const & _s) {
+    tactic_state const & s  = to_tactic_state(_s);
+    try {
+        environment new_env = add_doc_string(s.env(), to_name(n), to_string(doc));
+        return mk_tactic_success(set_env(s, new_env));
+    } catch (throwable & ex) {
+        return mk_tactic_exception(ex, 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);
@@ -651,6 +673,8 @@ void initialize_tactic_state() {
     DECLARE_VM_BUILTIN(name({"tactic", "is_trace_enabled_for"}), tactic_is_trace_enabled_for);
     DECLARE_VM_BUILTIN(name({"tactic", "instantiate_mvars"}),    tactic_instantiate_mvars);
     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", "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/600c.lean

@@ -1,9 +1,9 @@
 /- /- -/ -/
 /- - /--/-/
 /-/-/--/-/-/
-/--/
-/------------/
-/---/
+/- -/
+/- -----------/
+/- --/
 /- ---/
 /-
 -/

tests/lean/run/doc_string1.lean

@@ -0,0 +1,48 @@
+/--
+Documentation for x
+
+Testing...
+-/
+def x := 10 + 20
+
+def y := "alo"
+
+open tactic
+
+run_command do
+  d   ← doc_string `x,
+  trace d
+
+run_command add_doc_string `y "testing simple doc"
+
+run_command do
+  d   ← doc_string `y,
+  trace d
+
+/-- Documentation for foo -/
+namespace foo
+  /-- Documentation for bla -/
+  namespace bla
+  /-- Documentation for single -/
+  inductive single
+  | unit
+
+  end bla
+end foo
+
+run_command do
+  doc_string `foo >>= trace,
+  doc_string `foo.bla >>= trace,
+  doc_string `foo.bla.single >>= trace
+
+
+/-- Documentation for constant A -/
+constant A : Type
+
+run_command doc_string `A >>= trace
+
+/-- Documentation for point -/
+structure point :=
+(x : nat) (y : nat)
+
+run_command doc_string `point >>= trace