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.2.tbz
sha256=f891507f58fba3ba29889dd07fbe69af3411d246488ae7595cd81d26c8422f14
sha512=224dfda8fae1ead7a5ae2a8ead527834bb5216b1788485a0c19deade3b0dd86767c19056931294a7973f132680e282c4491c76ef38638c0c566a029379f484e2

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: 12 Jan 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"