推荐使用Coq SerAPI：智能、数据驱动的Coq序列化库

请注意：Coq SerAPI已停止开发，0.20版本（针对Coq 8.20）将是最后一个由我们管理的版本。Coq SerAPI已被coq-lsp所替代，它解决了许多长期存在的问题和功能请求。有关更多信息，请查看此问题，以及serlib现在在新仓库中的情况。

---

Coq SerAPI：面向机器的友好型Coq数据序列化工具

要通过opam安装：

$ opam install coq-serapi
$ sertop --help

或者，如果你使用Nix：

$ nix-shell -p coq_8_13 coqPackages_8_13.serapi
$ sertop --help

Coq SerAPI是一个用于Coq证明助手与机器之间交互的库，特别强调IDE、代码分析工具和机器学习场景的应用。它提供了从/to JSON或S表达式（sexps）自动序列化Coq内部OCaml数据类型的功能。

尽管处于实验阶段，被认为是α质量，但SerAPI完全可用，支持异步证明检查、完整文档解析和Coq核心数据类型的序列化。此外，它还可以作为WebWorker线程运行，提供浏览器内的自包含Coq系统，加载时间在Google Chrome中通常少于一秒。

SerAPI的主要设计哲学是让客户端生活更轻松，通过提供一个方便、健壮的接口，隐藏与Coq交互时的复杂细节。

欢迎所有Coq用户和开发者提供反馈，并参与项目的内在发展。

文档和支持：

• 协议文档
• 接口文件
• SerAPI常见问题解答
• 技术报告
• 问题反馈系统
• Zulip聊天
• Gitter聊天室（遗留）
• 邮件列表

API警告：该协议处于实验阶段，可能会经常更改。

快速入门和安装：

SerAPI可以通过OPAM包coq-serapi或Nix包coqPackages_8_13.serapi进行安装。如需手动安装，请参阅构建说明。在线的实验性在浏览器版本也可供使用。

SerAPI提供了交互式的"读-打印-评估-循环"（sertop）、批处理编译器（sercomp）和批处理词法分析器（sertok）。每个命令的--help页面和手册页有更多详细信息。

熟悉SerAPI的好方法是启动sertop REPL，因为它提供了一个相对人性化友好的体验：

$ rlwrap sertop --printer=human

你可以输入命令，Ctrl-C将像中断coqtop一样中断繁忙的Coq进程。

程序sercomp为SerAPI的关键功能提供了命令行接口，可用于Coq源文件的批量处理，例如，将Coq源文件从/to Coq语句的S表达式列表中序列化和反序列化。更多信息和使用示例，见sercomp --help。程序sertok在Coq源文件令牌级别提供了类似的功能。

协议命令：

与sertop的交互通过命令进行，可选地以(tag cmd)形式标记；否则，会自动分配标签。对于每个命令，SerAPI 总会回复(Answer tag Ack)表示命令成功解析并交付给Coq，或当解析失败时回复SexpError。

存在三种类别的命令：

1. 文档操作：Add, Cancel, Exec, ... 这些命令指示Coq对当前文档执行某些操作。 每个命令都会产生零个或多个不同的tagged回答，最后的回答(Answer tag Completed)表明不会有更多的输出。

2. 查询：(Query ((opt value) ...) kind)：

   查询指定类型的Coq对象。范围包括选项、目标和假设、战术等。第一个参数是一系列选项：preds是组合过滤器列表，limit指定返回值的数量，pp控制输出格式：PpSer为全序列化，或PpStr为“漂亮打印”。

3. 打印：(Print opts obj): 提供访问Coq打印机的方法。主要用于打印（可能由IDE操纵）由Query返回的对象。

发展路线图和开发者组织：

SerAPI按上游Coq版本分支进行组织；通常，分支v8.XX与Coq 8.XX兼容，对应SerAPI 0.XX。这些分支是稳定的，可以依赖。

main分支跟踪Coq的master分支，不稳定，可能存在强制推送和随机重基。现在，由于开发者直接向其提交PR，开发流程已经改变，这导致了这种情况。目前，大部分与SerAPI相关的工作直接在Coq的上游仓库中进行。主要目标是改进证明文档模型，接下来将建立丰富的查询语言。查看我们在问题反馈系统中的路线图问题获取更多信息。

客户端和使用者：

SerAPI已经在一些场景下得到应用，以下是一些建议，欢迎您添加自己的！

• jsCoq使您可以在浏览器中运行Coq。jsCoq是SerAPI的前身，即将完全基于SerAPI。
• mCoq是一个基于SerAPI的变异分析工具。
• elcoq，Clément Pit-Claudel的emacs技术演示，虽然不完全功能，但展示了SerAPI的一些值得注意的特点。
• PeaCoq，一个Coq IDE的浏览器版，有一个实验性的SerAPI分支。
• GrammaTech的软件进化库（SEL）提供了用于程序修改和评估软件的工具。其Coq模块使用SerAPI将Coq源代码序列化为AST，然后解析成Common Lisp对象以进行进一步操作。
• CoqGym，一个基于Coq的定理证明学习环境，使用SerAPI与Coq交互和进行特征提取。

---

尽管Coq SerAPI的发展已转移到其他项目，但其历史影响和在Coq生态系统中的贡献不容忽视。如果你的项目需要与Coq深度集成，尤其是考虑到未来的稳定性和发展，那么Coq-lsp可能是你的最佳选择。然而，在过渡期间，理解SerAPI的工作原理和技术仍可能对现有项目有所帮助。