ob-coq provides Org Babel support for evaluating source blocks written in Coq.
Emacs Org Mode is a “major mode for keeping notes, authoring documents, computational notebooks, literate programming, maintaining to-do lists, planning projects, and more…” Like any other markup language, one can embed snippets of source code in Org Mode documents. Unlike other markup languges, however, Org Mode can evaluate those source blocks, passing them input from the Org Mode document itself, collecting their results, and passing those on to other source blocks.
Org Mode ships with support for many languages (C/C++, bash, awk & Python to name just a few). This package provides support for Coq, a proof assistant that provides a dependently-typed functional programming language. As part of the implementation, it also provides inf-coq, a comint-based major mode for interacting with coqtop in an inferior process.
This code is released under the GPL version 3.
ob-coq requires Emacs, Org Mode & Coq.
At present the package is only available as source:
git clone [email protected]:sp1ff/ob-coq.git
cd ob-coq
./bootstrap
./configure
make
make check
sudo make installThe build process does make an Emacs package, so you can also do:
# as above...
make check
make distto produce an Emacs package file (ob-coq-0.0.7.tar) which you can install with package-install-file in your Emacs.
This is early code, something I’ve tried to indicate through the version number (0.0.x). At the time of this writing, it only supports collecting results as output (as opposed to result). This reflects what I see as the primary use case for ob-coq: building Coq developments in Org Mode rather than plain Coq (i.e. .v) files.
Luc Pellissier maintained the original ob-coq under org-contrib. That implementation depended upon coq-inferior.el which used to be part of Coq, but was removed in 2018.
I’m using this package day-in & day-out while I learn Coq and am updating it as I find issues or missing features. Immediate next steps include building-out support for more Org Babel headers as well as hosting tarballs on my personal site. When it matures a bit I’d like to submit it to MELPA. Documentation also needs to be written.
In the meantime, bugs, feature requests & complaints are welcome in the issues, via e-mail or on IRC (I’m sp1ff on Libera.chat, where you can find me in the obvious places such as #emacs or #org-mode).