Coq Implementors Workshop

When I was a software engineer at Amazon, learning new APIs was easy. I always had experts around who understood those APIs, so if I couldn’t find the answer myself, I could always just ask.

Being a researcher is different. There are very few people who understand the APIs that I work with, and almost all of those people live in France.

Two weeks ago, I had the pleasure of going to the Coq Implementors Workshop in France to work with those people.  It was a lot like being at a software company again, except with better food. In just one day, for example, I was able to update my plugin from Coq 8.6 to Coq 8.8, address two mysterious bugs that had been so confusing I’d left the comment “TODO ask in France” in my code, and eat a three-hour-long French lunch. (Everything was good, but surprisingly, I think my favorite thing was the terrine.)

Here are five things I learned about plugin development at the workshop.

Coq has a Gitter!

Maybe this was obvious, but Coq has a Gitter (kind of like Slack, but linked to Git). While you can probably answer most beginner Coq questions through a quick Google search, and while the coq-club and coqdev mailing lists are great places to ask general questions that you think will benefit a larger audience, the Coq Gitter is perfect for really specific questions about the internal Coq API.

If you’re a plugin developer, it’s pretty much indispensable. I got live support through Gitter when I updated my plugin from 8.6 to 8.8, and it saved me so much time. This means you don’t actually have to go to France to communicate with people who know the APIs you’re using.

Coq developers really want to help plugin developers.

The Coq developers want people developing plugins and contributing to better Coq user experience. The Coq developers also expect to break plugins when they release new versions of Coq. With these things in mind, they are very willing to help developers adapt their plugins to new versions of Coq and understand the APIs that they are interacting with. If the internal API is confusing, feel free to cut an issue in Github and link it to the API documentation meta-issue. The Coq developers would love for you to put your plugin in the Coq CI.

Basically, don’t be shy about being involved with the development community if you’re writing a plugin. The development community wants you to be a part of it. Right now, few enough plugin developers are involved that the Coq developers are not always sure of the best ways to help and to get people involved. If you have ideas, let me know over the next month, because we’re working on putting together a plugin development community.

Coq is not the toy language we often imagine it to be.

People often tell me that writing the kinds of plugins I write is hard. I usually dismiss it as “just writing a compiler.” I still think this is true. You may have a fancy type system, but when you write code that takes in a Gallina term and manipulates it and spits out another Gallina term, you really just have a compiler from Gallina to Gallina. And at the core of my code, there are really just a bunch of functions traversing the AST and updating the environment and constructing new terms. If you’ve ever written a compiler, you can do what I do. A lot of the hard work is already done for you (if you know where in the code to look).

But it turns out the system that I write compilers for is complicated. When we talk about Coq, we often talk about the Calculus of Inductive Constructions (CIC). This is already a gross simplification, because Coq has universes, so it’s closer to CICω (plus a handful of other goodies). And it turns out that while you can usually get away without thinking about universes when you’re writing Coq code, when you actually try to write a plugin, universes always matter. A Coq term these days doesn’t actually mean anything without a corresponding set of universe constraints (currently stored in the evar_map, so-called because it also holds constraints for existential variables).

This can be really confusing when you write a plugin! In my case, I ran into several bugs where I was constructing terms that were well-typed and my plugin almost always worked. But occasionally, I would get universe errors. If I constructed the same term by hand in a Coq file, I wouldn’t get those universe errors. What gives?

I found out that you basically need to always thread your evar_map through your plugin and update it as you go. There’s still a lot that I don’t understand, though, which is why I have an open issue about this.

For example, one of the hardest things to do in a Coq plugin is to define a term. Yves Bertot has an excerpt in his plugin tutorial:

let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook =
 let open EConstr in
 let env = Global.env () in
 let sigma = Evd.minimize_universes sigma in
 let body = to_constr sigma body in
 let tyopt = Option.map (to_constr sigma) tyopt in
 let uvars_fold uvars c =
 Univ.LSet.union uvars (Univops.universes_of_constr env c) in
 let uvars = List.fold_left uvars_fold Univ.LSet.empty
 (Option.List.cons tyopt [body]) in
 let sigma = Evd.restrict_universe_context sigma uvars in
 let univs = Evd.check_univ_decl ~poly sigma udecl in
 let ubinders = Evd.universe_binders sigma in
 let ce = Declare.definition_entry ?types:tyopt ~univs body in
 DeclareDef.declare_definition ident k ce ubinders imps hook

let packed_declare_definition ident value_with_constraints =
 let body, ctx = value_with_constraints in
 let sigma = Evd.from_ctx ctx in
 let k = (Decl_kinds.Global,
 Flags.is_universe_polymorphism(), Decl_kinds.Definition) in
 let udecl = Univdecls.default_univ_decl in
 let nohook = Lemmas.mk_hook (fun _ x -> x) in
 ignore (edeclare ident k ~opaque:false sigma udecl body None [] nohook)

Do you understand that? Me neither, which is why I’m grateful that Yves wrote it. For now the recommendation is to copy and paste this into your plugin code. Hopefully it will become a part of the API at some point, or the API for defining terms will be easier to use. I’ve got an issue open about this one too.

So clearly, some of the difficulty is just a matter of improving the API. But for things like universe constraints, it’s hard to develop an API that abstracts this away from the plugin developer. Ideally you’d like to never think about universe constraints. But they do always matter.

It’s easy to accidentally reinvent the wheel if you can’t find the wheel to begin with.

I have an entire de Bruijn library in both of my plugins. I wrote this library because I had no idea that the Coq code already had de Bruijn management functions. I probably shouldn’t have written it to begin with.

The code base is big. There are a lot of useful functions in there to help you out if you know where to find them. But you probably won’t know where to find them without a little bit of help. And if you find them, you might find that there are several functions that you have access to, each with a slightly different name and signature, and it might not be clear which one you should call.

This is another place where the Coq Gitter can be really useful. I also hope that once we put together a plugin community, we can find a way to share our own library functions that aren’t in the core Coq code. I have a lot of useful higher-order functions for traversing and manipulating terms!

Even the Coq developers disagree on best practices, sometimes.

When Yves first sent out his plugin tutorial, it had a line that did this:

interp_constr (Global.env()) (Evd.from_env (Global.env())) e

I asked if there was any difference between using the global environment and using the current context:

let (env, evm) = Pfedit.get_current_context() in interp_constr env evm e

Well, there is. But which one you should actually use when was the subject of a 15 minute debate on the first day, and then another 15 minute debate another day, and then several disagreements on Gitter.

You should probably know that both of these exist, and that the latter gives you the proof context while the former just gives you all of your global constants and so on. Other than that, I guess when you have a system as complex as Coq, developed by world-class researchers who have come and gone since 1984 (six years before I was born, mind you), not every question you have is going to have an easy answer.

And don’t get me wrong: Any term you produce with a plugin is still ultimately going to go through type-checking, so unless you deliberately try to compromise type-checking, you’re not going to introduce anything bad. If you mess up, your users will just get confusing error messages. Not a huge deal.

But Coq is just code. Even this beautiful CICω-based system is still ultimately just pretty normal software once you look under the hood.  And to be honest, I think that is comforting. There’s no magic.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s