refactor: rename auto_attach attribute to wf_preprocess (#6972)

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

@@ -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"

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

stage0/src/stdlib_flags.h

@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// please update stage0
+
 namespace lean {
 options get_default_options() {
     options opts;