test(tests/lean/interactive): add old 'interactive' tests

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): add info_manager

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(frontends/lean): add 'server' module as a replacement for 'interactive'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(frontends/lean): fix style

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean/parser): save snapshots

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): store 'overload' information, remove #setline

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): save type information after elaboration, remove --flyinfo option

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(tests/lean): remove obsolete test

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean): remove duplicate info entries, fix bug in save_overload

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): provide 'partial' type information even when there are type errors

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean): make sure typing information is sorted, make sure the error messages contains line file name

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
doc(server): describe server mode format

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): default for inductive types, closes #32

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/aliases): namespace and constant have the same name, and 'using' produces the 'empty' alias

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(library/kernel_serializer): add assertions for invalid uses of anonymous names

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(util/name): avoid assertion violation when reading numeric names

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/hott/Makefile): specify LEAN_OPTIONS "--hott"
fix(bin/lmake): fix typo LEAN_OPTIONS
feat(emacs/lean-flycheck.el): add lean-flycheck.el
feat(emacs/lean-settings.el): add customization-settings file