feat(library/scoped_ext): allow extensions to mark whether an entry is
persistent or not
feat(frontends/lean): allow transient coercions, i.e., coercions that
are not saved in .olean files
feat(frontends/lean): allow transient classes/instances, i.e.,
classes/instances that are not saved in .olean files
feat(frontends/lean): definitions are opaque by default
feat(frontends/lean): add 'reducible' modifier for controlling which
definitions are unfolded during elaboration

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(frontends/lean): replace '[opaque]' modifier with 'opaque
definition', '[opaque]' is not a hint, but a kind of definition
refactor(frontends/lean): replace '[private]' modifier with 'private
definition' and 'private theorem', '[private]' is not a hint.
refactor(frontends/lean): replace '[protected]' modifier with 'protected definition' and 'protected theorem', '[protected]' is not a hint.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): add 'irreducible' as syntax sugar for 'reducible [off]'
refactor(library/data/vector): rename 'vec' to 'vector'
doc(declarations): private, opaque, protected definitions
doc(reducible): add documentation for reducible hints.
fix(emacs/lean-flycheck): support windows

In windows, we need to first call python interpreter to call linja.
fix(emacs/lean-tags): support windows
fix(bin/linja): support windows

':' has a special meaning in build.ninja and has to be escaped. In
windows, ':' is used for drive names (i.e. c:).
refactor(bin/linja): clean up