fix(emacs/lean-info): type of a symbol at the end of buffer
fix(emacs/lean-info): handle when both identifier and symbol info exist

Example: library/data/int/basic.lean file (398, 22)

The '+' symbol is attached with both of identifier info and symbol info

-- SYMBOL|398|22
+
-- ACK
-- IDENTIFIER|398|22
int.add
-- ACK
fix(emacs/lean-type): problem with lean-eldoc-nay-retry-time

If (current-idle-time) is non-zero, we need to set a timer to run
eldoc-documentation-function again when idle-time = (current-idle-time)
+ retry-delay.
feat(emacs/lean-type): maintain nay-retry timer
fix(library/Makefile): ignore flycheck generated files in the Makefile, fixes #101

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(util/lean_path): if directory 'foo' does not contain 'default.lean', then we should also check whether the file 'foo.lean' exists or not, fixes #102

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(util/lean_path): throws an exception if there is an ambiguity when importing a module

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean/server): add CLEAR_CACHE command, closes #100

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean/server): ignore output produced by worker thread, fixes #98

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(frontends/lean/server): refactor lean info server, closes #90, closes #69

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean): distribute '@' over choice

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(library/logic/connectives): make dependence prop <- eq <- basic
fix(frontends/lean/server): compilation warning

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(tests/lean/run/class_coe): adjust test to reflect library changes

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(library/logic/basic): rename absurd_elim to absurd, delete contrapos and trivial_not_true theorems

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(library/logic): rename connectives -> core, basic -> connectives
feat(frontends/lean/server): preserve info that occurs in columns before first changed column

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean/server): add ECHO command for debugging purposes

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
test(tests/lean/interactive): add --server test

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(src/emacs): add 'begin' reserved keyword

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>