Next steps:
- Implement more validators (e.g., blockid validator, type checker).
- Implement C++ code generator (in Lean). We can use it for testing the new
lean_obj module implemented in C++.
- Implement interpreter (in C++) for sanity checking.
- Implement LLVM IR generator (in Lean). It just outputs a text file using LLVM
syntax. After, we are confident we are generating valid LLVM IR, we
can try to link LLVM with Lean.
Remark: the non monadic versions are called list.all and list.any.
We did not use `list.mall` and `list.many` since `mall` and `many` are
existing words.
Before this commit, the unifier would try to solve the unification consraint
?m =?= fun x_1 ... x_n, ?m x_1 ... x_n
by assigning
?m := fun x_1 ... x_n, ?m x_1 ... x_n
which fails the occurs check.
This commit skips the assignment by using eta-reduction.
The new lean_obj objects will be defined at util.
Reason: we will define `name`, `options`, `format`, ... on top of lean_obj.
lean_obj depends on mpz.
Remark: lean_obj will replace vm_obj.
numeric_traits is dead code. It was used to implement a simplex that was
parametric on the number type. This code has been moved to Z3.
So, we don't need it anymore.
It just adds extra complexity and is in conflict for our plans for
Lean4. Moreover, in our experiments it impacts negatively on
performance: master and lean4 branches. The negative impact has been
confirmed by @kha too.
memory_pool object introduces memory contention and unnecessary
complexity. Moreover, it actually reduces performance when we compile
Lean using JEMALLOC.
Here are the numbers for corelib
jemalloc with memory_pool: 13.83 secs
jemalloc without memory_pool: 13.60 secs
We use small_object_allocator to allocate vm_obj's.
However small_object_allocator is not thread safe. So, we need to copy
vm_obj's between threads. Moreover, in our experiments, we observed that
JEMALLOC is actually faster than the small_object_allocator.
Here are numbers for the reduced corelib.
small_object_allocator: 15.62 secs
gcc 4.9 allocator: 16.19 secs
jemalloc: 13.83 secs
This abstraction was added when we started Lean.
We wanted to focus on nonlinear arithmetic and support dReal.
The zpz module was going to be used to implement polynomial
factorization procedures similar to the ones in Z3 and computer algebra
systems.
This is not a goal for the Lean project anymore.
These two abstractions were added when we planned to have an efficient
Simplex module, written in C++, in Lean. We have moved this module to
Z3. So, we don't need these abstractions anymore.
Binary rationals were added when we started the Lean project.
We wanted to use them to implement an algebraic number module similar to the
one we implemented in Z3.
If one day we implement algebraic numbers in Lean, we will do it in Lean
instead of C++.
All theorems are proved without using the tactic framework.
Thus, we can define `fin/uint32/uint64` types and their operations
before we define the tactic framework.
