perf: PR for radar testing of Fsub

[chenson2018]

Please do not review yet, this PR is for initial benchmarking of inlining grind annotations.

[chenson2018]

!radar

[leanprover-radar]

Benchmark results for 4bde46f against 02e2a23 are in! @chenson2018

Warning

These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.

• Bench repo commit hashes for run main differ between commits.

Large changes (1✅)

• ✅ build/module/Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Typing//instructions: -12.7G (-7.3%)

Medium changes (1✅)

• ✅ build/module/Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Safety//instructions: -22.5G (-33.6%)

Small changes (1🟥)

• 🟥 build/module/Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.WellFormed//instructions: +12.7G (+11.3%)

[chenson2018]

!radar

[leanprover-radar]

Benchmark results for b6c5720 against 02e2a23 are in! @chenson2018

Warning

These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.

• Bench repo commit hashes for run main differ between commits.

Large changes (1✅)

• ✅ build/module/Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Typing//instructions: -11.7G (-6.7%)

Medium changes (1✅)

• ✅ build/module/Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Safety//instructions: -22.5G (-33.6%)

[chenson2018]

!radar

[leanprover-radar]

Benchmark results for dee05e5 against 02e2a23 are in! @chenson2018

Warning

These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.

• Bench repo commit hashes for run main differ between commits.

Large changes (1✅)

• ✅ build/module/Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Typing//instructions: -13.3G (-7.6%)

Medium changes (1✅)

• ✅ build/module/Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Safety//instructions: -22.6G (-33.6%)

Small changes (1✅)

• ✅ build/module/Cslib.Languages.LambdaCalculus.LocallyNameless.Fsub.Subtype//instructions: -13.9G (-12.7%)

[chenson2018]

I think this at least identifies some of the problem areas. I'd still like to see if a pattern can guard against these instead of having to always specify them by hand.