nixpkgs 的圣杯：用 SAT/ASP 求解器给无版本包管理器加上版本范围

概述

fzakaria 在 nixpkgs-multiverse（nixpkgs 历史版本的并集，30.9 万个包版本、1541 个 nixos-unstable 修订、几乎全可缓存命中）基础上推出 grail：给「版本号是单一、无版本范围」的 Nixpkgs 加上版本范围求解能力。Nixpkgs 历来每个属性只有一个版本，因而无需、也没有依赖求解器；一旦 multiverse 把所有版本「去删除」回来，选择就成真问题——范围求解是布尔可满足性（SAT，NP-hard）。grail 借鉴 Spack 的 spec 语言：@ 后接范围、^ 串联共存组（须在同一修订解析）、|| 或、逗号逻辑与；支持 >=<=、.x/.* 前缀、.. 闭区间，还支持日期范围与 glibc 时代。底层用 ASP（Answer Set Programming / clingo）编码事实与约束：每个 spec 恰好选一个允许版本、每个共存组停在某个候选修订、并杀掉让成员不在其组修订存活的模型；策略上先最小化修订数、再最大化新版本、再最小化 glibc 时代。grail lock 写出与 mvs 同格式的 lock 文件，甚至可在 derivation 里直接写 specs，让 clingo 在沙箱内求解、经 import-from-derivation 物化 nixpkgs，全程可被 nixpkgs-multiverse 索引的缓存命中。对 libc 兼容用 .gnu.version_r 的 GLIBC_2.x 需求做成事实让求解器回溯混用。