Aesop.buildGlobalRule now needs goal : MVarId

Stream: metaprogramming / tactics

[Geoffrey Irving]

Aesop.buildGlobalRule now needs a Context since it runs inside Aesop.ElabM. The Context hasgoal : MVarId. I was calling buildGlobalRule in an attribute handler to make global rules, and thus not inside a proof where there are goals. Is there an appropriate fake goal to use?

[Geoffrey Irving]

If buildGlobalRule fundamentally needs the goal, what does it do with it?

[Geoffrey Irving]

The code I have to update: https://github.com/leanprover-community/mathlib4/pull/10562/files#diff-c70f7019794a20f5fc3a6bae8b84b29c08832b54b3de126ef0ee5e5a43ad2b02R90

[Jannis Limperg]

Sorry about that; it's a hack to work around some limitations of the Lean API. You can use ElabM.Context.forAdditionalGlobalRules like here.