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 field was originally added to create hashtables based on pointer
equality. We don't use them anymore, and the caches based on
m_hash_alloc can be implemented using m_hash without any performance
impact. This commit also fixes two places where `expr_set` was used
instead of `expr_struct_set`.
This commit is also important for the Lean4 plans where `expr` will
be implemented in Lean, and fields like `m_hash_alloc` would require us
to track state.
@nunoplopes @aqjune
I had to add a new primitive to allow you to execute a tactic from the
`main` function. The `main` function is in the `io` monad. The new
primitive has type:
```
meta constant io.run_tactic {α : Type} (a : tactic α) : io α
```
I also added a new test that shows how to use it.
The test displays all declarations that have the `nat` prefix.
cc @kha
The tactic_state object will contain a name_generator for creating fresh
names. `tactic_state.mk_empty` is bad because it does not have sufficient
information to create this name_generator.
Moreover `tactic_state.mk_empty` was only being used to convert
`tactic A` into a `parser A`.
We implement this primitive now in C++. In C++, we will be able
to use the parser name generator to initialize a fresh `tactic_state`.
