Survey of the Coq community

Purpose and participation instructions

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!

Personal data protection

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.

Proof assistant and programming experience

How did you first hear about Coq?

Choose one of the following answers
Please choose only one of the following:

  • Via the web / media
  • In scientific literature or at a technical presentation
  • Through a colleague or a friend
  • In a class
  • Other

How long have you used Coq?

Choose one of the following answers
Please choose only one of the following:

  • I have never used Coq
  • Less than a year
  • 1-2 years
  • 2-5 years
  • 5-10 years
  • More than 10 years

Many of the following questions assume you have used Coq before. If this is not the case, please select "I have never used Coq" above, which will hide all such questions.

Only answer this question if the following conditions are met:
Answer was at question '2 [howlong]' (How long have you used Coq?)

When was the last time you wrote Coq code? Please select the first answer that applies.

Only answer this question if the following conditions are met:
Answer was NOT 'I have never used Coq' at question '2 [howlong]' (How long have you used Coq?)

Choose one of the following answers
Please choose only one of the following:

  • Less than 1 week ago
  • Less than 1 month ago
  • Less than 6 months ago
  • Less than 1 year ago
  • Less than 2 years ago
  • Less than 5 years ago
  • Less than 10 years ago
  • 10 or more years ago

Do you have experience with other proof assistants?

Only answer this question if the following conditions are met:
Answer was NOT 'I have never used Coq' at question '2 [howlong]' (How long have you used Coq?)

Choose one of the following answers
Please choose only one of the following:

  • Yes
  • No

Which other proof assistant(s) do you have experience with?

Only answer this question if the following conditions are met:
Answer was 'Yes' at question '5 [proofassistantexp]' (Do you have experience with other proof assistants?)

Check all that apply
Please choose all that apply:

  • ACL2
  • Agda
  • F*
  • HOL Light
  • HOL4
  • Idris
  • Isabelle/HOL
  • Lean
  • LEGO
  • Matita
  • Mizar
  • NuPRL
  • PVS
  • Twelf
  • Other:

Did you have programming experience before you started using Coq?

Only answer this question if the following conditions are met:
Answer was NOT 'I have never used Coq' at question '2 [howlong]' (How long have you used Coq?)

Choose one of the following answers
Please choose only one of the following:

  • Yes
  • No

Which programming style(s) were you familiar with before you started using Coq?

Only answer this question if the following conditions are met:
Answer was 'Yes' at question '7 [programmingexp]' (Did you have programming experience before you started using Coq?)

Check all that apply
Please choose all that apply:

  • Imperative programming
  • Object-oriented programming
  • Functional programming
  • Logic programming
  • Other:

Which functional programming language(s) did you have prior experience with?

Only answer this question if the following conditions are met:
Answer was at question '8 [programmingstyle]' (Which programming style(s) were you familiar with before you started using Coq?)

Check all that apply
Please choose all that apply:

  • Clojure
  • Elixir
  • Elm
  • Erlang
  • F#
  • Haskell
  • OCaml
  • PureScript
  • Racket
  • ReasonML / Rescript
  • Scala
  • Scheme
  • Standard ML
  • Other:

Your use of Coq

For what purposes have you used Coq?

Only answer this question if the following conditions are met:
Answer was NOT 'I have never used Coq' at question '2 [howlong]' (How long have you used Coq?)

Check all that apply
Please choose all that apply:

  • Learning Coq
  • Learning something other than Coq
  • Teaching Coq
  • Teaching something other than Coq
  • Academic research
  • Industrial research / application
  • Personal projects
  • Other:

What are your Coq application domains?

Only answer this question if the following conditions are met:
((howlong.NAOK != "no"))

Check all that apply
Please choose all that apply:

  • Formalization of existing mathematical results
  • Formalization of novel mathematical results
  • Verification of software
  • Verification of hardware
  • Formalization of theoretical systems or languages
  • Other:

How did you start learning Coq?

Only answer this question if the following conditions are met:
Answer was NOT 'I have never used Coq' at question '2 [howlong]' (How long have you used Coq?)

Check all that apply
Please choose all that apply:

  • In a class
  • By myself
  • Together with or advised by colleagues in academia
  • Together with or advised by colleagues in industry
  • Other:

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.

Only answer this question if the following conditions are met:
-------- Scenario 1 --------
Answer was at question '10 [whatfor]' (For what purposes have you used Coq?)
-------- or Scenario 2 --------
Answer was at question '10 [whatfor]' (For what purposes have you used Coq?)
-------- or Scenario 3 --------
Answer was at question '12 [howlearn]' (How did you start learning Coq?)

If applicable, how would you describe the level of Coq use in your workplace?

Choose one of the following answers
Please choose only one of the following:

  • Coq is already well established at my workplace or in my team.
  • We use Coq at my workplace, but it’s not yet well established.
  • We have experimented with Coq at my workplace, but we have not yet committed to using it.
  • We haven't used Coq at my workplace.

What's the trend in Coq use in your workplace or team?

Only answer this question if the following conditions are met:
Answer was 'Coq is already well established at my workplace or in my team.' at question '14 [workplace]' (If applicable, how would you describe the level of Coq use in your workplace?)

Choose one of the following answers
Please choose only one of the following:

  • Coq usage is stable
  • Coq usage is increasing
  • Coq usage is decreasing

Which versions of Coq do you use?

Only answer this question if the following conditions are met:
howlong.NAOK != "no" and lastused.NAOK != "10y" and lastused.NAOK != "1y" and lastused.NAOK != "2y" and lastused.NAOK != "5y" and lastused.NAOK != "more"

Choose one of the following answers
Please choose only one of the following:

  • Mostly recent versions (8.13 or more recent)
  • Mostly older versions (8.12 or older)
  • Both

If you have projects that are not compatible with recent versions of Coq (8.13 or more recent), why is that?

Only answer this question if the following conditions are met:
howlong.NAOK != "no" and lastused.NAOK != "10y" and lastused.NAOK != "1y" and lastused.NAOK != "2y" and lastused.NAOK != "5y" and lastused.NAOK != "more"

Check all that apply
Please choose all that apply:

  • It would take too much effort to port them.
  • I don’t care that they aren’t on the latest version.
  • A dependency of the project is not compatible with recent versions of Coq.
  • Other:

Which operating system(s) have you last used Coq on (or would like to use Coq on)?

Check all that apply
Please choose all that apply:

  • Linux
  • macOS
  • Windows
  • Other:

Which Linux distribution(s) have you last used Coq on (or would like to use Coq on)?

Only answer this question if the following conditions are met:
Answer was at question '18 [operatingsystem]' (Which operating system(s) have you last used Coq on (or would like to use Coq on)?)

Check all that apply
Please choose all that apply:

  • ArchLinux
  • Debian
  • Fedora / RedHat
  • Linux Mint
  • Mandriva
  • NixOS
  • openSUSE
  • Ubuntu LTS ("Long Term Support")
  • Ubuntu non-LTS
  • Other:

Which version(s) of macOS have you last used Coq on (or would like to use Coq on)?

Only answer this question if the following conditions are met:
Answer was at question '18 [operatingsystem]' (Which operating system(s) have you last used Coq on (or would like to use Coq on)?)

Check all that apply
Please choose all that apply:

  • macOS 12: “Monterey”
  • macOS 11: “Big Sur”
  • macOS 10.15: “Catalina”
  • macOS 10.14: “Mojave”
  • macOS 10.13: “High Sierra”
  • An older macOS version

Which version(s) of Windows have you last used Coq on (or would like to use Coq on)?

Only answer this question if the following conditions are met:
Answer was at question '18 [operatingsystem]' (Which operating system(s) have you last used Coq on (or would like to use Coq on)?)

Check all that apply
Please choose all that apply:

  • Windows 10 (or Windows 11)
  • An older version of Windows

Have you run (or would like to run) Coq in WSL (Windows Subsystem for Linux) or as a "native" Windows application?

Only answer this question if the following conditions are met:
Answer was at question '21 [windowsversion]' (Which version(s) of Windows have you last used Coq on (or would like to use Coq on)?)

Choose one of the following answers
Please choose only one of the following:

  • In the Windows Subsystem for Linux
  • As a "native" Windows application
  • Both

How have you installed Coq?

Only answer this question if the following conditions are met:
Answer was NOT 'I have never used Coq' at question '2 [howlong]' (How long have you used Coq?)

Check all that apply
Please choose all that apply:

  • Chocolatey
  • Conda
  • Coq Platform scripts
  • From sources
  • Homebrew
  • macOS installer
  • Nix
  • opam (without the Coq Platform scripts)
  • Package manager from my Linux distribution (synaptic, apt, yum, dnf, pacman, ...)
  • Snap
  • Windows installer
  • Other:

How have you installed the Coq libraries and plugins your work depends on?

Only answer this question if the following conditions are met:
Answer was NOT 'I have never used Coq' at question '2 [howlong]' (How long have you used Coq?)

Check all that apply
Please choose all that apply:

  • git submodule
  • Manually (e.g., by running make install)
  • Nix
  • opam
  • Vendoring (i.e., copying the sources of the dependencies in a sub-directory of your project)
  • Other:

Which editors or IDEs have you used for Coq?

Only answer this question if the following conditions are met:
Answer was NOT 'I have never used Coq' at question '2 [howlong]' (How long have you used Coq?)

Check all that apply
Please choose all that apply:

  • Emacs and variants (Spacemacs, Doom...)
  • Vim and variants (NeoVim...)
  • Visual Studio Code with VSCoq
  • CoqIDE
  • jsCoq
  • Executable notebook with coq_jupyter
  • Other:

Which Emacs plugins have you used for Coq?

Only answer this question if the following conditions are met:
Answer was at question '25 [ide]' (Which editors or IDEs have you used for Coq?)

Check all that apply
Please choose all that apply:

Which Vim plugins have you used for Coq?

Only answer this question if the following conditions are met:
Answer was at question '25 [ide]' (Which editors or IDEs have you used for Coq?)

Check all that apply
Please choose all that apply:

What factors influence your choice of one IDE over another?

Only answer this question if the following conditions are met:
Answer was NOT 'I have never used Coq' at question '2 [howlong]' (How long have you used Coq?)

Check all that apply
Please choose all that apply:

  • Lack or availability of particular features
  • Quality of community help for solving issues
  • (Limited) awareness of alternatives
  • Editor preference
  • Ease of installation
  • Other:

If you have Coq projects, have you used continuous integration (CI) for any of them?

Only answer this question if the following conditions are met:
Answer was NOT 'I have never used Coq' at question '2 [howlong]' (How long have you used Coq?)

Choose one of the following answers
Please choose only one of the following:

  • Yes.
  • I don’t know what CI is.
  • I know what CI is, but I don’t use it for my Coq projects.

Why don't you use continuous integration (CI) for your Coq projects?

Only answer this question if the following conditions are met:
Answer was 'I know what CI is, but I don’t use it for my Coq projects.' at question '29 [useci]' (If you have Coq projects, have you used continuous integration (CI) for any of them?)

Choose one of the following answers
Please choose only one of the following:

  • I don't want / need it.
  • I don't know how to / did not manage to set it up.
  • Other

Your use of Coq features, libraries and tools

The questions in this section are hidden when "I have never used Coq" is selected in the first section. Please proceed to the next section.

Only answer this question if the following conditions are met:
Answer was 'I have never used Coq' at question '2 [howlong]' (How long have you used Coq?)

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.

Only answer this question if the following conditions are met:
Answer was NOT 'I have never used Coq' at question '2 [howlong]' (How long have you used Coq?)

Tactic groups

Only answer this question if the following conditions are met:
Answer was NOT 'I have never used Coq' at question '2 [howlong]' (How long have you used Coq?)

Please choose the appropriate response for each item:

Usage Importance
Advanced user Casual user Plan to use Impossible to do without Hard to do without
The standard tactics
SSReflect

Tactic languages

Only answer this question if the following conditions are met:
Answer was NOT 'I have never used Coq' at question '2 [howlong]' (How long have you used Coq?)

Please choose the appropriate response for each item:

Usage Importance
Advanced user Casual user Plan to use Impossible to do without Hard to do without
Ltac
Ltac2
Mtac2
MetaCoq
Coq-Elpi

Language features

Only answer this question if the following conditions are met:
Answer was NOT 'I have never used Coq' at question '2 [howlong]' (How long have you used Coq?)

Please choose the appropriate response for each item:

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

Core plugins and tools

Only answer this question if the following conditions are met:
Answer was NOT 'I have never used Coq' at question '2 [howlong]' (How long have you used Coq?)

Please choose the appropriate response for each item:

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)

Ecosystem plugins and tools

Only answer this question if the following conditions are met:
Answer was NOT 'I have never used Coq' at question '2 [howlong]' (How long have you used Coq?)

Please choose the appropriate response for each item:

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

General libraries

Only answer this question if the following conditions are met:
Answer was NOT 'I have never used Coq' at question '2 [howlong]' (How long have you used Coq?)

Please choose the appropriate response for each item:

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

Mathematical Components libraries

Only answer this question if the following conditions are met:
Answer was NOT 'I have never used Coq' at question '2 [howlong]' (How long have you used Coq?) and Answer was NOT at question '38 [genlib]' (General libraries (Mathematical Components Label Usage))

Please choose the appropriate response for each item:

Domain-specific libraries

Only answer this question if the following conditions are met:
Answer was NOT 'I have never used Coq' at question '2 [howlong]' (How long have you used Coq?)

Please choose the appropriate response for each item:

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

Sublibraries of Coq's standard library

Only answer this question if the following conditions are met:
Answer was NOT 'I have never used Coq' at question '2 [howlong]' (How long have you used Coq?)

Please choose the appropriate response for each item:

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

Program extraction targets

Only answer this question if the following conditions are met:
Answer was NOT 'I have never used Coq' at question '2 [howlong]' (How long have you used Coq?)

Please choose the appropriate response for each item:

Usage Importance
Advanced user Casual user Plan to use Impossible to do without Hard to do without
OCaml
Haskell
Scheme
JSON

If you’re interested in new extraction targets, which languages do you want?

Only answer this question if the following conditions are met:
Answer was NOT 'I have never used Coq' at question '2 [howlong]' (How long have you used Coq?)

Please write your answer here:

If you have multiple answers, please provide a comma-separated list.

Other features

Only answer this question if the following conditions are met:
Answer was NOT 'I have never used Coq' at question '2 [howlong]' (How long have you used Coq?)

Please choose the appropriate response for each item:

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

If you are willing to share the contents of your coqrc file (after removing any potentially identifying information), please include it here.

Only answer this question if the following conditions are met:
((howlong.NAOK != "no") and (otherfeatures_coqrc_0.NAOK == "casua" or otherfeatures_coqrc_0.NAOK == "advan"))

Please write your answer here:

Your use of Coq IDEs

This section contains questions about various IDEs for Coq, depending on what IDE you have declared you have used in the "Your use of Coq" section. If you would like to see all the questions, including those corresponding to other IDEs, you can do so by changing the answer to the first question bellow.

Do you want to show all the IDE questions, including for IDEs that you did not say you have used? *

Please choose only one of the following:

  • Yes
  • No

How satisfied are you with Proof General?

Only answer this question if the following conditions are met:
((emacsplugins_pg.NAOK == "Y")) or ((showidequestions.NAOK == "Y"))

Choose one of the following answers
Please choose only one of the following:

  • Very satisfied
  • Satisfied
  • Neutral
  • Unsatisfied
  • Very unsatisfied

How long have you used Proof General?

Only answer this question if the following conditions are met:
((emacsplugins_pg.NAOK == "Y")) or ((showidequestions.NAOK == "Y"))

Choose one of the following answers
Please choose only one of the following:

  • Less than 1 year
  • 1-2 years
  • 2-5 years
  • 5-10 years
  • More than 10 years

Which variants of Emacs have you used with Proof General?

Only answer this question if the following conditions are met:
((emacsplugins_pg.NAOK == "Y")) or ((showidequestions.NAOK == "Y"))

Check all that apply
Please choose all that apply:

  • GNU Emacs
  • Spacemacs
  • Doom
  • Other:

For each of the following features of Proof General, please indicate your awareness and use of the feature. Please skip any feature that you don't know and are not interested in (leave "No answer" for these).

Only answer this question if the following conditions are met:
((emacsplugins_pg.NAOK == "Y")) or ((showidequestions.NAOK == "Y"))

Please choose the appropriate response for each item:

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.

How do you show proof script, goals and responses in Proof General?

Only answer this question if the following conditions are met:
((emacsplugins_pg.NAOK == "Y")) or ((showidequestions.NAOK == "Y"))

Choose one of the following answers
Please choose only one of the following:

  • Usually in three separate Emacs windows (option proof-three-window-enable or command M-x proof-three-window-toggle )
  • Usually in two windows
  • It varies

Are there any features of Company-Coq that you find distracting or that you manually disable? Which ones?

Only answer this question if the following conditions are met:
-------- Scenario 1 --------
Answer was at question '26 [emacsplugins]' (Which Emacs plugins have you used for Coq?)
-------- or Scenario 2 --------
Answer was 'Yes' at question '46 [showidequestions]' (Do you want to show all the IDE questions, including for IDEs that you did not say you have used?)

Please write your answer here:

Do you use specific customizations or fixups of Proof General or Company-Coq (in your ~/.emacs)? If yes, briefly speaking, what are these customizations and would you like to have some of them applied by default?

Only answer this question if the following conditions are met:
((emacsplugins_pg.NAOK == "Y")) or ((showidequestions.NAOK == "Y"))

Please write your answer here:

What improvements, bug fixes and new features would you most like to see in Proof General? (The issue tracker for Proof General is https://github.com/ProofGeneral/PG/issues.)

Only answer this question if the following conditions are met:
((emacsplugins_pg.NAOK == "Y")) or ((showidequestions.NAOK == "Y"))

Please write your answer here:

How satisfied are you with Coqtail?

Only answer this question if the following conditions are met:
-------- Scenario 1 --------
Answer was at question '27 [vimplugins]' (Which Vim plugins have you used for Coq?)
-------- or Scenario 2 --------
Answer was 'Yes' at question '46 [showidequestions]' (Do you want to show all the IDE questions, including for IDEs that you did not say you have used?)

Choose one of the following answers
Please choose only one of the following:

  • Very satisfied
  • Satisfied
  • Neutral
  • Unsatisfied
  • Very unsatisfied

How long have you used Coqtail?

Only answer this question if the following conditions are met:
((vimplugins_coqtail.NAOK == "Y")) or ((showidequestions.NAOK == "Y"))

Choose one of the following answers
Please choose only one of the following:

  • Less than 1 year
  • 1-2 years
  • 2-5 years
  • 5-10 years
  • More than 10 years

Which variants of Vim have you used with Coqtail?

Only answer this question if the following conditions are met:
((vimplugins_coqtail.NAOK == "Y")) or ((showidequestions.NAOK == "Y"))

Check all that apply
Please choose all that apply:

  • Vim
  • NeoVim
  • Other:

What Vim / NeoVim features or plugins would you like to have better integrated with Coqtail?

Only answer this question if the following conditions are met:
((vimplugins_coqtail.NAOK == "Y")) or ((showidequestions.NAOK == "Y"))

Please write your answer here:

What improvements, bug fixes and new features would you most like to see in Coqtail? (The issue tracker for Coqtail is https://github.com/whonore/Coqtail/issues.)

Only answer this question if the following conditions are met:
((vimplugins_coqtail.NAOK == "Y")) or ((showidequestions.NAOK == "Y"))

Please write your answer here:

How satisfied are you with VsCoq?

Only answer this question if the following conditions are met:
-------- Scenario 1 --------
Answer was at question '25 [ide]' (Which editors or IDEs have you used for Coq?)
-------- or Scenario 2 --------
Answer was 'Yes' at question '46 [showidequestions]' (Do you want to show all the IDE questions, including for IDEs that you did not say you have used?)

Choose one of the following answers
Please choose only one of the following:

  • Very satisfied
  • Satisfied
  • Neutral
  • Unsatisfied
  • Very unsatisfied

How long have you used VsCoq?

Only answer this question if the following conditions are met:
((ide_vscode.NAOK == "Y")) or ((showidequestions.NAOK == "Y"))

Choose one of the following answers
Please choose only one of the following:

  • Less than 1 year
  • 1-2 years
  • 2-5 years
  • 5-10 years
  • More than 10 years

What improvements, bug fixes and new features would you most like to see in VsCoq? (The issue tracker for VsCoq is https://github.com/coq-community/vscoq/issues.)

Only answer this question if the following conditions are met:
((ide_vscode.NAOK == "Y")) or ((showidequestions.NAOK == "Y"))

Please write your answer here:

How satisfied are you with CoqIDE?

Only answer this question if the following conditions are met:
-------- Scenario 1 --------
Answer was at question '25 [ide]' (Which editors or IDEs have you used for Coq?)
-------- or Scenario 2 --------
Answer was 'Yes' at question '46 [showidequestions]' (Do you want to show all the IDE questions, including for IDEs that you did not say you have used?)

Choose one of the following answers
Please choose only one of the following:

  • Very satisfied
  • Satisfied
  • Neutral
  • Unsatisfied
  • Very unsatisfied

How long have you used CoqIDE?

Only answer this question if the following conditions are met:
((ide_coqide.NAOK == "Y")) or ((showidequestions.NAOK == "Y"))

Choose one of the following answers
Please choose only one of the following:

  • Less than 1 year
  • 1-2 years
  • 2-5 years
  • 5-10 years
  • More than 10 years

Do you use the Templates menu in CoqIDE?

Only answer this question if the following conditions are met:
((ide_coqide.NAOK == "Y") or (showidequestions.NAOK == "Y")) and (lastused.NAOK != "10y" and lastused.NAOK != "5y" and lastused.NAOK != "more")

Choose one of the following answers
Please choose only one of the following:

  • Yes
  • No

What improvements, bug fixes and new features would you most like to see in CoqIDE? (The issue tracker for CoqIDE is https://github.com/coq/coq/labels/part%3A%20IDE.)

Only answer this question if the following conditions are met:
((ide_coqide.NAOK == "Y")) or ((showidequestions.NAOK == "Y"))

Please write your answer here:

How satisfied are you with jsCoq?

Only answer this question if the following conditions are met:
-------- Scenario 1 --------
Answer was at question '25 [ide]' (Which editors or IDEs have you used for Coq?)
-------- or Scenario 2 --------
Answer was 'Yes' at question '46 [showidequestions]' (Do you want to show all the IDE questions, including for IDEs that you did not say you have used?)

Choose one of the following answers
Please choose only one of the following:

  • Very satisfied
  • Satisfied
  • Neutral
  • Unsatisfied
  • Very unsatisfied

How long have you used jsCoq?

Only answer this question if the following conditions are met:
((ide_jscoq.NAOK == "Y")) or ((showidequestions.NAOK == "Y"))

Choose one of the following answers
Please choose only one of the following:

  • Less than 1 year
  • 1-2 years
  • 2-5 years
  • 5-10 years
  • More than 10 years

What have you used jsCoq for?

Only answer this question if the following conditions are met:
((ide_jscoq.NAOK == "Y")) or ((showidequestions.NAOK == "Y"))

Check all that apply
Please choose all that apply:

  • Casual proof development (e.g., to quickly check statements / perform usual Coq work)
  • Embedding in HTML documents (in author interactive documents as described in embedding.md)
  • Sharing snippets with other users (using the sharing feature of the scratchpad)
  • Other:

What improvements, bug fixes and new features would you most like to see in jsCoq? (The issue tracker for jsCoq is https://github.com/jscoq/jscoq/issues.)

Only answer this question if the following conditions are met:
((ide_jscoq.NAOK == "Y")) or ((showidequestions.NAOK == "Y"))

Please write your answer here:

How satisfied are you with coq_jupyter?

Only answer this question if the following conditions are met:
-------- Scenario 1 --------
Answer was at question '25 [ide]' (Which editors or IDEs have you used for Coq?)
-------- or Scenario 2 --------
Answer was 'Yes' at question '46 [showidequestions]' (Do you want to show all the IDE questions, including for IDEs that you did not say you have used?)

Choose one of the following answers
Please choose only one of the following:

  • Very satisfied
  • Satisfied
  • Neutral
  • Unsatisfied
  • Very unsatisfied

How long have you used coq_jupyter?

Only answer this question if the following conditions are met:
((ide_jupyter.NAOK == "Y")) or ((showidequestions.NAOK == "Y"))

Choose one of the following answers
Please choose only one of the following:

  • Less than 1 year
  • 1-2 years
  • 2-5 years
  • 5-10 years
  • More than 10 years

Have you used (or have you tried to use) Jupyter hosted by third parties (e.g Binder/Azure Notebooks/Google Colaboratory/CoCalc) with coq_jupyter?

Only answer this question if the following conditions are met:
((ide_jupyter.NAOK == "Y")) or ((showidequestions.NAOK == "Y"))

Choose one of the following answers
Please choose only one of the following:

  • I use it.
  • I don't use it, but I have tried.
  • I don't use it and haven't tried.

Have you had any issues or lack of support for coq_kernel for any service? If so, feel free to share here.

Only answer this question if the following conditions are met:
Answer was 'I use it.' or 'I don't use it, but I have tried.' at question '73 [jupyterthirdparty]' (Have you used (or have you tried to use) Jupyter hosted by third parties (e.g Binder/Azure Notebooks/Google Colaboratory/CoCalc) with coq_jupyter?)

Please write your answer here:

Have you used coq_jupyter collaboratively (meaning accessing the same instance of the kernel from different machines / by different users)?

Only answer this question if the following conditions are met:
((ide_jupyter.NAOK == "Y")) or ((showidequestions.NAOK == "Y"))

Choose one of the following answers
Please choose only one of the following:

  • Yes
  • No

What improvements, bug fixes and new features would you most like to see in coq_jupyter? (The issue tracker for coq_jupyter is https://github.com/EugeneLoy/coq_jupyter/issues.)

Only answer this question if the following conditions are met:
((ide_jupyter.NAOK == "Y")) or ((showidequestions.NAOK == "Y"))

Please write your answer here:

Your use of Continuous Integration

The questions in this section only appear if you answered that you have used CI on some Coq project in the "Your use of Coq" section. Please proceed to the next section.

Only answer this question if the following conditions are met:
Answer was NOT 'Yes.' at question '29 [useci]' (If you have Coq projects, have you used continuous integration (CI) for any of them?)

Which CI platforms have you last used for your Coq projects?

Only answer this question if the following conditions are met:
Answer was 'Yes.' at question '29 [useci]' (If you have Coq projects, have you used continuous integration (CI) for any of them?)

Check all that apply
Please choose all that apply:

  • Travis CI
  • GitHub Actions
  • GitLab CI
  • Circle CI
  • Other:

Which of these tools have you last used?

Only answer this question if the following conditions are met:
((useci.NAOK == "yes"))

Check all that apply
Please choose all that apply:

What encouraged you to use a custom solution rather than one of the coq-community tools? (Docker-Coq, Docker-Coq-Action, Coq Nix Toolbox, templates)
 

Only answer this question if the following conditions are met:
((citools_docke.NAOK == "Y")) or ((citools_nix.NAOK == "Y")) or ((citools_opam.NAOK == "Y")) or ((citools_other))

Check all that apply
Please choose all that apply:

  • I didn't know about them.
  • They don't fit my use case.
  • I didn't use them because of licensing concerns.
  • I already used another solution before they were available or before I learned about them.
  • It's more work to learn how to use them than to use my custom solution.
  • I use a tool made by someone else.
  • Other:

If you have general feedback on CI in the Coq ecosystem, feel free to share it here.

Only answer this question if the following conditions are met:
((useci.NAOK == "yes"))

Please write your answer here:

Renaming Coq

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 communityall 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.

Should Coq be renamed?

Choose one of the following answers
Please choose only one of the following:

  • Absolutely
  • Probably should
  • I don't care / I don't know
  • Probably should not
  • Absolutely not

If you wish to elaborate on why Coq should / should not be renamed, feel free to do it here.

Please write your answer here:

If Coq is renamed, how would you rate the following options?

Please choose the appropriate response for each item:

Love Like Find acceptable Do not like Hate

Change only the pronunciation to C.O.Q.
(least disruptive option)

Adjust the name to make it sound more French
(will not require changing command-line tools)

In particular, how would you rate the three specific examples below?

LPC (Le Prouveur Coq)

Le Coq Formel
(should not be shortened into LCF to avoid confusion with the proof assistant from the 1970s)

Le Coq

Make the name longer
(will not require changing command-line tools)

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
(a two-legged dragon or serpent-like creature with a rooster's head, see:
https://en.wikipedia.org/wiki/Cockatrice
https://fr.wikipedia.org/wiki/Cocatrix)

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
(requires changing command-line tools and adjusting some tool and library names in the ecosystem)

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)

If you wish to share any specific arguments in favor or against some specific name choices, please do so here.

Please write your answer here:

Coq improvements

In order to make you more productive in Coq and to encourage others to learn and use Coq, how important are improvements in the following areas (relative to their current state)? (Skip any item you don't have an opinion on, or if you have no idea of what the current state is.)

Please choose the appropriate response for each item:

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

Feel free to elaborate on any of the items listed above, their importance, etc. Are there other improvements that you think would be important? Also, feel free to tell us how Coq does compared to other proof assistants you have experience with.
 

Please write your answer here:

How important are improvements to the following aspects of the Coq documentation (relative to their current state)? (Skip any item you don't have an opinion on, or if you have no idea of what the current state is.)

Please choose the appropriate response for each item:

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

Feel free to elaborate on any of the items listed above, their importance, etc. Are there other improvements that you think would be important?

Please write your answer here:

Do you agree that the availability of more written materials in languages other than English would encourage more people to use Coq? (Skip if you don't know.)

Choose one of the following answers
Please choose only one of the following:

  • Strongly agree
  • Agree
  • Neutral
  • Disagree
  • Strongly disagree

What languages would be the most useful to support?

Only answer this question if the following conditions are met:
-------- Scenario 1 --------
Answer was 'Strongly agree' at question '90 [nonenglishdoc]' (Do you agree that the availability of more written materials in languages other than English would encourage more people to use Coq? (Skip if you don't know.))
-------- or Scenario 2 --------
Answer was 'Agree' at question '90 [nonenglishdoc]' (Do you agree that the availability of more written materials in languages other than English would encourage more people to use Coq? (Skip if you don't know.))

Please write your answer here:

If you have multiple answers, please provide a comma-separated list.

How was your experience while learning Coq? For example, what were the easiest and/or most difficult parts of the process? Do you have suggestions to improve the experience?

Only answer this question if the following conditions are met:
Answer was NOT 'I have never used Coq' at question '2 [howlong]' (How long have you used Coq?)

Please write your answer here:

Have you ever tried contributing changes to the Coq GitHub project, such as to libraries, documentation or code for bug fixes or improvements?

Choose one of the following answers
Please choose only one of the following:

  • Yes
  • No

Why not?

Only answer this question if the following conditions are met:
Answer was 'No' at question '93 [triedcontributing]' (Have you ever tried contributing changes to the Coq GitHub project, such as to libraries, documentation or code for bug fixes or improvements?)

Check all that apply
Please choose all that apply:

  • Not interested
  • Don’t have the time
  • Never considered it
  • Limited programming skills
  • Too difficult to do so
  • Other:

Did you accomplish what you wanted?

Only answer this question if the following conditions are met:
Answer was 'Yes' at question '93 [triedcontributing]' (Have you ever tried contributing changes to the Coq GitHub project, such as to libraries, documentation or code for bug fixes or improvements?)

Choose one of the following answers
Please choose only one of the following:

  • Yes
  • No

How much do the following hinder your ability or desire to contribute changes to Coq?

Please choose the appropriate response for each item:

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 elaborate on the contributing experience, what we can do better, or why you do not contribute.

Please write your answer here:

Community inclusion

Before reading this question, were you aware of the Code of Conduct that applies to all spaces (physical and online) of the Coq community?

Choose one of the following answers
Please choose only one of the following:

  • No, I wasn't aware.
  • Yes, I was aware that it exists, but I hadn't read it (yet).
  • Yes, I was aware, and I had read it.

Have you ever, while contributing to Coq or participating in the Coq community (online or offline, on official or non-official channels), encountered situations in which you have felt unwelcome or treated unfairly?

Choose one of the following answers
Please choose only one of the following:

  • Yes
  • No

How often have you encountered such situations?

Only answer this question if the following conditions are met:
Answer was 'Yes' at question '99 [unwelcome]' (Have you ever, while contributing to Coq or participating in the Coq community (online or offline, on official or non-official channels), encountered situations in which you have felt unwelcome or treated unfairly?)

Choose one of the following answers
Please choose only one of the following:

  • Less than once per year
  • Yearly
  • Monthly
  • Weekly
  • Daily

Where did these situations occur?

Only answer this question if the following conditions are met:
((unwelcome.NAOK == "yes"))

Check all that apply
Please choose all that apply:

  • Official Coq repositories (https://github.com/coq/coq and https://github.com/opam-coq-archive)
  • Other Coq-related repositories
  • Official forums (Coq-Club, Coqdev mailing list, Discourse forum, Zulip chat)
  • Other forums (Stack Overflow, Stack Exchange, Reddit, Twitter, etc.)
  • In-person events (Coq Workshop, CoqPL, Coq meetup, etc.)
  • Other:

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.

Only answer this question if the following conditions are met:
((unwelcome.NAOK == "yes"))

Demographics and conclusion

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.

What is your gender?

Check all that apply
Please choose all that apply:

  • Woman
  • Man
  • Non-binary
  • Prefer to self-describe:

What is your age?

Choose one of the following answers
Please choose only one of the following:

  • 19 or younger
  • 20 - 29
  • 30 - 39
  • 40 - 49
  • 50 - 59
  • 60 - 69
  • 70 or older

Where do you live?

Choose one of the following answers
Please choose only one of the following:

  • Afghanistan
  • Åland Islands
  • Albania
  • Algeria
  • American Samoa
  • Andorra
  • Angola
  • Anguilla
  • Antarctica
  • Antigua & Barbuda
  • Argentina
  • Armenia
  • Aruba
  • Australia
  • Austria
  • Azerbaijan
  • Bahamas
  • Bahrain
  • Bangladesh
  • Barbados
  • Belarus
  • Belgium
  • Belize
  • Benin
  • Bermuda
  • Bhutan
  • Bolivia
  • Bosnia & Herzegovina
  • Botswana
  • Bouvet Island
  • Brazil
  • British Indian Ocean Territory
  • British Virgin Islands
  • Brunei
  • Bulgaria
  • Burkina Faso
  • Burundi
  • Cambodia
  • Cameroon
  • Canada
  • Cape Verde
  • Caribbean Netherlands
  • Cayman Islands
  • Central African Republic
  • Chad
  • Chile
  • China mainland
  • Christmas Island
  • Cocos (Keeling) Islands
  • Colombia
  • Comoros
  • Congo - Brazzaville
  • Congo - Kinshasa
  • Cook Islands
  • Costa Rica
  • Côte d’Ivoire
  • Croatia
  • Cuba
  • Curaçao
  • Cyprus
  • Czechia
  • Denmark
  • Djibouti
  • Dominica
  • Dominican Republic
  • Ecuador
  • Egypt
  • El Salvador
  • Equatorial Guinea
  • Eritrea
  • Estonia
  • Eswatini
  • Ethiopia
  • Falkland Islands
  • Faroe Islands
  • Fiji
  • Finland
  • France
  • French Guiana
  • French Polynesia
  • French Southern Territories
  • Gabon
  • Gambia
  • Georgia
  • Germany
  • Ghana
  • Gibraltar
  • Greece
  • Greenland
  • Grenada
  • Guadeloupe
  • Guam
  • Guatemala
  • Guernsey
  • Guinea
  • Guinea-Bissau
  • Guyana
  • Haiti
  • Heard & McDonald Islands
  • Honduras
  • Hong Kong SAR
  • Hungary
  • Iceland
  • India
  • Indonesia
  • Iran
  • Iraq
  • Ireland
  • Isle of Man
  • Israel
  • Italy
  • Jamaica
  • Japan
  • Jersey
  • Jordan
  • Kazakhstan
  • Kenya
  • Kiribati
  • Kuwait
  • Kyrgyzstan
  • Laos
  • Latvia
  • Lebanon
  • Lesotho
  • Liberia
  • Libya
  • Liechtenstein
  • Lithuania
  • Luxembourg
  • Macao SAR
  • Madagascar
  • Malawi
  • Malaysia
  • Maldives
  • Mali
  • Malta
  • Marshall Islands
  • Martinique
  • Mauritania
  • Mauritius
  • Mayotte
  • Mexico
  • Micronesia
  • Moldova
  • Monaco
  • Mongolia
  • Montenegro
  • Montserrat
  • Morocco
  • Mozambique
  • Myanmar (Burma)
  • Namibia
  • Nauru
  • Nepal
  • Netherlands
  • New Caledonia
  • New Zealand
  • Nicaragua
  • Niger
  • Nigeria
  • Niue
  • Norfolk Island
  • North Korea
  • North Macedonia
  • Northern Mariana Islands
  • Norway
  • Oman
  • Pakistan
  • Palau
  • Palestinian Territories
  • Panama
  • Papua New Guinea
  • Paraguay
  • Peru
  • Philippines
  • Pitcairn Islands
  • Poland
  • Portugal
  • Puerto Rico
  • Qatar
  • Réunion
  • Romania
  • Russia
  • Rwanda
  • Samoa
  • San Marino
  • São Tomé & Príncipe
  • Saudi Arabia
  • Senegal
  • Serbia
  • Seychelles
  • Sierra Leone
  • Singapore
  • Sint Maarten
  • Slovakia
  • Slovenia
  • Solomon Islands
  • Somalia
  • South Africa
  • South Georgia & South Sandwich Islands
  • South Korea
  • South Sudan
  • Spain
  • Sri Lanka
  • St. Barthélemy
  • St. Helena
  • St. Kitts & Nevis
  • St. Lucia
  • St. Martin
  • St. Pierre & Miquelon
  • St. Vincent & Grenadines
  • Sudan
  • Suriname
  • Svalbard & Jan Mayen
  • Sweden
  • Switzerland
  • Syria
  • Taiwan
  • Tajikistan
  • Tanzania
  • Thailand
  • Timor-Leste
  • Togo
  • Tokelau
  • Tonga
  • Trinidad & Tobago
  • Tunisia
  • Turkey
  • Turkmenistan
  • Turks & Caicos Islands
  • Tuvalu
  • U.S. Outlying Islands
  • U.S. Virgin Islands
  • Uganda
  • Ukraine
  • United Arab Emirates
  • United Kingdom
  • United States
  • Uruguay
  • Uzbekistan
  • Vanuatu
  • Vatican City
  • Venezuela
  • Vietnam
  • Wallis & Futuna
  • Western Sahara
  • Yemen
  • Zambia
  • Zimbabwe

Are you...

Check all that apply
Please choose all that apply:

  • employed by an academic institution?
  • employed by a non-academic public institution?
  • employed by a non-academic private organization, such as a company or a non-profit?
  • self-employed?
  • a student?
  • retired?
  • not employed?
  • Other:

What is the highest level of education you've completed?

Choose one of the following answers
Please choose only one of the following:

  • No high school diploma
  • High school or equivalent
  • Bachelor's degree or equivalent
  • Master's degree or equivalent
  • PhD or equivalent

If you're doing research (as an academic researcher, as a student, in industry, or independently), what topics do you research?

Check all that apply
Please choose all that apply:

  • Programming languages
  • Formal methods
  • Algorithms and complexity
  • Software engineering
  • Computer science other than the above
  • Logic
  • Algebra
  • Analysis
  • Topology
  • Mathematics other than the above
  • Physics
  • Engineering
  • Social science
  • Economics
  • Law
  • Linguistics
  • Philosophy
  • Other:

Thanks for completing the survey! Did you encounter any issues with the survey that you'd like to report or do you have other feedback that we should hear about? If so, please use the text field below.

Please write your answer here:

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.