multiple environment changing attributes

Stream: mathlib4

[Floris van Doorn]

When writing

@[to_additive, simps] def foo := ...

It seems that@[simps] doesn't get the environment after @[to_additive] has finished running.
@[to_additive] runs modifyEnv (ToAdditive.translations.addEntry · (src, tgt)), but if @[simps] then runs (ToAdditive.translations.getState env).find? src it will return none.
It does work as expected when writing

@[to_additive] def foo := ...
attribute [simps] foo

Is there a way for @[to_additive, simps] to do the same?

[Floris van Doorn]

I can post a MWE if desired.

[Scott Morrison]

Presumably this will need a fix to Lean 4, for which a MWE will be helpful.

[Gabriel Ebner]

Does it work the other way around with @[simps, to_additive]?

[Floris van Doorn]

Oh, I think I found the culprit:

initialize registerBuiltinAttribute {
    name := `to_additive
    [...]
    -- Because `@[simp]` runs after compilation,
    -- we have to as well to be able to copy attributes correctly.
    applicationTime := .afterCompilation
  }

[Floris van Doorn]

It still doesn't work if I put applicationTime := .afterCompilation also in simpsAttr. Is it possible that ParametricAttribute is added before BuiltinAttribute? Should be make to_additive not a BuiltinAttribute?

[Floris van Doorn]

MWE:

-- Mathlib.test
import Std.Lean.NameMapAttribute
import Lean.Elab.Exception

open Lean Meta Elab

initialize dict : NameMapExtension Name ← registerNameMapExtension _

syntax (name := attr1) "attr1" : attr
syntax (name := attr2) "attr2" : attr

initialize registerBuiltinAttribute {
    name := `attr1
    descr := ""
    add := fun src stx _ => match stx with
      | `(attr| attr1) => modifyEnv (dict.addEntry · (src, `foo))
      | _ => throwUnsupportedSyntax
    applicationTime := .afterCompilation }

initialize attr2Attr : ParametricAttribute Name ←
  registerParametricAttribute {
    name := `attr2
    descr := "",
    getParam := fun nm stx => match stx with
    | `(attr| attr2) => do
      logInfo m!"{(dict.getState (← getEnv)).find? nm}"
      return `bar
    | _ => throwUnsupportedSyntax
    applicationTime := .afterCompilation }

then we get the following output:

import Mathlib.test

@[attr1, attr2] -- none
def foo := 1

@[attr2, attr1] -- none
def bar := 1

@[attr1]
def baz := 1

attribute [attr2] baz  -- some (foo)

[Gabriel Ebner]

Oh, it looks like registerParametricAttribute completely ignores the applicationTime field...