From 26f508db87dea042a7c4d210c9228effa70674b7 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Thu, 26 Sep 2024 12:30:37 +0200
Subject: [PATCH] test: check that recusive functions do not apply attriubutes
 twices (#5480)

I suspected a bug based on reading the code, but it seems there is no
bug.
---
 tests/pkg/user_attr/UserAttr/BlaAttr.lean | 10 ++++
 tests/pkg/user_attr/UserAttr/Tst.lean     | 65 +++++++++++++++++++++++
 2 files changed, 75 insertions(+)

diff --git a/tests/pkg/user_attr/UserAttr/BlaAttr.lean b/tests/pkg/user_attr/UserAttr/BlaAttr.lean
index dd652db07b53..5373e6d96d2a 100644
--- a/tests/pkg/user_attr/UserAttr/BlaAttr.lean
+++ b/tests/pkg/user_attr/UserAttr/BlaAttr.lean
@@ -21,3 +21,13 @@ initialize fooAttr : ParametricAttribute (Nat × Bool) ←
     afterSet := fun declName _ => do
       IO.println s!"set attribute [foo] at {declName}"
   }
+
+syntax (name := trace_add) "trace_add" : attr
+
+initialize registerBuiltinAttribute {
+  name := `trace_add
+  descr := "Simply traces when added, to debug double-application bugs"
+  add   := fun decl _stx _kind => do
+    logInfo m!"trace_add attribute added to {decl}"
+  -- applicationTime := .afterCompilation
+}
diff --git a/tests/pkg/user_attr/UserAttr/Tst.lean b/tests/pkg/user_attr/UserAttr/Tst.lean
index ec7b9af6e477..c374a7c5c083 100644
--- a/tests/pkg/user_attr/UserAttr/Tst.lean
+++ b/tests/pkg/user_attr/UserAttr/Tst.lean
@@ -88,3 +88,68 @@ simproc [my_simp] reduceBoo (boo _) := fun e => do
 example : f x + boo 2 = id (x + 2) + 12 := by
   simp
   simp [my_simp] -- Applies the simp and simproc sets
+
+
+namespace TraceAdd
+
+set_option trace.Meta.Tactic.simp.rewrite false
+
+/-- info: trace_add attribute added to TraceAdd.foo -/
+#guard_msgs in
+@[trace_add] def foo := 1
+
+/-- info: trace_add attribute added to TraceAdd.foo -/
+#guard_msgs in
+attribute [trace_add] foo
+
+/-- info: trace_add attribute added to TraceAdd.structural -/
+#guard_msgs in
+@[trace_add] def structural : Nat → Nat
+  | 0 => 0
+  | n+1 => structural n+1
+termination_by structural n => n
+
+/-- info: trace_add attribute added to TraceAdd.wf -/
+#guard_msgs in
+@[trace_add] def wf : Nat → Nat
+  | 0 => 0
+  | n+1 => wf n+1
+termination_by n => n
+
+/--
+info: trace_add attribute added to TraceAdd.mutual_structural_1
+---
+info: trace_add attribute added to TraceAdd.mutual_structural_2
+-/
+#guard_msgs in
+mutual
+@[trace_add] def mutual_structural_1 : Nat → Nat
+  | 0 => 0
+  | n+1 => mutual_structural_2 n+1
+termination_by structural n => n
+@[trace_add] def mutual_structural_2 : Nat → Nat
+  | 0 => 0
+  | n+1 => mutual_structural_1 n+1
+termination_by structural n => n
+end
+
+/--
+info: trace_add attribute added to TraceAdd.mutual_wf_1._mutual
+---
+info: trace_add attribute added to TraceAdd.mutual_wf_1
+---
+info: trace_add attribute added to TraceAdd.mutual_wf_2
+-/
+#guard_msgs in
+mutual
+@[trace_add] def mutual_wf_1 : Nat → Nat
+  | 0 => 0
+  | n+1 => mutual_wf_2 n+1
+termination_by n => n
+@[trace_add] def mutual_wf_2 : Nat → Nat
+  | 0 => 0
+  | n+1 => mutual_wf_1 n+1
+termination_by n => n
+end
+
+end TraceAdd