This post is the second of four posts that summarize the results of the Coq Community Survey 2022. Following the first part that focused on who Coq users are, we now cover how people use Coq, such as their Coq version and IDE choice. The third part then covers usage of Coq features, plugins, tools, and libraries. The fourth and last part includes the rest of the results, and the links to the associated research paper and Zenodo artifact.
We invite the Coq community to provide feedback as replies to this post. In particular, we are interested in hearing if something was unclear about survey questions and plots or if you have suggestions for improvements or questions you’d like to see answered with the survey data. For those who prefer, we also welcome feedback in this Zulip topic.
The Coq Community Survey 2022 was an online public survey conducted during February 2022. Its main goal was to get an updated picture of the Coq user community and inform future decisions taken by the Coq team and other Coq ecosystem participants. The survey was available in English and Chinese, and had 109 questions, some of which were only visible depending on answers to previous questions. See the initial post for more detailed information on the survey.
In this summary part, the survey working group looked at the nuts and bolts of how respondents use Coq on a daily (or weekly or yearly) basis, focusing in particular on the software infrastructure: operating systems, package managers, package installation, etc.
Most respondents use Coq on Linux-based operating systems, in particular Debian-derived ones such as Ubuntu, Debian, and Mint. Arch Linux, Fedora and NixOS are also popular. Other Linux distributions reported by several respondents include Gentoo (7), openSUSE (6), Majaro (3), and Void (2). Second in popularity after Linux comes macOS, in particular macOS 12, followed by Windows (mostly 10 or later). Newcomers (defined as respondents who have declared they have used Coq for less than 2 years and less than 1 year ago) are somewhat more likely to use Windows than long-time users (defined as respondents who have declared they have used Coq for more than 5 years). Two respondents report using (or wanting to use) Coq on NetBSD.
Since 2021, the recommended way to install Coq, in particular for beginners, is by using Coq Platform releases. These releases are based on the opam package manager but also provide binaries for most operating systems, e.g., a snap for Linux. However, many respondents opt to use opam directly to install and manage Coq, a method which has been available for many years and continues to be supported.
New Platform releases (including new releases of Coq itself) are made approximately every six months. Most repondents use a recent Coq version (8.13 from January 2021, or a later version). However, many respondents have projects that rely on old Coq versions; these projects are typically not upgraded due to lack of incentives or because of compatibility constraints in project dependencies.
In addition to Coq, respondents may need to install libraries and plugins to build their projects. For this purpose, opam is still the most popular tool, but they also use manual installation, e.g., by downloading Coq code archives from the web, and version control submodules. Among other answers, 4 respondents report having already all the dependencies they need as part of the Coq Platform. Handling dependencies is necessary for continuous integration (CI) of Coq projects, which a significant minority of respondents use. In particular, GitHub Actions is used for CI. Additional results for questions related to CI were reported in a GitHub issue.
The Coq Platform comes with the CoqIDE standalone user interface, and many respondents report that they use CoqIDE. However, Emacs and its ProofGeneral package is slightly more popular, with the VS Code IDE using the VsCoq extension in third place. We provide results also for other interfaces to Coq, namely, Vim, Coqtail, jsCoq, and coq_jupyter. Among the other answers, 3 respondents report having used Coqoon / PIDE, a now unmaintained Eclipse interface.
The survey included additional questions specific to each of the polled user interfaces, whose results were reported in GitHub issues (for CoqIDE, ProofGeneral, Company-Coq, VsCoq, Coqtail, jsCoq, coq_jupyter).
Among other answers to the question “What factors influence your choice of one IDE over another?”, 10 respondents report “ease of use” / “learning curve”, which is not quite the same as “ease of installation” (which was proposed among the pre-defined answers). There are about 9 answers specifying specific features that they need from their IDE. Finally, 4 respondents highlight the need for a stable and mature interface.