coq-serapi
  1. Overview
  2. Docs
Serialization library and protocol for machine interaction with the Coq proof assistant

Install

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

Authors

  1. E
    Emilio Jesús Gallego Arias
  2. K
    Karl Palmskog
  3. C
    Clément Pit-Claudel
  4. K
    Kaiyu Yang

Maintainers

  1. E
    e@x80.org

Sources

coq-serapi-8.16.0.0.16.3.tbz
sha256=66137df53e01398a26e9e51056af7439997bcf562fbe4503946fe89e0c5df443
sha512=5c71f7acd4537c33853122d9c526e61f35d2934504c77ce95196f8d595f1c619a680fccd46ba9deb69b509eeb936984056380b18b65fae617ae1cce704df90a1

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).

Published: 20 Feb 2023

Dependencies (13)

  1. ppx_deriving_yojson >= "3.4"
  2. yojson >= "1.7.0"
  3. ppx_hash >= "v0.13.0"
  4. ppx_compare >= "v0.13.0"
  5. ppx_sexp_conv >= "v0.13.0" & < "v0.16.0"
  6. ppx_deriving >= "4.2.1"
  7. ppx_import build & >= "1.5-3" & < "2.0"
  8. dune >= "2.0.1"
  9. sexplib >= "v0.13.0"
  10. ocamlfind >= "1.8.0"
  11. cmdliner >= "1.1.0"
  12. coq >= "8.16" & < "8.17"
  13. ocaml >= "4.09.0"

Dev Dependencies

None

Used by (1)

  1. coq-lsp < "0.1.6.1+8.17"

Conflicts (1)

  1. result < "1.5"