feat(frontends/lean/parser): provide environment as an argument to macros, allow macros to parse tactics

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean/parser): add command macros

The idea is to allow users to define their own commands using Lua.
The builtin command Find is now written in Lua.
This commit also fixes a bug in the get_formatter() Lua API.
It also adds String arguments to macros.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean/parser): protect imported modules from Lua definitions and macros in the file importing the module

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean/parser): add existing command macros when creating parser object

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(frontends/lean/parser): tactic macros, and tactic Lua bindings

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(frontends/lean/parser): tactic macros, and tactic Lua bindings