Home

Awesome

Note: Coq SerAPI has now stopped development, the 0.20 release for Coq 8.20 will be the last managed by us. Coq SerAPI has been succeeded by coq-lsp, which solves many longstanding issues and feature requests.

See https://github.com/ejgallego/coq-serapi/issues/252 for more information. The serlib component of this repository now lives in the coq-lsp repository..

We'd like to thanks all the people that have contributed in one way or another to SerAPI after all these years, without you neither SerAPI or coq-lsp would have been possible.

SerAPI: Machine-Friendly, Data-Centric Serialization for Coq

Build Status Zulip

To install with opam:

$ opam install coq-serapi
$ sertop --help

Alternatively, if you use Nix:

$ nix-shell -p coq_8_13 coqPackages_8_13.serapi
$ sertop --help

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. However, it is fully functional and supports, among other things, asynchronous proof checking, full-document parsing, and serialization of Coq's core datatypes. SerAPI can also be run as WebWorker thread, providing a self-contained Coq system inside the browser. Typical load times in Google Chrome are less than a second.

The main design philosophy of SerAPI is to make clients' lives easy, by providing a convenient, robust interface that hides most of the scary details involved in interacting with Coq.

Feedback from Coq users and developers is very welcome and intrinsic to the project. We are open to implementing new features and exploring new use cases.

Documentation and Help:

API WARNING: The protocol is experimental and may change often.

Quick Overview and Install:

SerAPI can be installed as the OPAM package coq-serapi or the Nix package coqPackages_8_13.serapi. See build instructions for manual installation. The experimental in-browser version is also online.

SerAPI provides an interactive "Read-Print-Eval-Loop" sertop, a batch-oriented compiler sercomp, and a batch-oriented tokenizer sertok. See the manual pages and --help pages of each command for more details.

To get familiar with SerAPI we recommend launching the sertop REPL, as it provides a reasonably human-friendly experience:

$ rlwrap sertop --printer=human

You can then input commands. Ctrl-C will interrupt a busy Coq process in the same way it interrupts coqtop.

The program sercomp provides a command-line interface to some key functionality of SerAPI and can be used for batch processing of Coq documents, e.g., to serialize Coq source files from/to lists of S-expressions of Coq vernacular sentences. See sercomp --help for some usage examples and an overview of the main options. The program sertok provides similar functionality at the level of Coq source file tokens.

Protocol Commands:

Interaction with sertop is done using commands, which can be optionally tagged in the form of (tag cmd); otherwise, an automatic tag will be assigned. For every command, SerAPI will always reply with (Answer tag Ack) to indicate that the command was successfully parsed and delivered to Coq, or with a SexpError if parsing failed.

There are three categories of commands:

Roadmap and Developer organization:

SerAPI is organized in branches corresponding to upstream Coq versions; usually, branch v8.XX is compatible with Coq 8.XX, and corresponds to SerAPI 0.XX. These branches are stable and can be relied upon.

The branch main tracks Coq master branch, and it is not a stable branch; force pushes and random rebases can happen there; handle with care!

We are working on fixing this problematic setup, which is that way as in the past such branch used to be "private", but now that SerAPI is in Coq's CI the development workflow has changed, with developer submitting PRs to it.

These days, most work related to SerAPI is directly happening over Coq's upstream itself. The main objective is to improve the proof-document model; building a rich query language will be next. See the roadmap issue in our bug tracker for more information about roadmap and the Developer Information section for more details on the development setup.

Clients and Users:

SerAPI has been used in a few contexts already, we provide a few pointers here, feel free to add your own!

Quick Demo (not always up to date):

$ rlwrap sertop --printer=human
(Add () "Lemma addn0 n : n + 0 = n. Proof. now induction n. Qed.")
  > (Answer 0 Ack)
  > (Answer 0 (Added 2 ((fname "") (line_nb 1) (bol_pos 0) (line_nb_last 1) (bol_pos_last 0) (bp 0) (ep 26))
  >            NewTip))
  > ...
  > (Answer 0 (Added 5 ... NewTip))
  > (Answer 0 Completed)

(Exec 5)
  > (Answer 1 Ack)
  > (Feedback ((id 5) (route 0) (contents (ProcessingIn master))))
  > ...
  > (Feedback ((id 5) (route 0) (contents Processed)))
  > (Answer 1 Completed)

(Query ((sid 3)) Goals)
  > (Answer 2 Ack)
  > (Answer 2
  >  (ObjList ((CoqGoal ((fg_goals (((name 5) (ty (App (Ind ...))))
                         (bg_goals ()) (shelved_goals ()) (given_up_goals ()))))))
  > (Answer 2 Completed)

(Query ((sid 3) (pp ((pp_format PpStr)))) Goals)
  > (Answer 3 Ack)
  > (Answer 3 (ObjList ((CoqString
  >   "\
  >    \n  n : nat\
  >    \n============================\
  >    \nn + 0 = n"))))
  > (Answer 3 Completed)

(Query ((sid 4)) Ast)
  > (Answer 4 Ack)
  > (Answer 4 (ObjList ((CoqAst ((((fname "") (line_nb 1) (bol_pos 0) (line_nb_last 1)
  >                                (bol_pos_last 0) (bp 34) (ep 50)))
  > ...
  >            ((Tacexp
  >              (TacAtom
  >                (TacInductionDestruct true false
  > ...
  > (Answer 4 Completed)

(pp_ex (Print ((sid 4) (pp ((pp_format PpStr)))) (CoqConstr (App (Rel 0) ((Rel 0))))))
  > (Answer pp_ex Ack)
  > (Answer pp_ex(ObjList((CoqString"(_UNBOUND_REL_0 _UNBOUND_REL_0)"))))

(Query () (Vernac "Print nat. "))
  > (Answer 6 Ack)
  > (Feedback ((id 5) (route 0) (contents
  >    (Message Notice ()
  >    ((Pp_box (Pp_hovbox 0) ...)
  > (Answer 6 (ObjList ()))
  > (Answer 6 Completed)

(Query () (Definition nat))
  > (Answer 7 Ack)
  > (Answer 7 (ObjList ((CoqMInd (Mutind ....)))))
  > (Answer 7 Completed)

Technical Report:

There is a brief technical report describing the motivation, design, and implementation of SerAPI. If you are using SerAPI in a project, please cite the technical report in any related publications:

@techreport{GallegoArias2016SerAPI,
  title = {{SerAPI: Machine-Friendly, Data-Centric Serialization for Coq}},
  author = {Gallego Arias, Emilio Jes{\'u}s},
  url = {https://hal-mines-paristech.archives-ouvertes.fr/hal-01384408},
  institution = {MINES ParisTech},
  year = {2016},
  month = Oct,
}

Developer Information

Technical Details

SerAPI has four main components:

Building your own toplevels using serlib and serapi is encouraged.

Advanced Use Cases

With a bit more development effort, you can also:

We would also like to provide a Jupyter/IPython kernel.

Developer/Users Mailing List

SerAPI development is mainly discussed on GitHub and in the Gitter channel. You can also use the jsCoq mailing list by subscribing at: https://x80.org/cgi-bin/mailman/listinfo/jscoq

The mailing list archives should also be available at the Gmane group: gmane.science.mathematics.logic.coq.jscoq. You can post to the list using nntp.

Acknowledgments

SerAPI has been developed at the Centre de Recherche en Informatique of MINES ParisTech (former École de Mines de Paris) and was partially supported by the FEEVER project.