fix(Translate): apply (attr := ...) attributes in order of application time

Mathlib/Tactic/Translate/Core.lean

@@ -1205,7 +1205,19 @@ partial def applyAttributes (t : TranslateData) (cfg : Config) (src tgt : Name)
   let allDecls := #[src, tgt] ++ nestedDecls
   if attrs.size > 0 then
     trace[translate_detail] "Applying attributes {attrs.map (·.stx)} to {allDecls}"
+  -- Sort the attributes based on their application time.
+  let mut attrs₁ := #[]
+  let mut attrs₂ := #[]
+  let mut attrs₃ := #[]
   for attr in attrs do
+    match getAttributeImpl (← getEnv) attr.name with
+    | .error errMsg => throwError errMsg
+    | .ok attrImpl =>
+      match attrImpl.applicationTime with
+      | .beforeElaboration => attrs₁ := attrs₁.push attr
+      | .afterTypeChecking => attrs₂ := attrs₂.push attr
+      | .afterCompilation => attrs₃ := attrs₃.push attr
+  for attr in attrs₁ ++ attrs₂ ++ attrs₃ do
     if let some impl := (← generatingAttrs.get).find? attr.name then
       withRef attr.stx do withLogging do
         translateLemmas t allDecls "simps lemmas" cfg

MathlibTest/Attribute/ToDual.lean

@@ -455,3 +455,20 @@ structure HasLimitsOfSize where
 @[to_dual]
 structure HasColimitsOfSize where
   cofoo : ∀ _ : Type u, True
+
+-- The `simps` attribute is applied after `implicit_reducible`,
+-- which allows the `simps` lemmas to be `@[defeq]`
+@[to_dual (attr := simps, implicit_reducible) MyLE']
+def MyLE : Preorder α where
+  le := (· ≤ ·)
+  lt := (· < ·)
+  le_refl := le_refl
+  le_trans _ _ _ := le_trans
+  lt_iff_le_not_ge _ _ := lt_iff_le_not_ge
+
+/--
+info: @[defeq] theorem MyLE_le : ∀ {α : Type} [inst : PartialOrder α] (x1 x2 : α), (x1 ≤ x2) = (x1 ≤ x2) :=
+fun {α} [PartialOrder α] x1 x2 => Eq.refl (x1 ≤ x2)
+-/
+#guard_msgs in
+#print MyLE_le