Serialization library and protocol for machine interaction with the Coq proof assistant
Description

SerAPI is a library for machine-to-machine interaction with the Coq proof assistant, with particular emphasis on applications in IDEs, code analysis tools, and machine learning. SerAPI provides automatic serialization of Coq's internal OCaml datatypes from/to JSON or S-expressions (sexps).

Install

Documentation github.com Readme Changelog GPL-3.0-or-later License Edit opam file

Published

12 Jan 2023

Authors

Maintainers

Sources

coq-serapi-8.16.0.0.16.2.tbz
sha256=f891507f58fba3ba29889dd07fbe69af3411d246488ae7595cd81d26c8422f14
sha512=224dfda8fae1ead7a5ae2a8ead527834bb5216b1788485a0c19deade3b0dd86767c19056931294a7973f132680e282c4491c76ef38638c0c566a029379f484e2

Dependencies

ppx_deriving_yojson >= "3.4"
yojson >= "1.7.0"
ppx_hash >= "v0.13.0"
ppx_compare >= "v0.13.0"
ppx_sexp_conv >= "v0.13.0"
ppx_deriving >= "4.2.1"
ppx_import build & >= "1.5-3" & < "2.0"
dune >= "2.0.1"
sexplib >= "v0.13.0"
ocamlfind >= "1.8.0"
cmdliner >= "1.1.0"
coq >= "8.16" & < "8.17"
ocaml >= "4.09.0"

Reverse Dependencies

coq-lsp

Conflicts

result < "1.5"