Julin S (Dec 07 2021 at 04:01): 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?
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: Oct 13 2024 at 01:02 UTC