feat(kernel/conveter): improve support for proof irrelevant in the converter

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(README.md): remove link to Lean 0.1

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(doc/lean/tutorial): typos

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(emacs/lean-cmd): add set and eval cmds
feat(emacs/lean-syntax): support multi-line comments /- ... -/
refactor(emacs/lean-flycheck): remove lean-flycheck-initialized
refactor(emacs/lean-util): remove unused functions

 - take-first-n/last-n => use -take, -drop (from dash.el)
 - string-join => use one in flycheck
 - remove other unused functions
feat(emacs/lean-settings): add eldoc-use and eldoc-nay-retry-time

close #51
refactor(emacs/lean-server): use global-server-message-to-process

We are using asynchronous process mechanism to communicate between
lean-server and emacs. A sender function like
lean-eldoc-documentation-function sends a command and waits until
lean-global-server-message-to-process is non-nil. When a message is
received from lean-server, a filter function lean-server-output-filter
is triggered. This filter function concatenates a received message to
the buffer until it sees the end of message markers (--
END[INFO|SET|EVAL]). When it sees a marker, it splits the buffer
messages into pre, body, and post parts. Then it assembles a message to
process and attaches the message to
lean-global-server-message-to-process variable. A sender function which
is watching for the variable will recognize it, exit the polling, and
process the message.
feat(emacs/lean-info): use cl-struct lean-info-record
refactor(emacs/lean-type): clean up eldoc-function and fill-placeholder
feat(emacs/lean-mode): use define-derived-mode
feat(emacs/lean-type): add SET/EVAL commands
feat(emacs/lean-cmd): add cmd-to-string for SET/EVAL
refactor(lean-variable): init server-buffer and current-file-name with nil
feat(emacs/lean-type): implement lean-set-option and lean-eval-cmd

close #55
refactor(emacs/lean-server): lean-server-check-current-file takes file-name
fix(emacs/lean-server): when handle dead lean-server
fix(emacs/lean-server): check current-file before send EVAL
feat(emacs/lean-mode): add key-bindings, deps