feat(frontends/lean/server): display current option value instead of default value

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(frontends/lean/server): move option display_value to option_declarations

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean/elaborator): generate COERCION info

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean/server): add NAY and STALE status to --BEGININFO

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(emacs/lean-mode): remove lean-tab function
feat(emacs): implement non-blocking communication

The key idea is to pass a continuation function when we call
lean-server-send-cmd function. The passed continuation function is
called by lean-server-event-handler. Until the buffer is ready, the
event handler will be called in interval (lean-server-retry-time, 0.1
sec by default). When we have 'NAY' for INFO command, it will re-send
INFO commands to lean-server until we have one without 'NAY'.

Close #123
feat(emacs/lean-server): support SHOW and VALID

Implement lean-server-show and lean-server-valid functions.

Close #116
feat(emacs/lean-info): add coercion and stale in type info

Close #124
feat(emacs): use lexical scope for lean-info and lean-server
checkpoint for imenu