coq - 访问 Coq 丰富的类 XML AST 输出

Question

在旧版本的 Coq(< 8.5)中，主要的 coqtop 进程将使用字符串与 IDE 交换数据。

这应该是最近更改的 - 如何查询表示 AST 的更丰富的类似 XML 的结构？

用例:我想以不同的方式解释 Coq 计算的任何内容 - 也就是说，我需要在执行操作(例如调用战术)后以一种我需要解析的非字符串形式的结果。

Answer 1

注意:这个答案已经过编辑以使其保持最新

截至 2018 年底，唯一合理的选择是 SerAPI ，一个支持 Coq 文档全序列化的 Coq 语言服务器。使用 SerAPI，您可以获得任何 Coq 文档或内部结构的完整表示:

$ rlwrap sertop --printer=human
(Add () "Lemma u n : n + 0 = n.")
> (Answer 0 (StmAdded 2 (...) NewTip))
(Query ((sid 2)) Ast)
> (Answer 1(ObjList
>  ((CoqAst
>    (VernacStartTheoremProof Lemma
>     ((((((Id u)) ()))
>       (((LocalRawAssum
>          (((Name (Id n))))
>          (Default Explicit)
>          (CHole () IntroAnonymous ())))
>        (CNotation
>         "_ = _"
>         (((CNotation
>            "_ + _"
>            (((CRef
>               (Ident
>                 (Id n)))
>               ())
>              (CPrim
>               (Numeral (Ser_Bigint 0))))
>             () ()))
>           (CRef
>            (Ident
>              (Id n)))
>            ()))
>          () ()))
>        ())))
>     false)))))

请注意，SerAPI 是实验软件，我是主要作者。