perf: globally cache intermediate type class results

[JovanGerb]

See Zulip discussion here

This is a PR to determine whether this idea indeed results in faster type class search.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a17c3f424cb5f2390e645d8a2cf84e69a1b96a37 --onto 7db8e6482e1dc46fd1070b3bf549112f02a4c05e. (2024-05-13 16:25:08)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f3538dbdfa5595e361141986fc35daf23e225832 --onto 91244b2dd9d223006227648659203373f5a46b0b. (2024-05-14 22:02:27)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f3538dbdfa5595e361141986fc35daf23e225832 --onto 3035d2f8f689b52963f49b2414414913ca296953. (2024-05-15 11:47:15)
• 💥 Mathlib branch lean-pr-testing-4152 build failed against this PR. (2024-05-16 01:18:24) View Log
• 💥 Mathlib branch lean-pr-testing-4152 build failed against this PR. (2024-05-17 03:36:36) View Log
• ❌ Mathlib branch lean-pr-testing-4152 built against this PR, but testing failed. (2024-05-21 03:28:12) View Log
• ❌ Mathlib branch lean-pr-testing-4152 built against this PR, but testing failed. (2024-05-21 16:22:50) View Log
• 💥 Mathlib branch lean-pr-testing-4152 build failed against this PR. (2024-05-21 22:46:48) View Log
• 💥 Mathlib branch lean-pr-testing-4152 build failed against this PR. (2024-05-22 00:35:13) View Log
• ❌ Mathlib branch lean-pr-testing-4152 built against this PR, but testing failed. (2024-05-22 03:22:06) View Log
• ❌ Mathlib branch lean-pr-testing-4152 built against this PR, but testing failed. (2024-05-22 13:33:04) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f97a7d4234bd76bc0f61e43b8c6a78117c1376df --onto ff37e5d512efcd3981290270a2fc3ecb100bbd0c. (2024-05-22 19:51:59)
• 🟡 Mathlib branch lean-pr-testing-4152 build this PR didn't complete normally. (2024-05-22 20:27:40) View Log
• 💥 Mathlib branch lean-pr-testing-4152 build failed against this PR. (2024-05-23 17:33:01) View Log
• 💥 Mathlib branch lean-pr-testing-4152 build failed against this PR. (2024-05-23 18:38:54) View Log

[JovanGerb]

Can anyone explain why the output on two of the tests doesn't match the expectation? These tests have nothing to do with type classes...

[nomeata]

For the reader’s convenience, the errors are

[00:11 (00.000835)] lean-test-stage1> --- 1616.lean.expected.out    1970-01-01 00:00:01.000000000 +0000
[00:11 (00.000537)] lean-test-stage1> +++ 1616.lean.produced.out    2024-05-13 16:12:18.608808504 +0000
[00:11 (00.000532)] lean-test-stage1> @@ -2,6 +2,16 @@
[00:11 (00.000473)] lean-test-stage1>    @Linear ?m ?m (?m :: ?m) (?m :: ?m) c.right
[00:11 (00.004419)] lean-test-stage1>  context:
[00:11 (00.000027)] lean-test-stage1>  c : Cover ?m ?m ?m
[00:11 (00.000011)] lean-test-stage1> +⊢ List ?m
…

and

 [00:46 (00.000798)] lean-test-stage1> --- omega-failure.lean.expected.out   1970-01-01 00:00:01.000000000 +0000
[00:46 (00.000555)] lean-test-stage1> +++ omega-failure.lean.produced.out   2024-05-13 16:12:52.997271237 +0000
[00:46 (00.000522)] lean-test-stage1> @@ -57,8 +57,8 @@
[00:46 (00.000507)] lean-test-stage1>    d_1 ≥ 0
[00:46 (00.000434)] lean-test-stage1>    u ≥ 0
[00:46 (00.000424)] lean-test-stage1>    t ≥ 0
[00:46 (00.000669)] lean-test-stage1> -  w ≥ 0
[00:46 (00.000428)] lean-test-stage1>    q + r + s + t + u + v + w + x + y + z + a_1 + b_1 + c_1 + d_1 + e_1 ≥ 100
[00:46 (00.000516)] lean-test-stage1> +  w ≥ 0
[00:46 (00.000425)] lean-test-stage1>    r ≥ 0
[00:46 (00.000420)] lean-test-stage1>    y ≥ 0

No idea, though :-)