Add scripts/ + docs/REFACTOR_PLAYBOOK.md — long-term refactor cost reduction

Goal: same operation never costs more than the first time.

scripts/:
- rewrite-import.sh OLD NEW — bulk import path rewrite, refuses dirty
  working tree.
- lean-grep.sh — grep -r restricted to .lean (excludes .lake/, .git/).
- README.md — convention: lift into scripts/ after 3+ repetitions.

docs/REFACTOR_PLAYBOOK.md:
- Decision tree mapping refactor type → tool (LSP rename / scripts /
  Lake script / manual).
- Pre-flight checklist + atomic-commit discipline.
- Lake script vs bash matrix (Lake for AST-aware ops).
- Pitfall log from this lib's history: sed-corrupts-docstrings,
  open-scoped-namespace-missing, notation-parser-conflicts, eta in
  notation RHS, typeclass inference stuck, force-pushed trailers
  persisting in GitHub cache.
- Self-extending: 3+-repeat operations promote to playbook entries.

Author: Xinze-Li-Moqian

docs/REFACTOR_PLAYBOOK.md

@@ -0,0 +1,159 @@
+# Refactor Playbook
+
+Source of truth for OpenGALib refactor workflows. Sister to `scripts/`
+(reusable codemods) and the project's CLAUDE.md (architectural stance).
+
+The goal: **same operation never costs more than the first time**.
+
+---
+
+## Decision tree
+
+```
+What's the refactor about?
+├─ Rename a single identifier (def, theorem, structure field)?
+│   └─ VSCode F2 (Rename Symbol).
+│      Lean LSP scans the import graph semantically.
+│      Doesn't touch docstrings/comments. Safest possible.
+│
+├─ Rewrite an import path prefix across many files?
+│   └─ scripts/rewrite-import.sh OLD_PREFIX NEW_PREFIX
+│      Idempotent, refuses dirty working tree, prefix-match.
+│
+├─ Move file or directory?
+│   └─ git mv first, then scripts/rewrite-import.sh.
+│      git mv preserves rename detection in history.
+│
+├─ Introduce or migrate notation?
+│   └─ Hand-write a 5-line example file FIRST. Verify parsing,
+│      typeclass inference, simp interaction — before any sweep.
+│      THEN bulk-migrate via perl/sed AND audit docstrings
+│      (text replace catches them too — see Pitfalls #2).
+│
+├─ Change a typeclass cascade or generic signature?
+│   └─ Manual. No bulk tool helps. Build incrementally.
+│      Use git checkpoints between each step.
+│
+├─ Need an AST-aware operation (rename only in code, not in
+│   docstrings; find all theorems referencing X; etc.)?
+│   └─ Lake script. See "Lake script vs bash" below.
+│
+└─ Bulk delete dead content (e.g., a sub-package being removed)?
+    └─ git rm -r + scripts/lean-grep.sh to find dangling refs +
+       manual cleanup of those refs.
+```
+
+---
+
+## Pre-flight checklist (always)
+
+1. **`git status` clean.** No uncommitted changes. The bulk operation
+   should be a single revertible step.
+2. **Snapshot commit** of the current good state if there's any pending
+   work: `git commit -am "snapshot before X refactor"`.
+3. **One refactor concern per commit.** Don't bundle "rename + reorganize
+   + add deprecation alias" into one diff. Three separate commits.
+4. **`lake build` after each commit.** Catches silent breakage early
+   when revert is still cheap.
+
+If anything fails: `git reset --hard HEAD~1` and retry. The atomic-commit
+discipline makes rollback one command.
+
+---
+
+## Lake script vs bash — when to use which
+
+| Need | Tool | Reason |
+|------|------|--------|
+| File text replacement | bash + sed/perl | Milliseconds, well-understood |
+| Import path rewrite | `scripts/rewrite-import.sh` | Already written |
+| `grep` on Lean source only | `scripts/lean-grep.sh` | Excludes `.lake/`, `.git/` |
+| Rename identifier in code only (skip docstrings) | Lake script | Needs Lean syntax tree |
+| Find all theorems whose statement uses X | Lake script | Needs `Lean.Environment` API |
+| Audit `@[simp]` lemma RHS shapes | Lake script | Needs elaborator |
+| Generate a typeclass dependency graph | Lake script | Needs full elab info |
+| One-off file munging | Inline shell command | Don't bother formalizing |
+
+**Rule of thumb:** if the codemod would need to *understand* Lean
+syntax or semantics, write it in Lean (Lake script). Otherwise bash is
+faster to write and run.
+
+### Lake script template
+
+In `lakefile.lean`:
+
+```lean
+script myCodemod (args : List String) do
+  match args with
+  | [arg1, arg2] =>
+    -- ... do work using IO + Lean APIs ...
+    return 0
+  | _ =>
+    IO.eprintln "Usage: lake script run myCodemod ARG1 ARG2"
+    return 1
+```
+
+Invoke: `lake script run myCodemod foo bar`.
+
+For AST-level work, `import Lean` and use `Lean.Environment`,
+`Lean.Syntax`, `Lean.Elab.*`. Mathlib's `scripts/` directory has good
+examples.
+
+---
+
+## Pitfalls (encountered, in this lib's history)
+
+1. **Text-level sed corrupts docstrings.** `sed 's/X/Y/g'` on `.lean`
+   files matches `X` inside `/-- ... -/` blocks too. After bulk
+   migration, search docstrings with `scripts/lean-grep.sh '<old form>'`
+   and clean residual mentions. Or use VSCode F2 (semantic) when
+   available.
+
+2. **`open scoped X` requires the namespace to exist via imports.**
+   Adding `open scoped X` to a file whose import graph doesn't reach a
+   `namespace X` declaration produces "unknown namespace X" build
+   error. After any sweep that adds scoped opens, verify with
+   `scripts/lean-grep.sh 'open scoped'`.
+
+3. **Notation prefix conflicts with built-in syntax.**
+   - `T[x]` clashes with Lean's array indexing (`term[term]`)
+   - `T x` (where `T` is an identifier) is parsed as function
+     application, beating a `notation:max "T " x:max` pattern
+   - Solutions that work: paren form (`Tan(x)`, like `Ric(X, Y)`),
+     bracket form with non-identifier prefix (`∇[X]`, since `∇` is in
+     Unicode category `Sm`, not `Lu`).
+
+4. **Notation requires careful eta-reduction.** `fun x => f x`
+   wrappers in notation RHS create lambdas that don't beta-reduce in
+   simp's normal form, breaking pattern matches in subsequent rewrites.
+   Always eta-reduce: `notation X => f` not `notation X => fun x => f x`.
+
+5. **Typeclass inference can fail through `_` in notation.** A
+   `notation:max "Tan(" x ")" => TangentSpace _ x` gets stuck when
+   Lean can't pin the implicit `I : ModelWithCorners` from
+   surrounding context. If this happens repeatedly, either:
+   (a) keep the original verbose form `TangentSpace I x`, or
+   (b) make `I` explicit in the notation.
+   `abbrev`-based shorthands hit similar issues.
+
+6. **Force-pushing to remove an oversight is partially effective.**
+   `Co-Authored-By: ...` trailers, once pushed to a public repo,
+   remain in GitHub's contributor cache even after the commit is
+   force-pushed away. The orphan commit is still server-side. Lesson:
+   **don't push to a public repo with a trailer you'd regret**.
+   Memory `feedback_release_repo_attribution.md` enforces this for
+   MathNetwork/OpenGA going forward.
+
+---
+
+## Adding to this playbook
+
+When a refactor pattern is performed **3+ times** with the same
+manual workaround, lift it into:
+
+* a `scripts/` entry (if shell-tool-shaped), or
+* a `lake script` entry (if AST-aware), and
+* a row in the decision tree above + a Pitfall note if it has a known
+  failure mode.
+
+The playbook is dogfood. Trust accumulates over commits.

scripts/README.md

@@ -0,0 +1,40 @@
+# `scripts/`
+
+Reusable codemods + dev helpers for OpenGALib refactor workflows.
+Sister to `docs/REFACTOR_PLAYBOOK.md` (which documents the decision
+tree for *which* tool to reach for).
+
+## Available scripts
+
+* **`rewrite-import.sh OLD_PATH NEW_PATH`** — rewrite every
+  `import OLD_PATH...` line to `import NEW_PATH...` across all `.lean`
+  files. Prefix match, so paths nested under `OLD_PATH` come along
+  automatically. Refuses to run on a dirty working tree.
+
+* **`lean-grep.sh [grep_flags] PATTERN`** — `grep -r` restricted to
+  `.lean` files, excluding `.lake/` and `.git/`. Use this instead of
+  raw `grep` to avoid matching Mathlib source under `.lake/`.
+
+## Convention for adding new scripts
+
+1. Triggered by **3+** repetitions of the same manual command in past
+   refactor sessions. One-off pain doesn't justify a script.
+2. Self-contained shell scripts (no Python / Node deps). `bash` + standard
+   Unix tools (`grep`, `sed`, `perl`, `find`).
+3. **Refuse to run on dirty working tree** if the script makes bulk
+   modifications. Bulk edits must be one revertible step.
+4. Document inputs / examples in the script header.
+5. Add an entry to this README's "Available scripts" list.
+
+## Why scripts and not just inline commands?
+
+Each script is a **frozen decision** about how to handle a recurring
+operation safely. Inline `sed` / `find` commands accumulate
+context-specific bugs (forget to exclude `.lake/`, miss a `git status`
+check, etc.). Lifting them into named scripts gives:
+
+* **Repeatability** — `scripts/rewrite-import.sh A B` always behaves the
+  same way, no edge case rediscovered.
+* **Documentation** — the script header is the spec.
+* **Auditability** — `git log scripts/` shows how the workflow has
+  evolved.

scripts/lean-grep.sh

@@ -0,0 +1,39 @@
+#!/usr/bin/env bash
+# Smart grep restricted to Lean source files in the project.
+# Excludes .lake/, .git/, and only matches .lean files.
+#
+# Usage:
+#   scripts/lean-grep.sh [GREP_FLAGS...] PATTERN [PATH...]
+#
+# Examples:
+#   scripts/lean-grep.sh -n 'TangentSpace I'         # show line numbers
+#   scripts/lean-grep.sh -l 'open scoped Riemannian' # list files only
+#   scripts/lean-grep.sh -E 'covDeriv|mlieBracket'   # extended regex
+#
+# Equivalent to:
+#   grep -r --include='*.lean' --exclude-dir=.lake --exclude-dir=.git "$@"
+# but always with the right exclusions so you never accidentally match
+# Mathlib source under .lake/ or stale build artifacts.
+
+set -euo pipefail
+
+if [[ $# -eq 0 ]]; then
+  echo "Usage: $0 [GREP_FLAGS...] PATTERN [PATH...]" >&2
+  echo "If no PATH given, searches from cwd." >&2
+  exit 1
+fi
+
+# Default search root if no path given: current directory.
+HAS_PATH=0
+for arg in "$@"; do
+  case "$arg" in
+    -*) ;;
+    *) HAS_PATH=1; break ;;
+  esac
+done
+
+if [[ $HAS_PATH -eq 0 ]]; then
+  exec grep -r --include='*.lean' --exclude-dir=.lake --exclude-dir=.git "$@" .
+else
+  exec grep -r --include='*.lean' --exclude-dir=.lake --exclude-dir=.git "$@"
+fi

scripts/rewrite-import.sh

@@ -0,0 +1,65 @@
+#!/usr/bin/env bash
+# Rewrite Lean import path prefixes across the project.
+#
+# Usage:
+#   scripts/rewrite-import.sh OLD_PATH NEW_PATH
+#
+# Example:
+#   scripts/rewrite-import.sh OpenGALib.Riemannian.Util OpenGALib.Util
+#
+# This rewrites every `import OLD_PATH...` line to `import NEW_PATH...`
+# across all .lean files (excluding .lake/, .git/). Prefix-only match,
+# so `import OLD_PATH.X.Y` becomes `import NEW_PATH.X.Y` automatically.
+#
+# Refuses to run on a dirty working tree — commit or stash first so the
+# bulk edit is one revertible step.
+
+set -euo pipefail
+
+if [[ $# -ne 2 ]]; then
+  cat >&2 <<EOF
+Usage: $0 OLD_PATH NEW_PATH
+
+Example:
+  $0 OpenGALib.Riemannian.Util OpenGALib.Util
+EOF
+  exit 1
+fi
+
+OLD="$1"
+NEW="$2"
+
+# Refuse to run on dirty working tree.
+if [[ -n "$(git status --porcelain --untracked-files=no)" ]]; then
+  echo "error: working tree not clean (modified files exist)." >&2
+  echo "Commit or stash first; bulk edits should be a single revertible step." >&2
+  git status --short >&2
+  exit 1
+fi
+
+# Escape regex metacharacters in OLD path.
+OLD_ESCAPED=$(printf '%s' "$OLD" | sed 's/[][\\.*^$/]/\\&/g')
+
+# Find files containing the import.
+FILES=$(grep -rlE "^import ${OLD_ESCAPED}" \
+          --include="*.lean" \
+          --exclude-dir=.lake --exclude-dir=.git \
+          . || true)
+
+if [[ -z "$FILES" ]]; then
+  echo "No files import '$OLD'. Nothing to do." >&2
+  exit 0
+fi
+
+# Show what will change.
+COUNT=$(echo "$FILES" | wc -l | tr -d ' ')
+echo "Rewriting 'import $OLD...' → 'import $NEW...' in $COUNT file(s):"
+echo "$FILES" | sed 's/^/  /'
+echo
+
+# Apply.
+echo "$FILES" | xargs perl -i -pe "s|^import ${OLD_ESCAPED}|import ${NEW}|"
+
+echo "Done. Verify with:"
+echo "  lake build"
+echo "If green, commit. If broken, 'git reset --hard' to revert."