chore(tactic/doc_commands): simpler tactic_doc / library_note encoding (#15913)
This does some encoding optimizations on the documentation commands:
* Long strings inside `expr` is a source of stack overflows in lean external checkers because the translation uses a chain of `string.cons` applications, so we should avoid putting doc strings in exprs.
* There is no need to hash names for either `library_note` or `tactic_doc`, because they already come with a unique name.
Concretely:
* Instead of encoding `/-- doc -/ library_note "my note"` as
```lean
@[library_note] def library_note._1234 := ("my note", "doc")
```
we encode it as
```lean
/-- doc -/
@[library_note] def library_note.«my note» := ()
```
so we don't have to do any string -> expr encoding.
* Similarly, the `description` field is removed from `tactic_doc_entry` and its data is moved to the doc string.
mathlib3
5be8529e - chore(tactic/doc_commands): simpler tactic_doc / library_note encoding (#15913)
