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
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.
@kha This commit is retracting the experiment using
`mk_fresh_name_generator_child` when creating new tasks.
The names get too long.
I'm still refactoring the code and trying to eliminate all occurrences
of `mk_fresh_name`. I still have a long way to go, but I am merging
this branch into master since it has many other fixes.
closes#1814
@kenmcmil: the error messages will now list aliased variables.
For example, in your file, the new error message is:
```
invalid type ascription, term has type
triple (ctxpre c' s_1 ∧ ctxpre c'_1 s_1) (bndngapp b s_1) (ctxpost c' s_1 ∧ ctxpost c'_1 s_1)
but is expected to have type
triple (ctxpre c' s_1 ∧ ctxpre c'_1 s_1) (bndngapp b s_1) (ctxpost c' s_1 ∧ ctxpost c'_1 s_1)
types contain aliased name(s): c'
remark: the tactic `dedup` can be used to rename aliases
state:
...
```
As described at issue #1760, the new error message is:
```
1760.lean:6:18: error: type mismatch at application
f x
term
x
has type
big_type : Type 1
but is expected to have type
?m_1 : Type
```
We need this feature for:
1) Defining nonlinear search patterns. Example: (?m <= ?m + 1)
2) Preprocessing recursive equations and support the pattern
refinement approach used in Agda. Example: in Agda, they accept
```
def append {A : Type} : Π (m n : nat), Vec A m -> Vec A n -> Vec A (m + n)
| m n nil ys := ys
| m n (cons m' x xs) ys := cons x (append m' n xs ys)
```
These equations have to be refined. For example, `m` has to be
replaced with `0` (in the first equation), and `succ m'` in the
second. To implement this kind of refinement, we need to convert
the pattern variables (local constants) into metavariables during
elaboration. Then, the unassigned metavariables become local constants
again. This preprocessing step will fix some of the issues on #1594.
To completely fix#1594, we will need yet another preprocessing step
which will implement "complete transition" used in the equation
compiler before we start elim_match.cpp
The kernel support opportunistic hash consing.
At commit e63c79c81e we have enabled this feature during
tactic execution, and fixed performance problems in the Certigrad
project (by @dselsam).
However, this change produced unexpected performance problems in
other Lean files (example: @JasonGross example at issue #1646 was 10x
slower after the commit above).
After analyzing the performance logs, I conjecture the hash_consing
may produce a substantial performance overhead if the following property
doesn't hold.
- Let `cache` be the hash_consing cache, then for each `e` in `cache`,
all children of `e` are also in the `cache`.
If the property above is not true, we may have problem whenever
we add an expression `t` containing multiple copies of a big term `T`.
For example, support we insert `f T_1 T_2`, where `T_1` and `T_2` are
structurally equal but are not pointer equal. Then, if we try to insert
`f T_2 T_1`, we will have to compare the huge terms twice, and the
comparison will be proportional to the size of `T_i`.
This commit tries to address this performance problem by enforcing
the property above. This is not a perfect solution since we may keep
trying to create terms using big terms created before hash_consing
has been enabled. After this commit, the example at issue #1646
is only 1.4x slower. It didn't impact the standard library
compilation (memory nor time).
I'm using this commit is a temporary workaround. We should probably
remove the hash_consing support from the kernel, and implement it
in key places. For example, for Certigrad, we can control memory
consumption by using hash_consing only during `simp`,
`instantiate_mvars` and `elaborator` finalization procedure.
@gebner @kha Any ideas/suggestions for this hash_consing issue?
