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.17.0.0.17.0.tbz
sha256=fe717f2aa1394434ca3cd9f02a4227e512fb2517c01d4f2726d71f4e3a18756d
sha512=c070d3ebb7f76df7929b04ddb68d4d28751e8991fdb870f56a64168389ff217e75e118317dc8069a8acf98ac88c523d2211fd91fdc777f916d3184b56d235a7c

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: 03 Apr 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 >= "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.17" & < "8.18"
  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"