leanprover
perf: `infer_app` with `infer_only := false` (WIP)
Here are the benchmark results for commit d1dd4b911b3a34645d823a6d3bfefa0e15eb83e3. There were significant changes against commit f76a17b33f85d714ea33d37e8975a02382abb28c:
Benchmark Metric Change
====================================================
+ tests/bench/ interpreted maxrss -1.1% (-11.5 σ)
- 💥 Mathlib branch lean-pr-testing-2781 build failed against this PR. (2023-10-29 04:31:34) View Log
- ✅ Mathlib branch lean-pr-testing-2781 has successfully built against this PR. (2023-10-29 10:49:22) View Log
- 🟡 Mathlib branch lean-pr-testing-2781 build this PR didn't complete normally. (2023-10-29 22:44:18) View Log
- ✅ Mathlib branch lean-pr-testing-2781 has successfully built against this PR. (2023-10-30 00:00:48) View Log
@leodemoura here is the comparison between Mathlib runs: http://speed.lean-fro.org/mathlib4/compare/e7b27246-a3e6-496a-b552-ff4b45c7236e/to/e7b27246-a3e6-496a-b552-ff4b45c7236e?hash1=1ca67b1a4b326c4224bb25a792b22c304c83b597&hash2=bb1b2648e3674b537c07efac0d4e66162fb7dab5
Unfortunately it doesn't look good: a 2.4% wallclock regression.
Unfortunately it doesn't look good: a 2.4% wallclock regression.
I took a look at the results. This commit affects "type checking" time, and it seems it went down.
This commit minimizes the number of instantiate operations, but it is not caching the type for partial applications. That is, if we have f a b and f a c. The previous approach caches the result for f a, but this commit skips it. That being said, it seems "type checking" time still went down. It is unclear to me how the "wall clock" time went up.
Either of these might or might not be noise, the instruction count suggests that there is probably no impact overall. We should try again on top of https://github.com/leanprover-community/mathlib4/pull/8224
