perf: do not inline constant syntax node kinds

[tydeu]

A quick test of my observation in #2425 (comment).

[tydeu]

!bench

[tydeu]

@Kha To verify, benching before the CI builds is fine? Or will that break the benchmark?

[Kha]

That's fine, they are independent. Having the runner waste time on a commit not known to compile is not fine but I guess that doesn't apply here.

[leanprover-bot]

Here are the benchmark results for commit aae92e5.
There were significant changes against commit f1412dd:

  Benchmark   Metric             Change
  ==============================================
- stdlib      tactic execution     1.1% (12.0 σ)

[tydeu]

In the full results, it did decrease the number of C lines by 2,398, but that metric does not appear to be part of significant changes because it lacks a stddev, It appears to have had a large effect stdlib instruction count (-1,253,594,950.5), which I am not sure why that was not considered significant (maybe because the stddev % is 0 and that throwing off some calculations?) Regardless, I think this change may be too small to have significant effect on anything else in the manner I hoped. I do wonder why there was a significant decrease in the tactic execution time though.

[tydeu]

@Kha Do you know what the significance threshold is for stdlib instructions/branches because the full results of the benchmark seem to suggest those should be significant but they do not appear as part of the significant changes. Is it because the Stddev % of both is 0?

[Kha]

It's complicated:

##
## A commit becomes significant if the following rules hold for at least one of its measurements and
## the corresponding measurement in the run of any parent commit:
##
## Rule 1: |(newValue - oldValue) / oldValue| >= significanceRelativeThreshold
## Rule 2: |newValue - oldValue| >= significanceStddevThreshold * stddev(newValues)
##
## If the amount of new values is below significanceMinStddevAmount, rule 2 doesn't apply.
##
significanceRelativeThreshold: 0.01
significanceStddevThreshold: 10
significanceMinStddevAmount: 2

[tydeu]

@Kha It certainly seems like the decrease in instructions should be significant. It is about a ~114 stddevs decrease. It also seems to pass both rules:

Rule 1: 0.032 >= 0.01
Rule 2: 1,253,594,950.5 >= 10*11,254,866.608

[Kha]

No, it's a decrease by 0.032%. The threshold is 1%.

[tydeu]

@Kha Ah, that the threshold was a raw fraction, not a percent. Makes sense. That does seem like a nigh impossible goal though for instructions/branches considering their magnitude. Especially for smaller changes that only affect some localized part of the library.

[tydeu]

!bench

[leanprover-bot]

Here are the benchmark results for commit 028bf8d.
There were no significant changes against commit f1412dd.

[tydeu]

To summarize the results here. @[noinline] is bad here presumably because it also causes the C code not to inline the definitions when it can, which is undesirable. However, @[inline] (which is implied by abbrev) is bad because it will inline the constants into the call sites which will result in them being extracted as duplicate closed term constants. Thus, a plain def is the best as it will not inline in Lean but will inline in C.

[leodemoura]

@tydeu The benchmarking results above suggest this change makes no (or very little) difference.

[tydeu]

@leodemoura Yeah, the change is small enough (i.e., effects not enough downstream code) that the stdlib code size decreases it produces are not enough to be significant. For example, while it does have 1.3 million / 59.3 stddev decrease in stdlib instructions, that is only a 0.035% decrease overall. This change would likely need to be combined with some other small, localized code size improvements to create a significant change.

[tydeu]

!bench

[leanprover-bot]

Here are the benchmark results for commit 49a1993.
There were no significant changes against commit f1412dd.

[tydeu]

Closing this since the effect is too small to be significant for now.