It is currently implemented in C++. The plan is to move the procedures
for inserting inc/dec, reset/reuse, and inferring borrow inferences to
Lean. Another goal is to make sure new IR optimizations can be
implemented in Lean, and to avoid backend optimizations that would
have to be duplicated in each backend (e.g., `emit_proj_inc_reset_seq`
at `emit_cpp.cpp`).
cc @kha
@kha
I am using this little program to generate big lean files to test the
new front end. For the output produced for `gen 5000`, the new frontend
is almost 10x slower than the old one.
I used `valgrind --tool=callgrind` to collect profiling data.
The number of closures is too big. For example, `free_closure_obj` was
invoked 38.5 million times. The total number of deallocated objects is around
49.5 million.
We use the same trick in the C++ version of this function.
I measured the impact using `lean --new-frontend core.lean` and checking
the number of instructions executed reported by Valgrind.
Before: 4,891,642,264
After: 4,847,313,330
The "quick" filter `&s1 != &s2` was incorrect.
It was actually always false, since it just comparing the stack address
of `s1` and `s2`.
I incorporated the quick filter into `string_eq`.
I measured the impact using `lean --new-frontend core.lean` and checking
the number of instructions executed reported by Valgrind.
Before: 5,210,225,530
After: 4,891,642,264
@kha
@kha I have disabled this check. It was implemented 2 years ago by
Daniel, and I don't want to fix it. It seems you have already fixed a
bug there. AFAICT, this check is just for improving error messages.
I believe we may not even need it since the kernel now supports nested
inductive types. AFAIR, Daniel implemented this check here because the
inductive compiler was introducing a lot of auxiliary declarations
that were making the kernel error messages unreadable.
@kha I tried to make the examples self contained.
- unionfind1.lean uses the modified StateT and ExceptT
- unionfind2.lean uses the standard StateT and ExceptT
