perf: fix implementation of move constructors and move assignment ope…

[legrosbuffle]

…rators

Right now those constructors result in a copy instead of the desired move. We've measured that expr copying and assignment by itself uses around 10% of total runtime on our workloads.

See #4698 for details.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries CI can not be attempted yet, as the nightly-testing-2024-07-09 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. (2024-07-09 13:02:53)
• 💥 Mathlib branch lean-pr-testing-4700 build failed against this PR. (2024-07-10 01:14:57) View Log
• ✅ Mathlib branch lean-pr-testing-4700 has successfully built against this PR. (2024-07-10 16:12:49) View Log

[leanprover-bot]

Here are the benchmark results for commit c3c46b2.
There were significant changes against commit 582d6e7:

  Benchmark     Metric             Change
  ==================================================
+ reduceMatch   instructions        -1.4% (-352.1 σ)
+ stdlib        tactic execution    -1.4% (-342.6 σ)

[kim-em]

Mathlib benchmark is hopefully running now at leanprover-community/mathlib4#14599.

[kim-em]

Mathlib benchmark is hopefully running now at leanprover-community/mathlib4#14599.

No significant changes in Mathlib build time. (This is, of course, not intended to be a representative benchmark!)

[Kha]

@legrosbuffle I assume the time savings happen in kernel type checking in your case? While lean4 and mathlib4 are not bottlenecked by the kernel at the moment, we are still interested in optimizing it. Do you think you could extract a representative stand-alone test case for the bottleneck and speedup?

[legrosbuffle]

@legrosbuffle I assume the time savings happen in kernel type checking in your case?

Yes, the majority of the cost if from src/kernel/replace_fn.cpp.

While lean4 and mathlib4 are not bottlenecked by the kernel at the moment, we are still interested in optimizing it. Do you think you could extract a representative stand-alone test case for the bottleneck and speedup?

It's not obvious that this is easy to reduce, but I'll see what I can do.