Stream: Coq users

Topic: Tools to parse coq documents


view this post on Zulip Julin S (Dec 07 2021 at 04:01):

Are there any libraries in any programming languages that can parse coq documents? I heard of pycoq that seems to getting ready. Are there others?
I guess metacoq is also a way?

view this post on Zulip Karl Palmskog (Dec 07 2021 at 08:58):

you can access Coq's lexer/parser through Coq's OCaml interface. This is what SerAPI does, but it also allows you to get serialized machine-readable data out from the lexer/parser: https://github.com/ejgallego/coq-serapi/

If you want to interact with Coq through a tool, including sending source code snippets that get parsed/processed, you can use SerAPI's protocol. See the #SerAPI stream.


Last updated: Feb 08 2023 at 23:03 UTC