may documentation be part of program?

Stream: general

[Erika Su]

(It's not a question specific to lean, rather more general question for software engineer)

For lean (or coq, or any other programming language providing rich meta-programming and flexible utillity), is it possible to have certain library and/or compiler plugin such that

/-- documentation on True -/
Inductive Unit where
     unit : Unit

can be compiled into something like

-- definition of Unit
namespace Unit
def doc : DocType := coe "documentation on True"  -- may be complicated as documentation may refer to semantic object, which require a "reference type" for semantic object
end Unit
-- or use attribute to associate documentation with the corresponding item

The relevant issues and advantages of this method might include:

1. Need a way to refer identifier's "name" rather than its value
2. Documentation needs to follows the programs' dependency: suppose A depends on B, B's documentation can't mention A, otherwise causing a loop of dependency. Or documents need to be compiled after the code.
3. Documentation should not be compiled in certain cases, they shall be attributed accordingly.
4. It's convenient for User can provide custom lean-native implementation (via typeclass) for parsing document to custom data and provide output of multiple format.
5. furthermore, it may be possible to attach certain data (format, etc.) to items so that source code can viewed as/compiled to a "notebook" such as jupyter and mathematica, which might be useful for proof assistant.

My question is, is it practical to implement such feature? If so, what need to be added/changed to implement such feature? compiler plugin, preprocessor, or a library (a generalized version of doc-gen4)?

I hope this question is not too bold.

Also, it may be a good idea to give a more conspicuous link to lean4-metaprogramming-book..... I didn't find it til tonight.....

[Eric Wieser]

It's already possibly to programmatically get a docstring for a declaration, if that's your question

[Eric Wieser]

That's how #docs and #docs4 work