feat(library/kernel_serializer): add serializer/deserializer for inductive decls

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/module): add inductive decls to .olean files

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/kernel_bindings): use standard environment in import_modules

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
test(lua): add inductive decl serialization test

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
doc(lua): update Lua API documentation, and reactivate doc tests

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
perf(library/shared_environment): replace shared_mutex with simple mutex, the shared_mutex is just overhead and impacts negatively on performance tests

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(build): add GPROF compilation mode for using gprof

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
test(lua): move slow tests to tests/lua/slow

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(*): tag 'slow' tests as 'expensive', and exclude 'expensive' tests when testing under valgrind

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
perf(kernel/environment): improve is_descendant performance, optimize for the common case: the is_descendant tree is huge but has few deep branches

This is an important optimization for module.cpp. The benchmark tests/lua/slow/mod2.lua is a good example where the cost of is_descendant was neutralizing the benefit of the replace method.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
perf(kernel/type_checker): reduce the overhead of creating delayed_justification objects, a huge number of them is created when type checking applications

We reduce the cost by avoiding the allocation of std::functional objects, and the unnecessary increment/decrement of reference counters.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
perf(library/module): do not use multiple threads when skipping type checking, add flag to disable/enable type checking theorems asynchronously

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/modules): add option for discarding the proof of imported theorems (after checking them)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/kernel_bindings): used 'named' parameters in import_modules API

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(util/name): add optional<name> helper functions for implementing Lua API

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/expr_lt): add expr_quick_cmp functional object

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/kernel_bindings): add to_io_state_ext helper function

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(library): add module namespace

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library): add support for creating 'private/hidden' names

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
test(lua): add is_sorted inductive predicate example

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