CoqPL 2024 (see call for presentations) had a Q/A session with Coq developers (@ejgallego, @ybertot, @rtetley, @mattam82) and the audience in the room. Below are my notes of the questions and answers.
Q: on the rename, why move from “proof assistant” to “(interactive) theorem prover”?
A: this is not a very intentional choice on our part.
Q: I would like to use notations well, but I don’t know how to and the manual is not good enough. Could we have a library of documented/annotated examples of advanced usage?
To everyone: if you have a usage example of Coq notations that you find interesting, could you drop me (Benjamin Pierce) an email?Q: current recommendations for IDEs for Coq? Still CoqIDE or vscode?
A: my (Yves’) take on that is that CoqIDE should be phased out because it is too much of an effort to maintain. vscode or vscodium would be the road to go, I think. We have two experiments on the topic right now.
Q: really happy to see more movement towards sort polymorphism. We have bug reports in Iris due to incompatibilities from different libraries pinning universe levels in incompatible ways. There is another topic that I would like to bring up (Ralf Jung). Every week I run into an issue caused by unification: I want to use apply and it does not work, I have to use rewrite instead. There is no unification on the roadmap. What is the status of that?
A: once we have sort polymorphism, it should be possible to just make the inductives polymorphic in the standard library. It should be.
A: for unification, we have two unification algorithms in Coq, one is used by tactics and another is used by typing, there are incomparable. The idea of unifall is to move everyoen to the one used by typing. It was blocked by this compatibility layer for primitive projects. RIght now I think we could unblock this problem, and go on with the unification of unification.
Q: defining coercions, there is a “uniform inheritance” condition. I stumbled upon a bug report that suggests it has been removed, but I still am getting warning about it.
A: my recollection is that it was made optional as it was too restrictive. You should ask on Zulip.
Q: ecosystem question, in my own project I ended up switching from coq_makefile to Dune. I don’t know if I regret it. I wonder what’s the community opinion on those two approaches. Is there a plan / an opinion on the long term?
A (Emilio): I don’t think there is a position. Make and Dune are really different in the approaches they use. It’s clear to me that Make does not cut it anymore, for large codebases for example. Dune should become the standard build system – but people who want to use Make can still do it. You can save several hours per week by using Dune. I thought we could migrate to Dune in one week (laughs), but it took much longer than expected. I think most users will find Dune better and easier.
A (Tej): I’m still using Makefiles everywhere. I don’t know how to setup a Coq Dune project. For makefiles I copy-paste the standardpp makefile and everything works beautifully. I think it is a matter of documentation.
gasche42Q: there was a change to Coq modules recently that required changing the Dune files quite a bit. Will the interface become stable in the future?
A (Emilio): the config language of Dune is versioned. Once we hit 1.0, it should keep working in the indefinite future.
Q: you mentioned Ltac2. I am looking forward to stop using Ltac1. Something that feels missing to me: my users are using Ltac1 in their proof scripts, and I think between Proof. and Qed. Ltac1 is fine. But then when you try to port something to Ltac2 for automation, you are stuck.
For example “intro patterns”, dealing with a list of intro patterns in Ltac2 is a pain, you keep having to go back to Ltac1 locally, it is annoying. I have seen on the roadmap, “porting ssreflect tactics to Ltac2”, to me that is less of a priority, I would to make it easy to migrate Ltac1 automation to Ltac2. There are too many APIs missing right now.A: I think you should contact Gaëtan with your request about the language.
We want to get in a situation where we forget about Ltac1. Have the proof scripts be nice.Q: I just wanted to say “Thank you”. I am using Coq mainly on Windows, and this has going significantly more painless over the last few years, especially with the Coq platform. Last year there were still some secret steps, but now there are documented and automated better. Thanks!
A: the platform is a bit of a worry in a way, until now it was a one-man project, which is always a bit of a risk. Romain Tetley joined to help Michael Soegstrop. If more people wants to join, it would be great to make it more of a collective effort. The Coq platform should be collaborative, not centered on the Coq core developers. We are going to try to make it happen by documenting as much as possible the inner bits.
Q (Amin): “better support for domain-specific logic”, what is the plan there?
A (Matthieu): have the metalanguage be more flexible in how you can program the elaborator and the tactics. In general we are looking to finetune the application of the Iris tactics for example. We are always interested in this kind of examples.
Q2 (Amin): the Iris proof mode generates very large proof terms. Slow Qed times. Is there anything you could do there to help?
A2: do it more reflectively, maybe?
A2’ (Tej): on Qed I have a trick which is to replace Qed by Admitted during CI. I would love to see this better supported by Coq. Check proofs occasionally.
A3 (Emilio): there is this experimental compiler called FCC which can do that.
An: Ralf: we thought about this hard, but things that should be O(1) are O(n), and we don’t see how to avoid that. We thought about avoiding strings, but nothing we could think of could get rid of that fundamental complexity issue.
Yves: it means we have some work to do as researchers.
Yves: this is the kind of things we are talking about, Iris is a frontrunner, we want to make it easier for Iris and for everyone else.
Q (Gregory): how many people have a real problem with proof term size and type-checking at QED time?
Q: there is a big question and bundling and unbundling, how this affect math classes and all that. Is there work on this, more memoization.
A: we tried hashconsing before and did not work out that well. There is work on introducing “constant with arities”, which avoids let you avoid repeating parameters of a constant, which we plan to look into to avoid redundancy.
Q (Ralf): part of my understand for why typechecking is hard in Coq is that it’s a global imperative step because of global universe levels. I understand that Lean does not that issue. Can we do better?
A (Matthieu): the type-checker is fully functional, the universes are dealt with separately. I don’t think universes are the issue.
Q (François): complexity of the cost of applying of a lemma. If I have a lemma that says (P → P), is the cost of applying it constant, or linear in the size of P? (If I apply this term a lot with the same P, will the result type-check P many times?)
A: yeah, possibly.
Q: can we hear more about the integration of observational type theory in Coq?
A: using the rewrite rules there is a prototype implementation of this by Loïc Pujet and Nicolas Tabareau, a version of OTT working with impredicate Prop. We don’t know yet whether we want to integrate it in the kernel or stick with rewrite rules.
The best exposition is their paper.Q (Gregory): we experimented at Bedrock Systems with fine-tuning term reduction, we think they are really valuable. If you are interested in that, I think we should chat.
A (Matthieu): I know Clément Pit-Claudel is interested in that.
Q: what’s the recommendation on the standard library to use? stdlib?
Q (Bas): what’s the status of SMT integration in Coq?
A (Yves): part of the work on Trakt is to try to do all the translations you would want to be able to use SMT solvers. This specific piece of work is not taken on by the core developers. People we know like Chantal Keller is working on that. We don’t really have a roadmap.
Q (Bas): are there known projects actively using SMT?
A (Yves): not that I know of.