elab_strategy

Stream: mathlib4

[Patrick Massot]

Is there a Lean 4 analog of the elab_strategy attribute? What should we do of it while porting?

[Henrik Böving]

I don't exactly know what it does but purely based on naming it sounds like elab_as_elim might be?

[Eric Wieser]

I don't think elab_strategy is ever supposed to be used, the docstring is "internal attribute for the elaborator strategy for a given constant"

[Eric Wieser]

I think it's a bit like the _simp_cache attribute; it's added by other attributes to help out metaprograms, but not intended to be applied by the user.

[Eric Wieser]

Why not backport removing the attribute and see if anything breaks?

[Patrick Massot]

There are exactly two uses of elab_strategy in mathlib, in data/fin/basic. Removing that attribute does break statements in the same file.

[Eric Wieser]

Maybe @[elab_as_eliminator, elab_strategy] means "attach the elab_as_eliminator attribute but overwrite the implementation details with the default strategy"?

[Eric Wieser]

Debugging with #print, it seems that @[elab_as_eliminator, elab_strategy] means the same as @[elab_strategy] which means @[elab_simple]

[Eric Wieser]

@Chris Hughes, do you remember why you wrote this?

[Patrick Massot]

I just sent #18049 and #18050 to CI. Let's see if one of them builds.

[Chris Hughes]

I think it was to do with Jordan Holder but I might not habe used it in the end

[Patrick Massot]

Both PRs passed CI. Eric expressed a preference for #18049 and delegated so I'll merge this tonight if nobody complains in the next couple of hours.

[Johan Commelin]

@Patrick Massot I see no harm in merging right now.