feat(frontends/lean): add option '-X': discard all proofs after theorems are checked

This option is useful for generating compact .olean files for web demos
feat(library/kernel_serializer): compress binder modifier annotations when saving .olean file
refactor(frontends/lean/parser): add missing 'const'
feat(frontends/lean): elaborate inductive datatypes and introduction rules as a single elaboration problem
chore(version): bump universe level to force .olean recompilation
feat(frontends/lean/inductive_cmd): don't force user to repeat argument declarations in every datatype in a mutually recursive datatype declaration
refactor(library/algebra/category/morphism): make sure bug #231 has been fixed
fix(frontends/lean/parser): segfault when ending scope without opening, fixes #244
fix(library/module): allow multiple calls to import_modules with the same modules

The idea is to store a set of already imported files.
This feature is useful when using the import_modules API directly (e.g.,
from javascript).
chore(library/Makefile): remove unused Makefile
feat(emacs/lean-type): add lean-show-type-add-to-kill-ring option

If a customization option 'lean-show-type-add-to-kill-ring' is non-nil
and a user runs 'lean-show-type' by explicitly typing 'C-c C-t',
lean-mode saves the displayed type information message into kill-ring
, which can be pasted by yank (C-y) command.

Close #245
feat(util/realpath.cpp): add EMSCRIPTEN case for lrealpath
feat(util/lean_path.cpp): add EMSCRIPTEN case for init_lean_path()
feat(CMakeLists.txt): add EMSCRIPTEN support
fixup
checkpoint
checkpoint