refactor(kernel/expr): remove the dangerous expr::release method

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(library/tactic): remove 'null' tactic, and operator bool tactics

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean/parser): reachable code

The new test nbug1.lean exposes the problem.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(kernel/formatter): hide 'unsafe' constructor

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(frontends/lean/pp): replace dangerous frontend reference with a weak_ref to the environment

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/kernel_bindings): make sure that when a formatter is invoked and it has a reference to an environment object, we get a read-only lock to the environment object

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(frontends/lean/pp): replace weak_ref with a strong reference, add new function (lean_formatter) for creating a Lean object formatter in the Lua API

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean/frontend): is_coercion for environment objects that have parents

Bug was exposed by tests/lua/coercion_bug1.lua

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(kernel/unification_constraint): remove 'null' unification_constraint and its operator bool

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