Zulip Chat Archive

Stream: mathlib4

Topic: elaborate context in attributes


Floris van Doorn (Oct 13 2022 at 19:02):

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 (Oct 13 2022 at 19:03):

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

Mario Carneiro (Oct 13 2022 at 19:34):

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 (Oct 13 2022 at 19:35):

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

Mario Carneiro (Oct 13 2022 at 19:40):

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 (Oct 13 2022 at 20:27):

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 (Oct 13 2022 at 20:30):

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 (Oct 13 2022 at 20:31):

Ah, it's a TSyntax "type error"

Floris van Doorn (Oct 13 2022 at 20:31):

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

Mario Carneiro (Oct 13 2022 at 20:31):

elabSyntaxConfig takes an optConfig directly

Mario Carneiro (Oct 13 2022 at 20:36):

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

Floris van Doorn (Oct 13 2022 at 20:39):

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 (Oct 13 2022 at 21:01):

not that I know of

Mario Carneiro (Oct 13 2022 at 21:01):

indeed it does

Mario Carneiro (Oct 13 2022 at 21:02):

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


Last updated: Dec 20 2023 at 11:08 UTC