Summary
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). SerAPI is a proof-of-concept and should be considered alpha-quality.
Versions
v0.16.1 :: 0/0.16.1 :: gentoo
- Modified
- License
- GPL-3+
- Keywords
- ~amd64
- USE flags
- emacs ocamlopt test
v0.16.0-r1 :: 0/0.16.0 :: gentoo
- Modified
- License
- GPL-3+
- Keywords
- ~amd64
- USE flags
- emacs ocamlopt test
v0.15.0-r3 :: 0/0.15.0 :: gentoo
- Modified
- License
- GPL-3+
- Keywords
- ~amd64
- USE flags
- emacs ocamlopt test
USE flags
General
- emacs
- Add support for GNU Emacs
- ocamlopt
- Enable ocamlopt support (ocaml native code compiler) -- Produces faster programs (Warning: you have to disable/enable it at a global scale)
- test
- Enable dependencies and/or preparations necessary to run tests (usually controlled by FEATURES=test but can be toggled independently)
Dependencies
dev-lang / ocaml : Programming language supporting functional, imperative & object-oriented styles
dev-ml / cmdliner : Declarative definition of command line interfaces for OCaml
dev-ml / dune : A composable build system for OCaml
dev-ml / ppx_compare : Generation of comparison functions from types
dev-ml / ppx_deriving : Type-driven code generation for OCaml
dev-ml / ppx_deriving_yojson : JSON codec generator for OCaml
dev-ml / ppx_hash : PPX rewriter that generates hash functions from type expressions and definitions
dev-ml / ppx_import : A syntax extension for importing declarations from interface files
dev-ml / ppx_sexp_conv : Support Library for type-driven code generators
dev-ml / sexplib : Library for automated conversion of OCaml-values to and from S-expressions
dev-ml / yojson : JSON parsing and pretty-printing library for OCaml
sci-mathematics / coq : Proof assistant written in O'Caml
Runtime Dependencies
dev-lang / ocaml : Programming language supporting functional, imperative & object-oriented styles
dev-ml / cmdliner : Declarative definition of command line interfaces for OCaml
dev-ml / dune : A composable build system for OCaml
dev-ml / ppx_compare : Generation of comparison functions from types
dev-ml / ppx_deriving : Type-driven code generation for OCaml
dev-ml / ppx_deriving_yojson : JSON codec generator for OCaml
dev-ml / ppx_hash : PPX rewriter that generates hash functions from type expressions and definitions
dev-ml / ppx_import : A syntax extension for importing declarations from interface files
dev-ml / ppx_sexp_conv : Support Library for type-driven code generators
dev-ml / sexplib : Library for automated conversion of OCaml-values to and from S-expressions
dev-ml / yojson : JSON parsing and pretty-printing library for OCaml
sci-mathematics / coq : Proof assistant written in O'Caml
Depending packages
sci-mathematics / alectryon : Toolkit for literate programming in Coq
Bugs
- 839102
- sci-mathematics/coq-serapi-0.15.0-r1 - :(.text+<snip>): undefined reference to camlCmdliner_entry
Change logs
- Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
sci-mathematics/coq-serapi: bump to 0.16.1
Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
sci-mathematics/coq-serapi: remove seq dependency
Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
sci-mathematics/coq-serapi: bump to 0.16.0
Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Maciej Barć · gentoo
sci-mathematics/coq-serapi: restrict coq version
Closes: https://bugs.gentoo.org/873604 Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
sci-mathematics/coq-serapi: fix elisp libraries installation
Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
sci-mathematics/coq-serapi: add ppx_sexp_conv version constraints
Signed-off-by: Maciej Barć <xgqt@gentoo.org> - Repository mirror & CI · gentoo
Merge updates from master - Maciej Barć · gentoo
sci-mathematics/coq-serapi: new package; add 0.15.0
Package-Manager: Portage-3.0.30, Repoman-3.0.3 Signed-off-by: Maciej Barć <xgqt@gentoo.org>