the interface list an implementation provides is derived from its artefact - #42
Merged
Merged
Conversation
…efact `provides-interfaces` in a package manifest is a declaration, and a declaration is checked rather than trusted. The check available to it already exists: clause 9's surface comparison walks SURFACE.txt group by group and decides, for each, whether the artefact exports it whole, in part, or not at all. "Which interfaces does this implementation provide" is that walk stopped one step earlier. `check-surface.sh` gains `--interfaces` and `--toml` rather than a second script, because a second derivation of the same walk would go stale the first time a group was added. `--toml` prints the array a manifest carries, so a package's declaration is GENERATED FROM THE ARTEFACT: a declaration derived from the thing it describes cannot disagree with it, and an implementation that gains an interface cannot forget to say so. `openkal.version` is excluded. SURFACE.txt says in its own header that it is not an interface --- it provides no resource --- and every conforming implementation exports it, so listing it would put a name that answers nothing in every package. A group exported in PART is not listed. An interface is provided in whole or not at all (clause 3), so half of one is not a smaller claim but a different and false one. CI asserts both directions against a real implementation: the list contains openkal.stream, and removing one of that group's definitions takes it out. Without the second leg the first passes against a script that prints every group in SURFACE.txt and reads no artefact at all. Co-authored-by: Claude Code <noreply@anthropic.com>
… object behind The step that requires the surface checker to reject an unspecified name removes `src/extra.cpp` and not the object it produced, so a `find` over `target/` still reports `kal_vendor_extension` and the next step examines an artefact no source in the tree describes. It now starts from a clean build, and refuses to run against an empty object list. Co-authored-by: Claude Code <noreply@anthropic.com>
…ims nothing impl-fd exists to show substitution, not conformance: it defines six of openkal.stream's seven names and none of any other group, so no interface is exported whole and every leg of the step was measuring an implementation that claims nothing --- which is why it reported 'no interface is exported whole' rather than a list. The subject is now an object built from SURFACE.txt in the step, with three groups whole and two names of a fourth. The answer is known in advance, which is what lets the check fail for the one reason it exists to catch: a group exported in part must not be listed, because an interface is provided in whole or not at all. Co-authored-by: Claude Code <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
provides-interfaces是一个声明，而声明要被校验而不是被信任。可用的校验早已存在：clause 9 的 surface 比对按SURFACE.txt的分组逐组走，对每一组判定产物是整组导出、部分导出、还是完全没有。"这个实现提供了哪些接口"就是这次行走早一步停下。改动
check-surface.sh增加--interfaces与--toml两个模式，而不是新写一个脚本——同一次行走的第二份推导会在新增一个组的那一刻起失效。于是一个包的
provides-interfaces由产物生成而不是手写：一个从它所描述的东西派生出来的声明，不可能与它不符；一个新增了接口的实现，也不可能忘了说。两处判定
openkal.version排除。SURFACE.txt自己的头里写明它不是接口（它不提供资源），而每个符合规范的实现都导出它——列出它等于在每个包里放一个什么都不回答的名字。判据
CI 新增一步，对真实实现两个方向各断言一次：
openkal.stream出现在列表里；没有第二条，第一条对一个"打印 SURFACE.txt 里每个组、根本不读产物"的脚本同样通过。