Basics

Do you use Coq?

Where have you used Coq? (check all that apply)

• Used it in a class
• Used it on my own
• Used it for research
• Used it professionally

Which of the following have you used to learn Coq?

• Software Foundations
• Certified Programming with Dependent Types (CPDT)
• Coq'Art
• Course material

What version of Coq do you use? (v8.4, v8.5, v8.6, trunk)

Do you use CoqIDE, ProofGeneral, Vim, or something else?

Ecosystem

Do you run into Coq bugs? Do you report them or find workarounds?

Do you follow coq-club@? Post to it?

Features

For all features, I would like to know if they've even heard of it, or knew about it but rejected it.

Do you customize warnings?

Do you use modules?

Module functors?

Do you use proof mode to construct terms in Type?

Do you use tactics in terms (ltac:())?

Do you write complicated automation?

Do you use parallel and/or lazy proof processing in CoqIDE?

Do you use coq_makefile?

Do you use Ltac selectors (1:, all:, par:)?

Do you use multiple successes (basically +)?

Do you write nested lemmas (start a proof within an outer proof script)? Do you leave nested lemmas in the final development, or only during development?

Type of usage

Do you ever need to improve the performance of Ltac code (to reduce memory usage or time)?

Do you use extraction? To OCaml or Haskell?

To what extent do you use dependent types?

• not at all (only polymorphism and theorems)
• occasionally (put some correctness conditions in types)
• heavily (types like Fin.t and others with strong guarantees)