Luna Flow
简体中文

internal/conformance 设计

设计目标

四个语料前端针对截然不同的数据（十进制行、区间语句、MPFR 行、TestFloat 向量）报告结果，而 Python 工具链会跨进程汇总这些结果。它们必须对”用例”、“通过”、“跳过”和”分片”的含义达成一致，否则公布的总数将无法相互比较。internal/conformance 一次性确定了这套术语：每个用例一种处置结果、具有固定恒等式的计数器，以及一条分片规则。

数学背景

结果与计数器

一个结果是四元组 (id,δ,π,m)(\mathit{id}, \delta, \pi, m)，其中处置结果 δ∈{E,D,L,U}\delta \in \{\mathsf{E}, \mathsf{D}, \mathsf{L}, \mathsf{U}\}（可执行、诊断、遗留、不支持），通过位为 π\pi，消息为 mm。对于结果列表 RR，定义计数向量

c(R)=∑r∈R{eexec+epassδ=E, π,eexec+efailδ=E, ¬π,eskip+eδδ∈{D,L,U},selected(R)=∣R∣,c(R) = \sum_{r \in R} \begin{cases} e_{\text{exec}} + e_{\text{pass}} & \delta = \mathsf{E},\ \pi,\\ e_{\text{exec}} + e_{\text{fail}} & \delta = \mathsf{E},\ \neg\pi,\\ e_{\text{skip}} + e_{\delta} & \delta \in \{\mathsf{D}, \mathsf{L}, \mathsf{U}\}, \end{cases} \qquad \text{selected}(R) = |R| ,

其中各 ee 是 N7\mathbb{N}^{7} 中的单位向量。RunSummary::from_results 精确地计算 c(R)c(R) 和 ∣R∣|R|，并存储调用者给出的总数 TT。

分片

对于 n≥1n \ge 1 和 0≤i<n0 \le i < n，分片 (n,i)(n, i) 选取序号集合 Si={k∈N:k mod n=i}S_i = \{ k \in \mathbb{N} : k \bmod n = i \}。

设计决策

四种处置结果，一种失败概念

只有可执行的结果才可能失败。区分诊断、遗留和不支持这三类跳过，使报告能够说明为什么某些行没有运行：诊断行不是测试（不损失任何结论），不支持的行是缺失的功能（损失一项结论），遗留行遵循已废弃的约定。success() 的含义是”没有可执行用例失败”；更严格的判定由调用者在其上叠加（ITL 前端在出现诊断时也判失败，各 CLI 可选择在出现不支持的行时判失败）。

轮转分片

将序号 kk 分配给分片 k mod nk \bmod n 无需知道总数，可以在流式处理中决定，并能将相邻的（往往代价相近的）用例分散到各个分片中。校验（try_new）与使用相分离，因此 selects 只是一次比较。

total 由外部提供，merge 取最大值

分片前的用例数由调用者知道，而不是由某个分片的结果列表知道。一次运行的每个分片都报告相同的总数 TT，因此无论分成多少部分，merge 中取最大值都返回 TT，而求和则会把它计算 nn 次。

从 1 开始的位置

SourceLocation 将行号和列号限制为至少为 1，因此格式化后的诊断（file:line:column: message）始终是有效的编辑器位置，即使调用者传入 0 表示”未知”也是如此。

正确性 / 不变式

计数恒等式。 对于每个汇总，selected=executable+skipped\text{selected} = \text{executable} + \text{skipped}，executable=passed+failed\text{executable} = \text{passed} + \text{failed}，且 skipped=diagnostic+legacy+unsupported\text{skipped} = \text{diagnostic} + \text{legacy} + \text{unsupported}。c(R)c(R) 的每个加项恰好在每个恒等式的一侧加 1，因此这些恒等式对 from_results 成立；merge 按分量相加计数器，从而保持线性恒等式。

分片划分序号。 每个 kk 模 nn 恰有一个余数，因此各 SiS_i 互不相交且覆盖 N\mathbb{N}。在前 NN 个序号中，分片 ii 分得

∣Si∩{0,…,N−1}∣=⌈N−in⌉,|S_i \cap \{0, \dots, N-1\}| = \left\lceil \frac{N - i}{n} \right\rceil ,

因此各分片大小至多相差一。

合并分片得到串行计数。 cc 是从（以拼接为运算的）列表到 (N7,+)(\mathbb{N}^7, +) 的幺半群同态：c(R+ ⁣ ⁣+R′)=c(R)+c(R′)c(R \mathbin{+\!\!+} R') = c(R) + c(R')，同样 ∣R+ ⁣ ⁣+R′∣=∣R∣+∣R′∣|R \mathbin{+\!\!+} R'| = |R| + |R'|。若各分片的结果就是串行运行的结果在 S0,…,Sn−1S_0, \dots, S_{n-1} 上的限制（只要一个用例的结果不依赖于其他用例，这就成立），则

merge⁡(fr(T,R∣S0),…,fr(T,R∣Sn−1)) and fr(T,R)\operatorname{merge}\bigl(\mathrm{fr}(T, R|_{S_0}), \dots, \mathrm{fr}(T, R|_{S_{n-1}})\bigr) \text{ and } \mathrm{fr}(T, R)

具有相等的计数器和相等的总数；只有结果列表的顺序不同（按分片分组）。

不可变性。 汇总在构造时和调用 results() 时都会复制结果数组，因此调用者事后无法修改汇总。

被否决的替代方案

  • 单一的”跳过”计数器。 这会掩盖非测试与缺失功能之间的区别，而这恰恰是符合性声明必须说明的。
  • 连续分片。 这需要事先知道总数，并会把代价高的文件集中到一个分片中。
  • 前端公开使用这些类型。 前端改为对它们进行包装，因此本包可以演进而不破坏已发布的 API。

边界

  • 不解析语料，不执行，不做 IO，不处理 JSON：这些属于各前端和 internal/runner_cli。
  • 不提供计时或性能数据。
  • 不检查结果的 passed 位是否与其处置结果一致。
  • 内部包：不能在 Luna-Flow/floating 之外导入，不提供稳定性承诺。