From 2e6206bbeb24108e3aa8e50322109ddbdf248b36 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Thu, 6 Feb 2025 12:28:23 +0100
Subject: [PATCH] refactor: rename auto_attach attribute to wf_preprocess
 (#6972)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

As per dicussion with team colleages, the feature shouldn’t be called
“auto attach” but rather “well-founded recursion preprocessing” to avoid
(imprecise) jargon.
---
 src/Init/Tactics.lean                          | 4 ++--
 src/Lean/Elab/PreDefinition/WF/AutoAttach.lean | 4 ++--
 stage0/src/stdlib_flags.h                      | 2 ++
 3 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index 4a93db2782..96468f9cd7 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -1663,12 +1663,12 @@ If there are several with the same priority, it is uses the "most recent one". E
 syntax (name := simp) "simp" (Tactic.simpPre <|> Tactic.simpPost)? patternIgnore("← " <|> "<- ")? (ppSpace prio)? : attr
 
 /--
-Theorems tagged with the `auto_attach` attribute are used during the processing of functions defined
+Theorems tagged with the `wf_preprocess` attribute are used during the processing of functions defined
 by well-founded recursion. They are applied to the function's body to add additional hypotheses,
 such as replacing `if c then _ else _` with `if h : c then _ else _` or `xs.map` with
 `xs.attach.map`. Also see `wfParam`.
 -/
-syntax (name := auto_attach) "auto_attach" (Tactic.simpPre <|> Tactic.simpPost)? patternIgnore("← " <|> "<- ")? (ppSpace prio)? : attr
+syntax (name := wf_preprocess) "wf_preprocess" (Tactic.simpPre <|> Tactic.simpPost)? patternIgnore("← " <|> "<- ")? (ppSpace prio)? : attr
 
 /-- The possible `norm_cast` kinds: `elim`, `move`, or `squash`. -/
 syntax normCastLabel := &"elim" <|> &"move" <|> &"squash"
diff --git a/src/Lean/Elab/PreDefinition/WF/AutoAttach.lean b/src/Lean/Elab/PreDefinition/WF/AutoAttach.lean
index 586c03708e..13cc559dc1 100644
--- a/src/Lean/Elab/PreDefinition/WF/AutoAttach.lean
+++ b/src/Lean/Elab/PreDefinition/WF/AutoAttach.lean
@@ -12,8 +12,8 @@ open Lean Meta
 
 namespace Lean.Elab.WF
 
-builtin_initialize autoAttachSimpExtension : SimpExtension ←
-  registerSimpAttr `auto_attach
+builtin_initialize wfPreprocessSimpExtension : SimpExtension ←
+  registerSimpAttr `wf_preprocess
     "(not yet functional)"
 
 end Lean.Elab.WF
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index b647d85f37..51489f0e3c 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// please update stage0
+
 namespace lean {
 options get_default_options() {
     options opts;