feat(frontends/lean): process theorem statement independently of proof, thus we have the same behavior in sequential and parallel compilation modes, closes #84

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

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library): minor cleanup, replace 'refl _' with 'rfl', define equivalence relation for sets

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library): correct markdown directories, revise defaults for logic and data
refactor(library): set up and document standard/classical/hott imports
chore(library): add 'universe polymorphism' to list of extra feat

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/num): bug in to_pos_num, missing test

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean): fail if theorem type has metavariables after type elaboration (and before proof elaboration)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/unifier): assertion violation

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

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(util/rb_tree): do not use thread local storage in template when compiling on OSX with clang++ without Boost

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean/info_manager): do not rely on typeid::before, the behavior is a platform specific

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(tests/lua/slow): reduce test size to avoid stackoverflow on OSX when compiling without Boost

Signed-off-by: Leonardo de Moura <leodemoura@cmacslab5.modck.cs.cmu.edu>
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