Skip to content

Commit 15da11a

Browse files
authored
a per-target declaration that stays falsifiable (#454)
* a per-target declaration that stays falsifiable `[excluded]` is whole-member, and some members are neither measured-and-broken nor excludable. `cmp-module` RUNS on `x86_64-windows-gnu` and cannot build on `x86_64-linux-gnu`: asio's `detail/config.hpp:899` includes `<linux/version.h>` whenever `__linux__` is defined, OUTSIDE every `ASIO_DISABLE_*` guard, so no configuration macro prevents it. openkal runs on the Linux kernel, so `__linux__` is correct; the uapi headers glibc's userspace installs beside it are not part of what openkal presents. Excluding the member outright would discard a result that is true in order to hide one that is also true. `[not-portable.<member>]` declares one target of one member, with the reason and the evidence. THE BAR IS THAT NO MANIFEST KEY REACHES IT. Upstream source asking in the preprocessor qualifies. A generated configuration header this index writes does not: `curl`'s `linux/tcp.h` is `#define HAVE_LINUX_TCP_H 1` inside `#if defined(__linux__)` in `pkgs/c/compat.curl.lua`, which reads a correct fact about the kernel as a claim about which userspace headers are installed. That is a recipe defect, the same shape as expat's `arc4random_buf`, and it belongs in the recipe. The two were one item in the plan; they are not one thing. THE DECLARATION STAYS FALSIFIABLE. The cell is measured anyway and `compat.py check` FAILS when a declared cell builds: contradicted declaration: cmp-module on x86_64-linux-gnu: declared not-portable and recorded runs -- remove the declaration Measured both ways before it was committed: red on a synthetic result recording `runs`, green on one recording `fails`. A declaration that removes a cell from the figure on the strength of a sentence, and that nothing can contradict, is a permanent excuse; the cost of keeping it honest is a build that was already being paid for. `selftest` gains three legs pinning that the table is read per (member, target) and not per member --- reading it per member is exactly the mistake that would take `cmp-module`'s working Windows cell out of the figure. * curl's two failures have two different causes, and neither is unportability Both are recipe defects. linux `#define HAVE_LINUX_TCP_H 1` inside `#if defined(__linux__)`. The kernel IS Linux, so the predicate is right; reading it as "glibc's userspace headers are installed" is not. The honest test is `__has_include(<linux/tcp.h>)`. The same block also asserts `HAVE_GLIBC_STRERROR_R`, false over musl. windows the recipe's `windows` branch omits HAVE_CONFIG_H so curl_setup.h reaches the checked-in `lib/config-win32.h`, and links `-lws2_32` with Schannel. Over openkal that target presents POSIX and is LP64; config-win32.h is written for LLP64 and the Win32 API. THE SECOND IS THE INTERESTING ONE: the recipe branches on the PLATFORM where the question is about the C ENVIRONMENT. Those two agreed on every target this index had until openkal presented POSIX on Windows, and mcpp has the predicate for the question actually being asked --- `cfg(c-abi = "musl")`. Recorded rather than fixed here: it also needs this index's OpenSSL over the same environment, so it is a larger change than the first.
1 parent 5198b69 commit 15da11a

4 files changed

Lines changed: 130 additions & 4 deletions

File tree

docs/openkal-compat.md

Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -101,6 +101,45 @@ question is about a target rather than the package as a whole.
101101
that cannot be built in any openkal graph, each with its reason; a member that
102102
fails is measured and published, not excluded.
103103

104+
`[not-portable.<member>]` declares one TARGET of one member unbuildable by
105+
construction, with the reason. It exists because `[excluded]` is whole-member
106+
and some members are neither: `cmp-module` runs on `x86_64-windows-gnu` and
107+
cannot build on `x86_64-linux-gnu`, because asio's `detail/config.hpp`
108+
includes `<linux/version.h>` whenever `__linux__` is defined, outside every
109+
`ASIO_DISABLE_*` guard. Excluding the member outright would discard a result
110+
that is true in order to hide one that is also true.
111+
112+
**The bar is that no manifest key reaches it.** Upstream source asking in the
113+
preprocessor qualifies; a generated configuration header this index writes
114+
does not, and belongs in the recipe instead. `curl`'s `linux/tcp.h` is the
115+
second kind — `#define HAVE_LINUX_TCP_H 1` inside `#if defined(__linux__)` in
116+
`pkgs/c/compat.curl.lua`, which reads a correct fact about the kernel as a
117+
claim about which userspace headers are installed.
118+
119+
**The cell is measured anyway, and `compat.py check` fails if it builds.** A
120+
declaration that takes a cell out of the figure on the strength of a sentence
121+
has to stay falsifiable; one that nothing can contradict is a permanent
122+
excuse. The cost is a build that was already being paid for before the
123+
declaration existed.
124+
125+
### curl's two failures have two different causes
126+
127+
Both are recipe defects, and neither is the same defect:
128+
129+
| target | first diagnostic | cause |
130+
| --- | --- | --- |
131+
| `x86_64-linux-gnu` | `lib/setopt.c:31: 'linux/tcp.h' file not found` | `#define HAVE_LINUX_TCP_H 1` inside `#if defined(__linux__)`. The kernel IS Linux, so the predicate is right; what is wrong is reading it as "glibc's userspace headers are installed". The honest test is `__has_include(<linux/tcp.h>)`. The same block also asserts `HAVE_GLIBC_STRERROR_R`, which is false over musl. |
132+
| `x86_64-windows-gnu` | `curl_setup.h:591: "too small curl_off_t"` | The recipe's `windows` branch omits `HAVE_CONFIG_H` so that `curl_setup.h` reaches the checked-in `lib/config-win32.h`, and links `-lws2_32` with Schannel. Over openkal that target presents POSIX and is **LP64**, while `config-win32.h` is written for LLP64 and the Win32 API. |
133+
134+
**The second is the interesting one: the recipe branches on the PLATFORM where
135+
the question is about the C ENVIRONMENT.** Those two agreed on every target
136+
this index had until openkal presented POSIX on Windows, and mcpp has the
137+
predicate for the question actually being asked — `cfg(c-abi = "musl")`
138+
(mcpp docs/22, "Adaptation To The Resolved Target Side"). Selecting the
139+
generated POSIX configuration there, rather than the checked-in Win32 one, is
140+
the shape; it also needs this index's OpenSSL over the same environment, so
141+
it is a larger change than the first and is not folded into it.
142+
104143
## 3. When it runs
105144

106145
`.github/workflows/openkal-compat.yml` runs weekly and on demand, measuring every

docs/zh/openkal-compat.md

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -35,6 +35,23 @@
3535

3636
`tests/openkal/members.toml` 列出测量对象。`[excluded]` 列出在任何 openkal 依赖图中都无法构建的成员,并逐条写明原因;失败的成员照常测量并公布,不列入排除。
3737

38+
`[not-portable.<成员>]` 声明某个成员的**某一个目标**按构造无法构建,并写明理由。它存在是因为 `[excluded]` 是整成员级的,而有些成员两头都不是:`cmp-module``x86_64-windows-gnu` 上 runs,在 `x86_64-linux-gnu` 上建不起来——asio 的 `detail/config.hpp` 只要 `__linux__` 有定义就 include `<linux/version.h>`,而那行在所有 `ASIO_DISABLE_*` 守卫之外。整个排除掉这个成员,等于为了藏起一个真的结果而丢掉另一个同样真的结果。
39+
40+
**门槛是「没有任何清单键伸得进去」。** 上游源码在预处理期发问,算;本索引自己生成的配置头,不算,那属于配方。`curl``linux/tcp.h` 就是后者——`pkgs/c/compat.curl.lua``#if defined(__linux__)` 里写了 `#define HAVE_LINUX_TCP_H 1`,把一个关于内核的正确事实读成了关于「装了哪些 userspace 头」的断言。
41+
42+
**这个格子照常测量,而 `compat.py check` 在它构建成功时会红。** 一条凭一句话把格子移出统计的声明必须保持**可证伪**;没有任何东西能反驳的声明就是一张永久豁免。代价是一次在声明存在之前本来就要付的构建。
43+
44+
### curl 的两条失败是两个不同的真因
45+
46+
两条都是配方缺陷,而且不是同一个缺陷:
47+
48+
| 目标 | 首条诊断 | 真因 |
49+
| --- | --- | --- |
50+
| `x86_64-linux-gnu` | `lib/setopt.c:31: 'linux/tcp.h' file not found` | `#if defined(__linux__)` 里写死了 `#define HAVE_LINUX_TCP_H 1`。内核**确实**是 Linux,谓词没错;错的是把它读成「glibc 的 userspace 头都装好了」。诚实的判据是 `__has_include(<linux/tcp.h>)`。同一个块里还有 `HAVE_GLIBC_STRERROR_R`,在 musl 上它是假的。 |
51+
| `x86_64-windows-gnu` | `curl_setup.h:591: "too small curl_off_t"` | 配方的 `windows` 分支**有意**不定义 `HAVE_CONFIG_H`,好让 `curl_setup.h` 去取仓库里checked-in 的 `lib/config-win32.h`,并链 `-lws2_32` 走 Schannel。而在 openkal 上,那个目标呈现的是 POSIX 且是 **LP64**,`config-win32.h` 写的是 LLP64 与 Win32 API。 |
52+
53+
**第二条才是有意思的那条:配方按「平台」分支,而问题问的是「C 环境」。** 在 openkal 于 Windows 上呈现 POSIX 之前,这两者在本索引的每一个目标上都同答案。mcpp 有那个真正被问的谓词——`cfg(c-abi = "musl")`(mcpp docs/22「按解析出的目标侧适配」)。在那里改选生成的 POSIX 配置而不是 checked-in 的 Win32 配置,就是它的形状;它还需要本索引的 OpenSSL 跑在同一个环境上,所以比第一条大,不与它合并。
54+
3855
## 3. 何时运行
3956

4057
`.github/workflows/openkal-compat.yml` 每周运行、可手动触发,测量全部列出的成员。对 PR,openkal 家族或 `tests/openkal` 变化时测量全部成员,否则测量依赖了被修改描述符的成员。除非启用下文的比较,它不阻止合并。

tests/openkal/compat.py

Lines changed: 57 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -45,7 +45,10 @@
4545
4646
`check` compares a results file with a baseline and fails when a member that
4747
the baseline records as `runs` or `builds` for a target is recorded lower. It
48-
is the regression guard for labels that have been published.
48+
is the regression guard for labels that have been published. It ALSO fails
49+
when a cell declared `[not-portable]` in members.toml built: a declaration
50+
that removes a cell from the figure has to stay falsifiable, or it is a
51+
permanent excuse nothing can contradict.
4952
"""
5053
from __future__ import annotations
5154

@@ -126,6 +129,17 @@ def platform_bound(manifest: dict) -> bool:
126129
return False
127130

128131

132+
def declared_not_portable(decls: dict, member: str, target: str) -> str | None:
133+
"""The reason `members.toml` gives for this (member, target) being
134+
unbuildable by construction, or None.
135+
136+
PER TARGET, NOT PER MEMBER. `[excluded]` already covers a member that
137+
cannot be built in any openkal graph; this covers one that builds on some
138+
targets and cannot on another, where excluding the member outright would
139+
discard a result that is true."""
140+
return ((decls.get(member) or {}).get(target)) or None
141+
142+
129143
def kind_of(manifest: dict, status: str) -> str | None:
130144
"""The platform-relation label for one (member, target) result -- see the
131145
`posix` / `platform` table in this module's docstring, which this
@@ -269,7 +283,12 @@ def cmd_run(args: argparse.Namespace) -> int:
269283
"pins": {k: v for k, v in pins.items() if k in ("runtime", "toolchain", "mcpp")},
270284
"members": {},
271285
"excluded": members_file.get("excluded", {}),
286+
# CARRIED INTO THE RESULTS so the consumer that computes the figure
287+
# can take these cells out of the denominator, and so a reader of the
288+
# results file can see WHY without opening another file.
289+
"not_portable": members_file.get("not-portable", {}),
272290
}
291+
not_portable = members_file.get("not-portable", {})
273292
for member in members:
274293
manifest = load_toml(os.path.join(EXAMPLES, member, "mcpp.toml"))
275294
entry = {"packages": packages_of(manifest),
@@ -284,6 +303,13 @@ def cmd_run(args: argparse.Namespace) -> int:
284303
kind = kind_of(manifest, entry["targets"][target]["status"])
285304
if kind:
286305
entry["targets"][target]["kind"] = kind
306+
# MEASURED ANYWAY. Skipping the build would make the declaration
307+
# unfalsifiable, and the cost is a cell that was going to be
308+
# measured before it was declared.
309+
why = declared_not_portable(not_portable, member, target)
310+
if why:
311+
entry["targets"][target]["declared"] = "not-portable"
312+
entry["targets"][target]["declared_reason"] = why
287313
print(f" {entry['targets'][target]['status']}"
288314
+ (f" ({kind})" if kind else "")
289315
+ (f": {entry['targets'][target].get('diagnostic', '')}"
@@ -312,11 +338,29 @@ def cmd_check(args: argparse.Namespace) -> int:
312338
if got < was:
313339
regressions.append(f"{member} on {target}: {rec['status']} -> "
314340
f"{((now or {}).get('targets', {}).get(target) or {}).get('status', 'absent')}")
341+
# A DECLARATION THAT NOTHING CAN CONTRADICT IS A PERMANENT EXCUSE.
342+
# `[not-portable]` takes a cell out of the figure on the strength of a
343+
# sentence, and the only thing that keeps the sentence honest is failing
344+
# here when the cell builds. The cell is measured for this reason alone.
345+
contradicted = []
346+
decls = load_toml(os.path.join(HERE, "members.toml")).get("not-portable", {})
347+
for member, targets in decls.items():
348+
if args.members and member not in args.members:
349+
continue
350+
for target in targets:
351+
rec = ((current.get("members", {}).get(member) or {})
352+
.get("targets", {}).get(target) or {})
353+
if RANK.get(rec.get("status"), 0) > 0:
354+
contradicted.append(
355+
f"{member} on {target}: declared not-portable and "
356+
f"recorded {rec.get('status')} -- remove the declaration")
315357
for line in regressions:
316358
print(f"regression: {line}")
317-
if not regressions:
318-
print("no published label regressed")
319-
return 1 if regressions else 0
359+
for line in contradicted:
360+
print(f"contradicted declaration: {line}")
361+
if not regressions and not contradicted:
362+
print("no published label regressed, and no declaration was contradicted")
363+
return 1 if (regressions or contradicted) else 0
320364

321365

322366
FAMILY_PREFIXES = ("pkgs/o/openkal", "pkgs/s/std-freestanding-alloc-kal", "tests/openkal/")
@@ -381,6 +425,15 @@ def cmd_selftest(_args: argparse.Namespace) -> int:
381425
classify_failure(ran, True)["status"], "builds"),
382426
("the same output without a runner is not evidence it built",
383427
classify_failure(ran, False)["status"], "fails"),
428+
# `[not-portable]` is per (member, target), and reading it per member
429+
# would take a working cell out of the figure along with the broken
430+
# one --- `cmp-module` runs on x86_64-windows-gnu.
431+
("a declaration is read for the target it names",
432+
declared_not_portable({"m": {"t1": "why"}}, "m", "t1"), "why"),
433+
("and not for a target it does not name",
434+
declared_not_portable({"m": {"t1": "why"}}, "m", "t2"), None),
435+
("nor for another member",
436+
declared_not_portable({"m": {"t1": "why"}}, "n", "t1"), None),
384437
]
385438
bad = 0
386439
for name, got, want in cases:

tests/openkal/members.toml

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,23 @@ curl = "HTTP client, C, sockets"
3636
tinyhttps = "HTTPS client, C++ modules, sockets"
3737
cmp-module = "coroutines, C++ modules"
3838

39+
# A member that cannot be built FOR ONE TARGET by construction, with the reason
40+
# and the evidence. It is measured anyway, and `compat.py check` FAILS if a
41+
# declared cell builds --- a declaration nothing can contradict is a permanent
42+
# excuse, and this project has shipped one of those before.
43+
#
44+
# DISTINCT FROM `[excluded]` BELOW, which is whole-member. `cmp-module` runs on
45+
# `x86_64-windows-gnu`; excluding it would discard a result that is true in
46+
# order to hide one that is also true.
47+
#
48+
# THE BAR IS "NO MANIFEST KEY REACHES IT". A generated configuration header
49+
# this index writes is a RECIPE DEFECT and belongs in the recipe, not here ---
50+
# `curl`'s `linux/tcp.h` is exactly that, `#define HAVE_LINUX_TCP_H 1` inside
51+
# `#if defined(__linux__)` in `pkgs/c/compat.curl.lua`. What qualifies is
52+
# upstream source that asks in the preprocessor where no key can answer.
53+
[not-portable.cmp-module]
54+
x86_64-linux-gnu = "asio's detail/config.hpp:899 includes <linux/version.h> whenever __linux__ is defined, OUTSIDE every ASIO_DISABLE_* guard, so no configuration macro prevents it. openkal runs on the Linux kernel, so __linux__ is correct; the uapi headers glibc's userspace installs beside it are not part of what openkal presents."
55+
3956
# Members that are not measured, each with the reason. A member belongs here
4057
# when it cannot be built in any openkal graph, not when it fails: a failure is
4158
# measured and published.

0 commit comments

Comments
 (0)