fix(library/declaration_index): style

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(emacs): replace metavar '?M_n' with '_' in synthed expr
fix(CMakeLists.txt): use bin/lean to build library

close #49
fix(library): add LEAN_VERSION_FILE to Makefile.common
fix(frontends/lean/parser): uninit variable

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(emacs/lean-flycheck): fix eval-after-load to use library name
feat(frontends/lean): add synthesis information only for 'explicit' placeholder

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/standard): add classes for relations
feat(library/hott): begin porting Coq HoTT
refactor(library/standard): integrate hott with standard library
feat(library/standard/hott/path.lean): add theorems and clean up file
feat(library/standard): add sigma types and subtypes, make inhabited constructive
feat(library/standard/logic): add class nonempty
feat(library/standard/classes): add nonempty
fix(tests/lean/run): adjust test to changes in the library

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(build): remove hott library directory, and move hott tests

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): annotate 'notation' subterms with 'noinfo' annotation (goal: improve typeinfo generation); fix initialization problem (with annotations)

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

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean/server): use separate thread for processing requests in server mode, interrupt whole parser when on interruption (when collecting information)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(doc/server): update server mode documentation

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