fix: take `synthPendingDepth` into account when caching TC results

leanprover / lean4

Lean 4 programming language and theorem prover

https://lean-lang.org

Apache License 2.0

3.88k stars 329 forks source link

fix: take `synthPendingDepth` into account when caching TC results #4120

Closed leodemoura closed 2 weeks ago

leodemoura commented 3 weeks ago

@semorrison This is for debugging purposes only. It contains only the TC cache fix. If #4119 does not fix the performance issues in Mathlib. We can use this one to check whether the issue is due to this commit or not.

leanprover-community-mathlib4-bot commented 3 weeks ago

Mathlib CI status (docs):

💥 Mathlib branch lean-pr-testing-4120 build failed against this PR. (2024-05-10 01:25:46) View Log
💥 Mathlib branch lean-pr-testing-4120 build failed against this PR. (2024-05-10 02:14:10) View Log

semorrison commented 2 weeks ago

Closing in favour of #4119.