When to [always_inline]?

Stream: lean4

[François G. Dorais]

I've been trying to figure out the difference between [inline] and [always_inline] but didn't find anything super useful. I'm especially puzzled by the fact that they are often used together!?

[Mario Carneiro]

this is a workaround for the fact that there are two lean compilers

[Henrik Böving]

I cannot speak for the old code generator, in the new code generator there is afaik no difference between the two right now but there is a TODO to limit the inlining of inline tagged declarations to a certain quota in the future. always_inline on the other hand does as you would expect force the new code generator to always perform inlining.

[Henrik Böving]

The old code generator does not seem to react to always_inline so that is the reason you are seeing declarations with both inline and always_inline.

[Mario Carneiro]

the old code generator does not recognize the [always_inline] attribute, while the new one needs it

[François G. Dorais]

That is enlightening! To summarize: [inline] is fine unless you realize you also need to [always_inline] when using the new code generator?

[François G. Dorais]

Aside: does abbrev always inline?

[Mario Carneiro]

I believe so

[Mario Carneiro]

it's marked as @[inline] (not @[always_inline]) automatically

[François G. Dorais]

So @[always_inline] abbrev ... could make sense?

[Mario Carneiro]

I think so

[Mario Carneiro]

@[always_inline] is normally only used on instances

[François G. Dorais]

Thanks! This was very helpful!