The purpose of this survey is to get a better understanding of the Coq community, how people use Coq and to get input to inform future decisions. We warmly encourage anyone interested to participate, whether you're an experienced or casual Coq user, a learner or a prospective user. Your data will be treated anonymously.
The multiple choice part of this survey takes about 30 minutes to fully complete. Your participation is still helpful even if you don't answer every question. Answer the questions in any order you wish; feel free to answer first the questions that are most important to you. You can navigate through the section list using the menu on the top right. You can save and later resume a partially completed survey. However, you must eventually press the "Submit" button in the last section so we receive your answers. The survey will be available until February 28, 2022 (Anywhere On Earth). Don’t forget to submit your answers by then!
Inria is committed to protecting personal data in accordance with the General Data Protection Regulation (GDPR). Inria uses this survey for the purpose described above, on the legal basis of consent.
The recipients of these data are the members of the Coq Community Survey Working Group who are located in the European Union. These data will be kept for one year and will not be transferred outside the European Union (aggregated data, which do not constitute personal data anymore, will be shared publicly with the Coq community). This data collection is voluntary and does not involve automated decision-making.
You can access your data, request their deletion, and exercise your rights of opposition, rectification and limitation of data processing. To exercise these rights or for any questions about the processing of your data, you can contact the DPO via dpo@inria.fr. However, if you believe that your rights are not respected or that the processing of your data is not compliant, you can submit a complaint to the CNIL.
There are 109 questions in this survey.
We are collecting a list of universities teaching Coq on this wiki page: https://github.com/coq/coq/wiki/Universities-teaching-Coq
We encourage you to edit it to add links to any course using Coq that you teach, that you have taken as a student, or that you are aware of.
What's the trend in Coq use in your workplace or team?
make install
) Warning: because of a survey software bug, you should avoid reloading this page after having started to answer any questions. For example, you should not click the "Previous" button or navigate to it from the menu, or use the "Resume later" feature on this page. In case the page is reloaded, you may lose some of your answers.
The bug only affects dual scale arrays (which are used on this page and nowhere else in the survey) and only triggers when reloading the page. Hence, as long as you answer all the questions on this page in one go and do not come back to it afterward, you should not be affected.
If you were planning to use the "Resume later" feature soon, we strongly recommend doing so before starting to answer the questions on this page.
Thank you for your understanding!
For each of the following questions, we ask you if you are planning to use or have already used the listed features, libraries and tools, and if it would be hard or impossible to do without them.
Skip any item that you do not know about or don't (plan to) use, leaving "No answer" selected, and skip the second column ("Importance") for any items that are not critical to your work.
In case you accidentally select something, clicking on "No answer" will reset your answers for both columns of a given item.
Usage | Importance | |||||
---|---|---|---|---|---|---|
Advanced user | Casual user | Plan to use | Impossible to do without | Hard to do without | ||
The standard tactics | ||||||
SSReflect |
Usage | Importance | |||||
---|---|---|---|---|---|---|
Advanced user | Casual user | Plan to use | Impossible to do without | Hard to do without | ||
Ltac | ||||||
Ltac2 | ||||||
Mtac2 | ||||||
MetaCoq | ||||||
Coq-Elpi |
Usage | Importance | |||||
---|---|---|---|---|---|---|
Advanced user | Casual user | Plan to use | Impossible to do without | Hard to do without | ||
Inductive types | ||||||
Universe polymorphism | ||||||
Cumulative inductive types | ||||||
Coinductive types | ||||||
SProp | ||||||
-type-in-type command-line option, the Universe Checking flag or the bypass_check(universes) attribute |
||||||
The -indices-matter command-line option |
||||||
Modules | ||||||
Module types (functors) | ||||||
Typeclasses | ||||||
Canonical structures | ||||||
Primitive integers | ||||||
Primitive floats | ||||||
Primitive arrays |
Usage | Importance | |||||
---|---|---|---|---|---|---|
Advanced user | Casual user | Plan to use | Impossible to do without | Hard to do without | ||
Bignums | ||||||
Coqdoc | ||||||
coq_makefile | ||||||
Equations | ||||||
Function | ||||||
Micromega (lia , nia , lra , nra , zify ) |
||||||
Nsatz | ||||||
Program | ||||||
Ring (ring , ring_simplify , field ) |
||||||
Solvers for logic and equality (tauto , intuition , congruence , firstorder ) |
Usage | Importance | |||||
---|---|---|---|---|---|---|
Advanced user | Casual user | Plan to use | Impossible to do without | Hard to do without | ||
AAC Tactics | ||||||
Alectryon | ||||||
CompCert | ||||||
coq-dpdgraph | ||||||
CoqHammer | ||||||
Dune | ||||||
Hierarchy Builder | ||||||
Interval | ||||||
Ott | ||||||
Paco | ||||||
Paramcoq | ||||||
PyCoq | ||||||
QuickChick | ||||||
SerAPI | ||||||
SMTCoq | ||||||
Unicoq |
Usage | Importance | |||||
---|---|---|---|---|---|---|
Advanced user | Casual user | Plan to use | Impossible to do without | Hard to do without | ||
Coq-ExtLib | ||||||
Coq-std++ | ||||||
Math Classes | ||||||
Mathematical Components | ||||||
TLC |
Usage | Importance | |||||
---|---|---|---|---|---|---|
Advanced user | Casual user | Plan to use | Impossible to do without | Hard to do without | ||
mathcomp-ssreflect | ||||||
mathcomp-algebra | ||||||
mathcomp-fingroup | ||||||
mathcomp-field | ||||||
mathcomp-character | ||||||
mathcomp-solvable | ||||||
mathcomp-zify | ||||||
mathcomp-finmap | ||||||
mathcomp-multinomials | ||||||
mathcomp-real-closed | ||||||
mathcomp-analysis | ||||||
infotheo |
Usage | Importance | |||||
---|---|---|---|---|---|---|
Advanced user | Casual user | Plan to use | Impossible to do without | Hard to do without | ||
CoLoR | ||||||
CoqEAL | ||||||
Coquelicot | ||||||
CoRN | ||||||
Fiat Crypto | ||||||
Flocq | ||||||
HoTT | ||||||
Iris | ||||||
UniMath | ||||||
Verified Software Toolchain |
Usage | Importance | |||||
---|---|---|---|---|---|---|
Advanced user | Casual user | Plan to use | Impossible to do without | Hard to do without | ||
Logic: Classical logic, dependent equality, extensionality, choice axioms | ||||||
Structures: Algebraic structures (types with equality, with order, ...) | ||||||
Bool: Booleans (basic functions and results) | ||||||
Arith: Basic Peano arithmetic | ||||||
PArith: Binary positive integers | ||||||
NArith: Binary natural numbers | ||||||
ZArith: Binary integers | ||||||
QArith: Rational numbers | ||||||
Numbers: An experimental modular architecture for arithmetic | ||||||
Relations: Relations (definitions and basic results) | ||||||
Sets: Sets (classical, constructive, finite, infinite, powerset, etc.) | ||||||
Classes | ||||||
Lists: Polymorphic lists | ||||||
Streams: Infinite sequences | ||||||
Vectors: Dependent datastructures storing their length | ||||||
Sorting: Axiomatizations of sorts | ||||||
Wellfounded: Well-founded Relations | ||||||
MSets: Modular implementation of finite sets using lists or efficient trees, modernizing FSets | ||||||
FSets: Modular implementation of finite sets and maps using lists or efficient trees | ||||||
Strings: Implementation of strings as list of ASCII characters | ||||||
Reals: Formalization of real numbers | ||||||
Array: Persistent native arrays |
Usage | Importance | |||||
---|---|---|---|---|---|---|
Advanced user | Casual user | Plan to use | Impossible to do without | Hard to do without | ||
OCaml | ||||||
Haskell | ||||||
Scheme | ||||||
JSON |
Usage | Importance | |||||
---|---|---|---|---|---|---|
Advanced user | Casual user | Plan to use | Impossible to do without | Hard to do without | ||
vio compilation | ||||||
vos / vok compilation | ||||||
The par: goal selector |
||||||
The Add LoadPath command |
||||||
The coqrc configuration file |
coqrc
file (after removing any potentially identifying information), please include it here.
Use | Aware of but don't use | Want to try | |
---|---|---|---|
Automatic indentation | |||
Ltac Debug mode support | |||
Automatic compilation of required libraries (option coq-compile-before-require ) |
|||
Quick / vos compilation of required libraries (option coq-compile-vos ) |
|||
Use Proof General locally running Coq on a big server (via Tramp ) |
|||
Proof visualization as a proof tree during proof development (prooftree ) |
|||
Omitting complete proofs for speed when processing large chunks (option proof-omit-proof-option ) |
|||
Display proof terms stepwise in the *response* buffer (option coq-show-proof-stepwise ) |
|||
Display proof diffs between consecutive goals thanks to the Set Diffs "on". or Set Diffs "removed". option enabled from the Proof General menu. |
|||
Automatically process the phrase when typing dot or double-dot, thanks to the Electric terminator or Double hit electric terminator modes (options proof-electric-terminator-enable or coq-double-hit-enable ) |
|||
Enable the mode to automatically add Proof using _. clauses. |
proof-three-window-enable
or command M-x proof-three-window-toggle
)
~/.emacs
)? If yes, briefly speaking, what are these customizations and would you like to have some of them applied by default?
If you have general feedback on CI in the Coq ecosystem, feel free to share it here.
The question of a name change is regularly discussed in the Coq community due to the offensive meaning that is most associated with the word "cock" in current English.
During a community-wide discussion on the topic in April 2021, testimonies were shared about current Coq users experiencing harassment and awkward situations, and potential Coq users turning away from the community—all due to the name.
Given the potential impact of the current name on the growth of our community and on its diversity, the Coq development team has opened a path to a possible renaming (https://coq.discourse.group/t/renaming-coq/1264).
A wiki page was opened to collect renaming ideas and this survey was announced to ask about many topics, including the possible name change.
The results of this survey will be used to inform the decision of the Coq development team. However, this is not a vote. The final decision on a possible renaming will be taken by the core developers alone.
Please provide us with your honest answers, not what you think we want to hear or what you perceive as socially acceptable.
Love | Like | Find acceptable | Do not like | Hate | |
---|---|---|---|---|---|
Change only the pronunciation to C.O.Q. |
|||||
Adjust the name to make it sound more French In particular, how would you rate the three specific examples below? |
|||||
LPC (Le Prouveur Coq) | |||||
Le Coq Formel |
|||||
Le Coq | |||||
Make the name longer In particular, how would you rate the five specific examples below? |
|||||
CoqPIT (PIT could mean: Prouveur Interactif de Théorèmes, i.e., a French translation of ITP for "Interactive Theorem Prover") |
|||||
Coquatrix |
|||||
Coqqio (a clever respelling of Korean "꼬끼오"—"Kkokkio"—, an onomatopoeia for the sound a rooster makes, which would be cock-a-doodle-doo in English) |
|||||
Coqorico (a respelling of French "cocorico", an onomatopoeia for the sound a rooster makes) |
|||||
Copa (Coq Proof Assistant) | |||||
Change the name to something unlike to the current name In particular, how would you rate the four specific examples below? |
|||||
Rocq (short for "Inria Rocquencourt", the place Coq was started at, also a respelling of a mythical bird: https://en.wikipedia.org/wiki/Roc_(mythology)) |
|||||
Gallo (the Italian word for rooster) |
|||||
Chook (Australian slang for a chicken) |
|||||
UP (Universal Prover) |
Essential | Worthwhile | Unimportant | Unwise | |
---|---|---|---|---|
Major new features | ||||
Refining existing features for better usability | ||||
Fixing bugs | ||||
Compatibility between releases and migration support | ||||
IDEs | ||||
Other development tools | ||||
Libraries and packages | ||||
Performance improvements | ||||
Documentation | ||||
Community building | ||||
Support channels |
Essential | Worthwhile | Unimportant | Unwise | |
---|---|---|---|---|
Description of individual tactics and commands | ||||
Examples of tactics and commands (in the documentation or in separate files) | ||||
Explanations of Coq error messages | ||||
Discussions of which tactics and commands to use in which circumstances | ||||
Explanations of how Coq works (e.g. unification) | ||||
Description of major features, such as Ltac2 and SSReflect | ||||
A high level overview of proof techniques and how to use them in Coq (e.g. what are the popular techniques and packages for doing proofs about software) | ||||
Description of the standard library |
Hinders a lot | Hinders noticeably | Hinders a little | Does not hinder | |
---|---|---|---|---|
Lack of internals documentation | ||||
Code is difficult to understand / seems overly complex | ||||
Insufficient assistance with questions | ||||
Don’t know what changes would be helpful | ||||
Don’t know how difficult potential changes are to implement | ||||
Review process takes too long or is too difficult |
Feel free to write to the Coq Code of Conduct enforcement team (coq-conduct@inria.fr) about any (past or current) specific situations. For past situations, feel free to also tell us if the situation was eventually resolved and how.
We don't provide an open text field on this subject in order to keep the answers anonymous.
This is the last section of the survey. To send your results, you will need to press the "Submit" button at the bottom of the page.
Before this, we would really appreciate if you would complete the questions below, so that we can get a better understanding of who uses Coq and how perspectives vary among different segments of the community (although, once again, all the questions are optional).
At the bottom of the page, you will also find a text field to provide feedback on this survey, if you have some.
Thank you for taking the time to answer this survey. We really appreciate it! Aggregated results will be shared on the usual Coq channels.
2022-03-01 – 14:19
Submit your survey.
Thank you for completing this survey.