fix(util/stackinfo): handle error codes in the Linux version

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/tactic): add beta-reduction tactic

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/parser): simplified theorem definition using tactical proof

When using tactics for proving theorems, a common pattern is

     Theorem T : <proposition> := _.
          apply <tactic>.
          ...
          done.

This commit allows the user to write the simplified form:

     Theorem T : <proposition>.
          apply <tactic>.
          ...
          done.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(*): typo

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(*): use 'explicit operator bool' everywhere.

operator bool() may produce unwanted conversions.
For example, we had the following bug in the code base.

...
   object const & obj = find_object(const_name(n));
   if (obj && obj.is_builtin() && obj.get_name() == n)
...

obj.get_name() has type lean::name
n              has type lean::expr

Both have 'operator bool()', then the compiler uses the operator to
convert them to Boolean, and then compare the result.
Of course, this is not our intention.

After this commit, the compiler correctly signs the error.
The correct code is

...
   object const & obj = find_object(const_name(n));
   if (obj && obj.is_builtin() && obj.get_name() == const_name(n))
...

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/fo_unify): first order unification

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(*): consistent file name convention

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(*): replace to_expr with to_nonnull_expr (when appropriate)

The goal is to make the Lua API more robust.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(util/stackinfo): compilation warning on mingw and cygwin

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(memcheck): add another suppression for LuaJIT

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(util/stackinfo): try to fix incorrect main thread stack size on OSX

This fix tries to fix two failures on our unit tests.
     tests/kernel/normalizer
     tests/kernel/type_checker

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(util/script_state): add join method to Lua threads

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(util/script_state): add a lua hook function that checks for the interrupt flag

This is a very convenient feature for interrupting non-terminating user scripts.
Before this commit, the user had to manually invoke check_interrupt() in potentially expensive loops. Now, this is not needed anymore.

Remark: we still have to check whether this trick works with LuaJIT or not.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(*): make sure LEAN_THREAD_UNSAFE build flag is handled correctly

When LEAN_THREAD_UNSAFE=ON, we:

- Do not run tests at tests/lua/threads
- Disable thread object at Lua API
- par tactical becomes an alias for interleave
- Disable some unit tests that use threads

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

Remark: on Windows, Ctrl-D does not seem to work.
So, this commit also changes the Lean startup message.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(shell/lean): add git hash to executable

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(util/stackinfo): compilation warning on cygwin/mingw

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean): do not display Ctrl-D message on Windows

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/tactic): add apply_tactic

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

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