feat: simp local confluence testing

[kim-em]

This adds @nomeata's simp local confluence testing tool in tests/simplc, and sets up whitelists to run this on the core Lean library.

The README contains instructions for running this is in downstream repositories.

I have not yet hooked this up to CI.

[tobiasgrosser]

This is exciting. Thank you @kim-em and @nomeata for this useful tool. I am happy to help further polishing the BitVec library with respect to confluence.

[tobiasgrosser]

Suggested change

	logInfo m!"Checking {thms.size} simp lemmas for critical pairs"
	let filtered_sthms := thms.foldl Lean.Meta.addSimpTheoremEntry (init := {})
	logInfo m!"Checking {thms.size} simp lemmas for critical pairs"
	let filtered_sthms := thms.foldl Lean.Meta.addSimpTheoremEntry (init := {})

Should this logInfo become a trace option?

[nomeata]

Maybe, I'll leave this to Kim who has the most experience actually using the tool.

In general I think there is a need for information from tactics/command that you can easily get, but doesn't show up in All Messages nor the build log. Maybe a custom hover. Until then a trace works.

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-5717 has successfully built against this PR. (2024-10-15 09:49:23) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5c70e5d8459ae445c237d85893e2e7280e226533 --onto 38c39482f40536b864a9b43c718e10e8413b26e5. (2024-10-31 01:51:30)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 465ed8af46e6a4491f9c81dd6d77ae37da11fd68 --onto 0fcee100e7ea382069854d91e854265c56b54428. (2024-11-01 02:39:53)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1659f3bfe26545f77fe4ea84f61ce5e441dea87d --onto 0de925eafcfcff0f2c86e036f91bb451136b04c4. (2024-11-04 00:05:03)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a4d521cf96d4994640c42d96b693c2d789016f5f --onto c779f3a039963fd38b03a78f635f0a7c36f24f42. (2024-11-05 02:45:38)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 8e2f92607fd20fc12b492504c4034e007ca3d927 --onto c779f3a039963fd38b03a78f635f0a7c36f24f42. (2024-11-05 10:52:35)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 4df71ed24f4be25ba0045b4963a03087d2302fa9 --onto c779f3a039963fd38b03a78f635f0a7c36f24f42. (2024-11-06 05:30:48)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 14c3d4b1a6cd6b9a755c952a2fa8f4c205c4b3e4 --onto c779f3a039963fd38b03a78f635f0a7c36f24f42. (2024-11-06 10:13:13)