Ann: ob-coq
I've pushed first code for ob-coq: Org Babel support for Coq.
Coq is a proof assistant. It provides a functional language based on the typed lambda calculus expressive enough to describe both proofs and programs, in which proof validation becomes type checking. You can do really cool things with it, like write programs whose type contains a proof of their correctness, then extract the computational portion of the program to an industrial FP language. Stephen Boyer has a nice tutorial here as part of a suite of Coq "developments"– bodies of proofs & programs concerning some problem area.
Org Mode has been described as Emacs' "killer app"; the thing that entices even non-programmers onto Emacs. I wrote about it a bit here. One of its (many) features is Babel– the ability to not merely embed code fragments in one's markup, but to evaluate them. This opens up the possibility of creating "live" notebooks as well as literate programming.
In particular, to me, it suggested a much nicer environment for building Coq developments:
- write them up in Org mode, taking advantage of Org's markup, support for cross-references, \(LaTeX\) and so on
- use Org Babel to evaluate the Coq code I was writing
- use Org mode's literate programming features to produce the final Coq
.vfiles
Now, there is some prior art in this area. There was an original ob-coq.el in the org-contrib repo, along with a request for a maintainer. I took a look, but it seems incomplete, and, fatally, depends upon the package inferior-coq.el. This was once distributed with Coq itself, but was removed back in 2018 (in commit 41d597866d4f79fe5109c25c6f5cc57d0ebf7f0f).
So, I decided to write a new ob-coq. Given that the Coq project seemed to have gotten out of the "inferior Coq" business in the abovementioned commit, I wrote my own (Mastering Emacs has a nice writeup on the comint package, Emacs' "command interpreter" base, by the way):
Org Babel support for individual languages takes the form of language-specific back-ends. Armed with my new command interpreter and ob-template.el, I got some first code working for a Coq back-end:
It's early days (version 0.0.2 at the time of this writing), but I am using it day-in & day-out for taking notes & generally working with Coq. One major feature I'm missing is handling the "result" source block header. When evaluating source code, Org Mode needs to know how to handle the results. The author expresses this in the :results source block header argument. When specifying "output", Org simply reports whatever's on stdout, or whatever comes back from the interpreter. The other possible setting is "result", by which the author asks Org Mode to interpret the output as an Emacs Lisp variable, presumably for subsequent use in another code block. Thing is, I'm not really sure what that would even mean in the case of Coq. I can imagine, if not at the moment name, an exotic use case in which Coq would be a natural choice for some sort of calculation, but its primary application is construction (it's based on the Calculus of Inductive Constructions, after all). That is to say, the point of Coq is primarily writing down terms that type check, not executing them.
Regardless, if there are any other users of both Org Mode and Coq out there, take a look; complaints, criticisms & suggestions welcome at sp1ff@pobox.com, @sp1ff on IRC. or in the issues.
04/10/24 11:07