The type checker (and type inferer) were not handling correctly Pi expressions where the type universe cannot be established due to the occurrence of metavariables. In this case, a max-constraint is created. The problem is that the domain and body of the Pi are in different contexts. The constrain generated before this commit was incorrect, it could contain a free variable. This commit fix the issue by using the context of the body, and lifting the free variables in the domain by 1.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit improves the condition for showing that an equality(and convertability) constraint cannot be solved. A nice consequence is that Lean produces nicer error messages. For example, the error message for unit test elab1.lean is more informative.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
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>
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>
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>
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>
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>
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>
Recursive functions that may go very deep should invoke the function check_stack. It throws an exception if the amount of stack space is limited.
The function check_system() is syntax sugar for
check_interrupted();
check_stack();
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
