Repository navigation
Conversation
…t does NOT have This corpus resolves names across a namespace tree and has been settling, in its own vocabulary, questions C++ settled decades ago and deployed at enormous scale. DESIGN section 3 says to model the accepted framework rather than re-coin it, so this points at that framework instead. Cited to the working draft and VERIFIED BY FETCHING IT, per the same verify-or-refuse rule extdeps.languages.cpp.subject records for the committee page: the fetched page identifies itself as clause 6.5 `Name lookup` [basic.lookup] at commit c7015b485cc3db8efaa9dfb9ff0809c5394a4ed1. It is the WORKING DRAFT and not the published ISO/IEC 14882, and the module says so rather than implying the published text was read -- iso.org 403s it, the caveat the subject module already carries. The six forms are kept at the standard's own stable labels, because a nickname here would be a second name for a concept the citation already names. THE LOAD-BEARING OBSERVATION IS A NEGATIVE ONE. There is no rule in the cited clause that searches the whole program for a unique declaration when no enclosing scope declares the name; lookup walks outward and the program is ill-formed if exhausted. That absence is easy to lose -- it leaves no clause to cite -- so it is carried as a declaration rather than left to be re-derived. docs/plans/namespace-resolution-design.md rejects global-unique-fallback AS A CLASS, and this gives that rejection an external referent: the most widely deployed namespace system in existence simply has no such mechanism. Per DESIGN section 4d it is recorded at the strength observed -- a reading of one document at one commit, not a proof about the language. The boundary is explicit in both directions, because an extdeps module that declared ArgumentDependentLookup without saying it is excluded would invite a reader to take its presence for licence. Unqualified and qualified lookup ground this corpus; ADL, using-directives, member lookup and elaborated-type-specifier lookup are excluded, each with its reason. extdeps models the upstream faithfully; a consumer that departs states the departure on its own carrier. Evidence: four arms in test.claim.cpp_name_lookup_witness, 4 PASS. Mutation-verified: flipping ADL to GroundsThisCorpus reds the_four_widening_forms_are_not_imported and nothing else. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: fd1c8bafa8
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| // THE AMBIGUITY RULE. Note what it is keyed on: not "more than one declaration" but "do not all | ||
| // denote the same entity". Several declarations of ONE entity are not ambiguous; two entities are, | ||
| // and the program is ill-formed rather than resolved by any priority order. | ||
|
|
||
| data cpp_ambiguity_rule: NonEmptyStr = "Otherwise, if the declarations found by name lookup do not all denote the same entity, they are ambiguous and the program is ill-formed." as NonEmptyStr |
There was a problem hiding this comment.
When lookup finds declarations for two different functions or function templates, [basic.lookup.general] first says they form an overload set; only the subsequent “Otherwise” arm applies the same-entity ambiguity test. By presenting the latter sentence in isolation and asserting that any two entities are ambiguous, this model incorrectly classifies ordinary overloaded functions as ill-formed. Include the overload-set precondition or narrow this declaration so consumers cannot apply it to function lookup.
Useful? React with 👍 / 👎.
| type CppLookupFormUse | ||
| = GroundsThisCorpus { because: NonEmptyStr } | ||
| | NotImportedHere { because: NonEmptyStr } | ||
|
|
||
| fn cpp_lookup_form_use(form: CppLookupForm) -> CppLookupFormUse { |
There was a problem hiding this comment.
cpp_lookup_form_use records whether this repository imports each C++ feature, which is downstream consumer policy rather than a fact about C++. This conflicts with both this module's statement that departures belong on the consumer's carrier and the ExternalModelScope contract in dag/extdeps/external_authority.dag, which excludes consumer coverage state from upstream modules. Keeping it here couples the reusable C++ model to one consumer and exposes GroundsThisCorpus as though it were upstream data; move this disposition and its witness to a downstream corpus/compiler module.
Useful? React with 👍 / 👎.
| data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { | ||
| uri: Uri { | ||
| scheme: Https, | ||
| locator: "eel.is/c++draft/basic.lookup" |
There was a problem hiding this comment.
The modeled facts repeatedly claim to describe commit c7015b485cc3db8efaa9dfb9ff0809c5394a4ed1, but this locator is the moving eel.is draft page and contains no revision. Once that page advances, the module's sole external authority will attest a different text while observed_at continues naming the old commit, so the quotations and negative lookup claim can no longer be checked against their cited source. Use a commit-addressed draft URL for this authority.
Useful? React with 👍 / 👎.
|
|
||
| data cpp_unqualified_parent_scope_rule: NonEmptyStr = "If no declarations are found, the results of the unqualified search are the results of an unqualified search in the parent scope of S, if any, from P." as NonEmptyStr | ||
|
|
||
| data cpp_unqualified_parent_scope_rule_citation: NonEmptyStr = "[basic.lookup.unqual] 6.5.3 paragraph 2" as NonEmptyStr |
There was a problem hiding this comment.
This citation is an untyped positional string disconnected from both cpp_unqualified_parent_scope_rule and extdeps_external_authority_anchor; the ambiguity citation repeats the same pattern. Consequently a rule rename or replacement leaves the citation apparently valid, and tooling cannot resolve which declaration the authority attests. The repository's extdeps.external_authority.FactCitation exists specifically to bind a DeclarationRef to an authority, so use that carrier while retaining the clause label separately if needed.
Useful? React with 👍 / 👎.
1 participant
Why model another language's lookup
This corpus resolves names across a namespace tree, and has been settling — in its own vocabulary — questions C++ settled decades ago and deployed at enormous scale. DESIGN §3 says to model the accepted framework rather than re-coin it, and §1 says to replace convention with necessity. This points at the framework instead of re-deriving it.
Cited by fetching, not from memory
Verified the way
extdeps.languages.cpp.subjectrecords doing for the committee page: the fetched page identifies itself as clause 6.5Name lookup[basic.lookup] at working-draft commitc7015b485cc3db8efaa9dfb9ff0809c5394a4ed1.It is the working draft, not published ISO/IEC 14882, and the module says so rather than implying otherwise — iso.org 403s the published text, the caveat the subject module already carries.
The six forms keep the standard's own stable labels (
basic.lookup.unqual,basic.lookup.argdep,basic.lookup.qual,class.member.lookup,basic.lookup.elab,basic.lookup.udir). A nickname here would be a second name for a concept the citation already names.The load-bearing observation is a negative one
Two rules are quoted rather than paraphrased, because in both cases the condition is the content:
And the one that matters most here: there is no rule that searches the whole program for a unique declaration when no enclosing scope declares the name. Lookup walks outward; if exhausted, the program is ill-formed.
That absence is easy to lose — it leaves no clause to cite — so it's carried as a declaration rather than left to be re-derived by the next reader.
docs/plans/namespace-resolution-design.md§13 rejects global-unique-fallback as a class. This gives that rejection an external referent: the most widely deployed namespace system in existence simply has no such mechanism. Relevant becausev2.compiler.03_resolvecurrently does fall back that way underNamespaceOnlyY.Per DESIGN §4d it is recorded at the strength observed — a reading of one document at one commit, not a proof about the language.
The boundary is explicit in both directions
An
extdepsmodule declaringArgumentDependentLookupwithout saying it is excluded would invite a reader to take its presence for licence. So each form carries a disposition with its reason:extdepsmodels the upstream faithfully; a consumer that departs states its departure on its own carrier (§3b). This corpus is stricter than what is modeled here — it rejects nearest-wins shadowing, which C++ permits — and that departure belongs in the consumer, not here.Evidence
Four arms in
test.claim.cpp_name_lookup_witness, 4 PASS. Mutation-verified: flipping ADL toGroundsThisCorpusredsthe_four_widening_forms_are_not_importedand nothing else.The arms deliberately do not claim to check the model against the standard — no executing route here fetches it, and an arm asserting a quoted sentence equals itself would be a change detector. What they establish is the boundary.
🤖 Generated with Claude Code