[Deicyde]

Closes #266. I took this on 2026-10-14 when the user asked for new work; the board lists #266 under this session.

The declaration index skipped Batteries' alias. So an article whose lean: named an alias got lean-target-not-found from autoform audit --lean-root, and render built no link for it. ATLAS v1 has six such targets, the last ones the index cannot resolve.

Indexing (autoform_cli/lean.py)

• alias b := a records b, and alias ⟨mp, mpr⟩ := a_iff records each of its names that is not _. Neither is recorded as ⟨mp.
• Attributes and modifiers are read as for any declaration.
• The := must be on the alias's line, which keeps lines where alias is an ordinary identifier out of the index. The target may be on that line or the next nonblank one.
• Every declaration now records whether it is protected, written on its line or on the lines above that hold only attribute lists and modifiers.
• A name written _root_.X is recorded as X, whatever namespace it is declared in. This applies to every declaration, not only aliases: theorem _root_.X inside a namespace was indexed under that namespace before.
• SourceIndex.alias_target resolves one alias, and SourceIndex.reached follows a chain of them.

How the audit treats an alias (autoform_cli/audit.py)

An alias has its target's kind, size and elaboration limits when the index can be sure what the target is.

Resolving the target.

• The audit tries the names Lean tries: the alias's namespace, each enclosing one, then the root. It passes over a declaration below the alias in its file, which Lean has not seen yet.
• The first other name must be an earlier declaration in the same file. Otherwise the target is unknown:
  • a name the index lacks may come from Mathlib;
  • one in another file may not be imported;
  • a protected one for a one-component target is skipped by Lean unless the module system has also made it private.
• An alias whose target is unknown matches any intent, and is measured by its own span, like any other declaration.
• On ATLAS, the review counted 69 aliases the first version placed; 68 of them have their target in their own file.

Kind.

• lean-target-kind-mismatch names an alias's kind as alias of def.
• Each name of an iff alias, and any alias of one, is a theorem whatever its target is, since Batteries emits a thmDecl.
• An alias of a non-theorem is a def in Batteries. The audit still checks it against its target's kind, because it asks what object an article describes, and an alias names its target's.

Other checks.

• lean-target-wanted reports an alias of a wanted command.
• An indexed alias ends the deprecated-attribute search and the node-too-large span of the declaration above it. Its own @[deprecated] makes it a deprecated target.

autoform unused-hypotheses

It now refuses an alias as an unread target ("an alias, whose own proof only names its target"), and the run exits 1. The probe would otherwise report every hypothesis as used.

Not covered

• An alias whose target is in another file is not followed.
• A target reachable only through open stays unresolved.
• An iff alias with its ⟨…⟩ list split across lines, or with its := on the next line, is not indexed. Mathlib has six.

Tests

• test_aliases_are_indexed_with_where_their_target_can_be:

  • both alias forms;
  • _ slots, modifiers and attributes;
  • guillemets, including a «x.y» target that counts as one component;
  • _root_ in names and targets;
  • a target on the very next line and after a blank line;
  • lines where alias is an ordinary identifier.

• test_root_qualified_names_leave_their_namespace_out.

• test_an_alias_is_followed_only_to_an_earlier_declaration_of_its_file:

  • a chain;
  • a same-file private target;
  • a dotted target that reaches a protected declaration;
  • an alias named like its target, which passes over itself.

  These come out unknown:

  • a cross-file alias, even when its own file holds an outer candidate;
  • a protected one-component target, with protected on the same line or on the line above;
  • a chain whose end the index cannot place.

• test_audit_resolves_an_alias_s_target_as_lean_does: every resolved alias shows as a finding, covering:

  • same namespace;
  • a chain;
  • a private target;
  • a declaration below the alias;
  • an iff alias of a Mathlib lemma and of a local axiom, and an alias of an iff alias;
  • innermost namespace first.

  Five aliases that cannot be placed must give no finding:

  • a protected target;
  • an enclosing-namespace target;
  • a target in another file;
  • the Mathlib-shadowed Nat case;
  • a Mathlib target.

• test_audit_reads_an_alias_s_limits_and_wanted_command_from_its_target:

  • a plain alias and an iff alias each report their target's limit;
  • an alias the index cannot place keeps its own limits;
  • an alias of a wanted command is reported as one.

• test_audit_measures_an_alias_by_its_target_s_span: the target named beside its alias counts once.

• test_an_alias_is_refused_without_running_lean, in test_unused_hypotheses.py: a cross-file alias and one the index could follow are both refused.

• test_an_alias_ends_the_source_span_of_the_declaration_above_it, plus an old-alias case in the deprecated test.

Twenty-four mutants of the change were each caught by these tests:

• the candidate order reversed, or only the first candidate tried;
• no chain following;
• the iff rule applied after resolving;
• other files allowed;
• continuing past a candidate the index lacks;
• no declared-later rule;
• protected always visible, or always skipped;
• the alias's keyword used in the wanted check;
• the alias's own limits and size;
• no dedup of a target named beside its alias;
• no unused-hypotheses refusal;
• _root_ kept in names;
• the next nonblank line skipped;
• atomicity read from a .;
• a cross-file candidate skipped instead of ending the search;
• the line check run before the file check;
• > for >= in the line check, which loops on an alias named like its target;
• reached stopping at an iff alias;
• an unplaced alias contributing no limits;
• unused-hypotheses refusing only unplaced aliases;
• a partly placed chain returning its last placed alias;
• protected read only from the keyword's line.

The unit suite on Python 3.10 passed on the second commit: https://github.com/facebookresearch/autoform-bot/actions/runs/38540151992. CI on this PR covers the third.

Review history

An adversarial review of the first commit found that it treated every project file as visible. That could reach a declaration Lean cannot see: a downstream or unrelated file, Batteries' implicitly private wanted placeholders, or module-system private names. It also found that an iff alias could take its local target's kind. The second commit narrows resolution to the alias's own file, makes iff aliases theorems, and adds the tests above.

A review of the second commit found that protected written on its own line above the keyword, as Mathlib does 29 times, was not recorded. It also found that several rules that end resolution were unpinned. The third commit reads modifiers from those lines and adds the tests for them.

Overlap

Trial merges are clean against #307, #296, #300 and #301. The rest resolve mechanically.

#90, in lean.py and audit.py:

• keep Scale roadmap inventories and the full DAG explorer #90's universe-binder stripping, then build the name with _qualified(namespaces, name) and pass protected;
• Scale roadmap inventories and the full DAG explorer #90 moves the lean-target-wanted block above the kind check, so compute bodies and kinds before it and keep this PR's kind and what in it;
• the size line becomes if resolved and node.catalog is None: sizes[node_id] = sum(spans[body.name] for body in bodies).

The #212-#219 and #284 stack, in lean.py, the README and tests/test_audit.py:

• the stack's _scan returns found, len(lines), so keep that return, with this PR's Declaration(...) line;
• the unused-hypotheses exit sentence becomes "it is not found, several source files declare it, or it is an alias, whose proof only names its target";
• keep both imports in tests/test_audit.py.

This machine is over the agreed load limit for local pytest runs. The tests were called directly in Python, and CI on this PR is the full run.

[Deicyde]

Verdict: ready to merge once it is out of draft. This review covers head f3f8be2. The PR went through three review rounds; each round's should-fix findings are fixed in the commit that followed it, and nothing above a nit remains.

Review rounds

1. First commit:

   • Resolution treated every other project file as visible. Lean sees only what a file imports, so a downstream or unrelated file could supply an alias's target, and the audit would report a wrong kind and charge another declaration's limits and span to the article. Batteries' wanted placeholders and module-system declarations are private without saying so, so they hit the same problem.
   • An iff alias took a local target's kind.
   • Six mutants survived the tests.

   The second commit follows an alias only to an earlier declaration of its own file, makes iff aliases theorems, and adds tests.

2. Second commit:

   • protected written on its own line above the keyword was not recorded. Mathlib does this 29 times.
   • The rules that end resolution were unpinned. One of them, the >= in the line check, is the only thing that stops an alias named like its target from looping.

   The third commit reads modifiers from those lines and adds the tests.

3. Third commit: checked here.

What was checked

• CI: all 11 checks pass on f3f8be2, real Lean included.
• Resolution against Lean: alias_target was compared with resolveGlobalName, resolveQualifiedName and resolvePrivateName (Lean/ResolveName.lean, the same from v4.27.0 to v4.35.0).
  • It returns None at a candidate the index lacks or one in another file.
  • It passes over a candidate below the alias in its file.
  • It returns None for a protected candidate with a one-component target. Lean skips such a candidate unless it is also private, written or under the module system.
  • Each step goes to an earlier line of one file, so chains end.
• Batteries: both names of an iff alias are theorems (addSide emits a thmDecl), and so is a plain alias of one (wasOriginallyTheorem).
• Tests: 24 mutants of the change were each caught by the tests. They are listed in the description.
• Scale: on ATLAS, 68 of the 74 aliases have their target earlier in their own file and are followed. The other six stay unknown and match any intent: five Mathlib targets reached through open ... in, and one in another file. On Mathlib, a survey of 5,766 aliases found every resolved target inside its file's import closure.

Known limits. None of these blocks merge.

1. Only same-file targets are followed. A cross-file alias matches any intent and is measured by its own span and limits. Following imports would recover the one cross-file ATLAS alias.

2. Shared target spans. An article naming an alias and another article naming its target are each charged the target's span, so a large target can give both a node-too-large. Splitting the target clears both.

3. Inherited scanner limits. Some limits of the lexical scanner now apply to aliases too:

   • namespace A.B … end B loses track of the namespace;
   • export, and import all;
   • declaration-like lines inside multi-line strings;
   • a quoted namespace component holding a dot, which gives an impossible candidate.

   These predate the PR, and each fails toward "unknown" or an existing gap rather than a new false finding.

4. Unindexed iff aliases. An iff alias whose ⟨…⟩ list is split across lines, or whose := is on the next line, is not indexed. Mathlib has six.

Overlap. #90 and the #212-#219/#284 stack each conflict mechanically. The description gives the resolution for whichever lands second.

Posted by PR swarm: PR Swarm Lead