Architectural follow-up from /sweep of epic #20732 (7 AlphaProof Nexus integrations).
Problem
Three of the seven AlphaProof Nexus port PRs (#20836, #20838, #20839) needed a Doctor cycle for the same class of bug: after the sed-style namespace rename (namespace Erdos741 → namespace Erdos741APN_I, etc.), in-body references inside tactic invocations like delta Erdos741.foo at h, simp_all [Erdos152.D_set], change Erdos26.X_seq kept the old namespace prefix.
The naïve sed s/^namespace Erdos741/namespace Erdos741APN_I/ only catches the ^namespace/^end lines, missing every in-body occurrence. The errors only surface at docker-build time. PR #20837 had one such leftover marked non-blocker; #20838 had three; #20839 had two — same root cause, three Doctor cycles burned.
Proposal
A small pre-PR check (script or Lean linter) that, given a file with namespace Foo declared, flags any token of the form Foo.<Ident> inside the file body. The flagged occurrences can then be either qualified to the renamed namespace or stripped to the unqualified form before the PR opens.
Rough sketch (Bash/grep is enough for the common case):
ns=$(grep -oP "^namespace \K\S+" "$file" | head -1)
old_ns=$(git log -p -- "$file" | grep -oP "^-namespace \K\S+" | head -1)
[ -n "$old_ns" ] && grep -n "\b${old_ns}\.[A-Z]" "$file"More robust as a Lean-syntax-aware linter, but grep-based catches >90% of cases.
Acceptance
- Script or check available in the repo (e.g.,
scripts/lint/check-renamed-namespace-refs.sh).
- A future port of an AlphaProof Nexus file would catch the namespace-leftovers before the builder opens the PR.
- Optional: integrate into the builder skill prompt so this is part of the pre-push checklist.
This is a small tooling investment; /architect or /hermit could scope it.
Architectural follow-up from /sweep of epic #20732 (7 AlphaProof Nexus integrations).
Problem
Three of the seven AlphaProof Nexus port PRs (#20836, #20838, #20839) needed a Doctor cycle for the same class of bug: after the
sed-style namespace rename (namespace Erdos741→namespace Erdos741APN_I, etc.), in-body references inside tactic invocations likedelta Erdos741.foo at h,simp_all [Erdos152.D_set],change Erdos26.X_seqkept the old namespace prefix.The naïve
sed s/^namespace Erdos741/namespace Erdos741APN_I/only catches the^namespace/^endlines, missing every in-body occurrence. The errors only surface at docker-build time. PR #20837 had one such leftover marked non-blocker; #20838 had three; #20839 had two — same root cause, three Doctor cycles burned.Proposal
A small pre-PR check (script or Lean linter) that, given a file with
namespace Foodeclared, flags any token of the formFoo.<Ident>inside the file body. The flagged occurrences can then be either qualified to the renamed namespace or stripped to the unqualified form before the PR opens.Rough sketch (Bash/grep is enough for the common case):
More robust as a Lean-syntax-aware linter, but
grep-based catches >90% of cases.Acceptance
scripts/lint/check-renamed-namespace-refs.sh).This is a small tooling investment; /architect or /hermit could scope it.