feat(emacs/lean-cmd): add WAIT command
feat(emacs/lean-company): call FINDG if cursor is at "_"
feat(emacs/lean-settings): add lean-flycheck-pp-width and lean-flycheck-max-messages-to-display
feat(bin/linja): add --flycheck-max-messages

Close #134
feat(bin/linja): add --cache option

Needed to solve #140
feat(emacs/lean-flycheck): "real" .clean file instead of "flycheck_real.clean"

Fix #140
feat(emacs/lean-mode): add imenu support

Close #97
chore(frontend/lean/pp_options): use consistent name convention for pp option names
refactor(library/logic/classes/decidable): rename 'decidable_eq_to_decidable' theorem to 'of_decidable_eq'
fix(frontends/lean/elaborator): missing constraint
feat(library/unifier): option 'unifier.computation true' will force elaborator to always consider an extra case-split when the right-hand-side of a flex-rigid constraint is not in weak-head-normal-form
refactor(library/unifier): move all_local outside of the class
fix(library/unifier): catch type error when checking is_def_eq of type incorrect expressions
feat(library/unifier): consider whnf case-split on flex-rigid constraints whenever the rhs contains a local constant that is not in the lhs
fix(tests/lean/interactive): interactive tests expected output, they must include the new '-- BEGINWAIT' messages

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(bin/linja): add build_ninja_and_save_at

Fix #129
feat(frontends/lean/server): add timebound to WAIT command, closes #156

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean/server): unifier maximum number of steps error in FINDG, closes #155

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(bin/linja): allow non-exist cache argument

Fix #163
fix(bin/linja): pass args to call_lean and handle_failure_for_flycheck

Fix #163