主要观点：

• 讨论了为 OCaml 5 新运行时系统开发属性测试（PBT）的过程及遇到的挑战和经验教训。
• 包括测试隐藏或不可控状态的 API、Cygwin 挑战、保持依赖最小化、在存在错误行为时测试、崩溃对测试运行器的影响、积极/消极/压力测试、误报、隐藏成本、难以重现的问题以及降低multicoretests的准入门槛和在multicoretests之外的使用等方面。

关键信息：

• STM和Lin可用于测试有状态模块接口，但标准库中一些模块状态隐藏或不可控。
• Cygwin 测试套件运行时间长，通过拆分和重新组织工作流解决，还设置了自定义opam仓库。
• 起初依赖ppxlib导致测试阻塞，后消除该依赖。
• 发现错误后继续测试，可调整属性、生成器或禁用测试。
• 测试运行器在 SUT 崩溃时也会崩溃，可通过fork子进程避免。
• 增加了负测试、压力测试等 PBT 变体。
• 存在跨平台行为差异和误报，通过减少误报来提高测试准确性。
• 尽管努力减少误报，但仍有一些问题难以重现。
• 为编译器工程师提供了通过标签运行测试套件的功能，STM的使用已扩展到其他库。

重要细节：

• Ephemeron测试因垃圾回收问题放弃Lin测试，改用STM测试并插入Gc.full_major调用。
• 早期 Cygwin 版本的opam较旧，影响编译器版本测试，通过设置自定义仓库解决。
• ppxlib依赖编译器 AST 导致测试阻塞，后消除依赖。
• 调整测试以避免触发特定错误，如Gc相关测试。
• 利用Util.fork_prop_with_timeout防止测试运行器崩溃。
• 增加了负测试和压力测试以加强对运行时的信心。
• 误报减少，通过分析 CI 工作流结果了解失败情况。
• 一些问题难以重现，如ocaml/ocaml#12707和Gc测试导致的 macOS ARM64 崩溃。
• 通过标签run-multicoretests让编译器工程师方便运行测试套件，该套件已发现多个问题。
• STM的使用已扩展到Saturn和Picos等库，以及 Ortac-QCheck-STM 工具。