elaborate context in attributes

Stream: mathlib4

[Floris van Doorn]

The @[simps] attribute has configuration options. I saw that there is a declare_config_elab command to automatically define a functions that elaborates configuration options. However, this lives in TermElabM, but the code that is executed when executing attributes is in AttrM (= CoreM).
I tried to use this in @[simps] in a very naive way, but (probably unsurprisingly) that doesn't work:

declare_config_elab elabSimpsConfig Simps.Config
[...]
initialize simpsAttr : ParametricAttribute (Array Name) ←
  registerParametricAttribute {
    getParam := fun
    | nm, stx@`(attr|simps $[?%$trc]? $[(config := $c)]? $[$ids]*) => do
      let cfg ← match c with
        | none => pure {}
        | some c => MetaM.run' <| TermElabM.run' <| elabSimpsConfig c
[...]

What is the right way to do this?
Relevant PR: mathlib4#445

[Floris van Doorn]

Btw: @[simps] passes most tests that do not have configuration options.

[Mario Carneiro]

I recently had cause to run a (fairly elaborate) TermElabM inside AttrM for the norm_num attribute. Perhaps it can give you some ideas

[Mario Carneiro]

https://github.com/leanprover-community/mathlib4/blob/2df4e5015eafec1e9d3ca5516a7d6e4f9286e26d/Mathlib/Tactic/NormNum/Core.lean#L156-L162

[Mario Carneiro]

That said I think what you wrote should more or less work; the only part that is going to cause problems if you forget it is withSaveInfoContext, which will make stuff like term goals show up inside the span of the config

[Floris van Doorn]

Whenever I add a configuration option to @[simps] (e.g. @[simps (config := {fullyApplied := false})]) I get the errors

declaration uses 'sorry'

cannot evaluate code because 'sorryAx' uses 'sorry' and/or contains errors

Any ideas what causes this? The errors are in test/Simps of mathlib4#445.

[Floris van Doorn]

It's hard to compare your code to mine, since I don't know what parts are already handled by declare_config_elab.

[Mario Carneiro]

Ah, it's a TSyntax "type error"

[Floris van Doorn]

Oh, maybe the problem is that elabSimpConfigCore expects an optional configuration...

[Mario Carneiro]

elabSyntaxConfig takes an optConfig directly

[Mario Carneiro]

syntax simpsArgsRest := (Tactic.config)? (ppSpace ident)*
...
      let cfg ← MetaM.run' <| TermElabM.run' <| elabSimpsConfig stx[2][0]

[Floris van Doorn]

Ok, that works! Thanks!
Is there a way to give the stx[2][0] a name in `(attr|simps $[?%$trc]? $[(config := $c)]? $[$ids]*)?
Does it correspond to the whole $[(config := $c)]??

[Mario Carneiro]

not that I know of

[Mario Carneiro]

indeed it does

[Mario Carneiro]

you could construct a config syntax from c but that seems wasteful