test: robin's Level.isEquiv

[arthur-adjedj]

This PR tests @Rob23oba 's Level.isEquiv algorithm, purposefully doesn't use the old isEquiv first to check for perf changes

[arthur-adjedj]

!bench

[arthur-adjedj]

downstream

[leanprover-radar]

Benchmark results for a54dcb9 against e12fac8 are in. There are significant results. @arthur-adjedj

• 🟥 build//instructions: +12.6G (+0.12%)

Medium changes (5🟥)

• 🟥 build/stat/imported bytes//bytes: +2GiB (+1.13%)
• 🟥 build/stat/imported consts//amount: +1.1M (+1.33%)
• 🟥 build/stat/imported modules//amount: +18.1k (+1.02%)
• 🟥 elab/charactersIn//instructions: +48.8M (+0.16%)
• 🟥 elab/workspaceSymbols//instructions: +33.5M (+0.17%)

Small changes (34✅, 758🟥)

• 🟥 build/lakeprof/longest rebuild path//instructions: +6.5G (+1.12%)
• ✅ build/module/Init.Data.List.Nat.Modify//instructions: -8.0M (-0.14%)
• 🟥 build/module/Lake.Build.Actions//instructions: +6.1M (+0.23%)
• 🟥 build/module/Lake.Build.Context//instructions: +6.3M (+0.60%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lake.Build.Executable//instructions: +5.9M (+0.53%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lake.Build.ExternLib//instructions: +5.7M (+0.29%)
• 🟥 build/module/Lake.Build.Fetch//instructions: +6.4M (+0.59%) (reduced significance based on absolute threshold)
• ✅ build/module/Lake.Build.Index//instructions: -11.2M (-0.61%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lake.Build.Info//instructions: +6.2M (+0.71%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lake.Build.Infos//instructions: +6.1M (+0.18%)
• ✅ build/module/Lake.Build.InitFacets//instructions: -10.3M (-1.43%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lake.Build.InputFile//instructions: +5.9M (+0.58%)
• 🟥 build/module/Lake.Build.Job.Basic//instructions: +6.3M (+0.41%)
• 🟥 build/module/Lake.Build.Job.Register//instructions: +5.9M (+0.39%)
• 🟥 build/module/Lake.Build.Job//instructions: +6.6M (+1.01%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lake.Build.Store//instructions: +6.3M (+0.55%)
• 🟥 build/module/Lake.Build.Target//instructions: +6.5M (+0.99%) (reduced significance based on absolute threshold)
• ✅ build/module/Lake.Build.Targets//instructions: -11.5M (-0.34%)
• 🟥 build/module/Lake.Build//instructions: +6.4M (+0.96%) (reduced significance based on absolute threshold)
• 🟥 build/module/Lake.CLI.Actions//instructions: +6.4M (+0.39%)
• and 772 more

[downstream-lean4]

The adaptation PR for this PR is leanprover/downstream-lean4#83.