此问卷调查旨在帮助我们更好地了解Coq社区，了解人们如何使用Coq，并收集建议以供将来参考。我们诚邀各位热心人士参与此调查，不论你有多少使用Coq的经验，或是正在学习或打算使用Coq。你提供的信息将被保密。
此调查中的多项选择部分预计耗时30分钟。跳过一些问题也没关系，你的意见依然对我们大有帮助。你可以任何顺序作答；例如可以先回答对你最重要的题目。你可通过右上角的菜单栏跳转到问卷的任一页面。你也可以做一半之后保存答案，有空再来继续。注意：答完之后，请记得在最后一页按下提交按钮，这样我们才会收到你的回答。本调查于北京时间2022年3月1日20时截止，请务必在此之前提交问卷！
法国国家信息与自动化研究所（Inria）致力于遵守通用数据保护条例（GDPR）保护个人信息。法国国家信息与自动化研究所基于自愿之前提，出于前文所述目的依法使用调查数据。
调查获取的数据将提供给Coq社区调查工作组，该组织位于欧盟境内。数据将被保管一年，且不会流向欧盟境外（不含个人信息的统计数据将向整个Coq社区公开发布）。以中文提交的回答将发送至欧盟境外，仅为翻译所用。调查数据由参与者自愿提供，且不被用于自动决策流程。
你可以获取你提供的信息、请求删除个人信息、对数据的处理方式行使反对、纠正、约束等权利。欲行使上述权利或咨询数据的处理方式，请联系数据保护专员，邮箱：dpo@infia.fr。如果你认为自己的权利收到侵害，或数据的处理方式不当，请向法国国家信息与自由权委员会举报（英文网站：https://www.cnil.fr/en/home、法文网站：https://www.cnil.fr/fr）。
本问卷有109个问题。
你是如何了解到Coq的?
下列问题大多假定你使用过Coq。如果你没使用过，请在上一问题中选择“我没使用过Coq”一项，以隐藏部分问题。
你上次写 Coq 代码是什么时候？请选择最接近的一项。
你是否有其他机器辅助证明工具的使用经验？
你还用过哪些机器辅助证明工具？
在接触使用Coq之前，你有无编程经验？
在接触使用Coq之前，你熟悉哪些编程风格？
你曾使用过哪些函数式编程语言？
Coq的维基页面收集了教授Coq的大学列表：
https://github.com/coq/coq/wiki/Universities-teaching-Coq
我们邀请您修订此页面，添加你教过、学过或听说过的课程。
你的工作单位使用Coq的程度如何？（仅限工作可能用到Coq的情况）
你的工作单位或团队使用Coq的程度呈什么趋势？
如果你有项目不兼容Coq 8.13以后的版本，会是出于什么原因？
你最近在哪些操作系统上使用，或愿意在哪些系统上使用Coq？
你更愿意在适用于Linux的Windows子系统（WSL）上，还是更愿意作为“原生”Windows应用运行Coq？
make install等命令） 你在选择集成开发环境（IDE）时的考量包括哪些？
你是否在Coq项目中使用过持续集成（CI）？
你不在Coq项目中使用持续集成是出于哪些考量？
如果你之前选择了“我没有使用过 Coq”，那么此部分题目将被隐藏，毋需作答。请前往下一章。
在下列问题中，针对 Coq 各项语言功能、函数库及工具，请选择你对它的使用程度，以及它对你的重要性。
如果你没听说过或不打算使用某一项，请选择“拒答”以跳过。如果某一项在你的工作中并非至关重要，请将“不可取代”、“难以取代”两栏留空。
如果你意外选择了某一栏，可点击“拒答”以清空所在行。
| 熟练运用 | 一般程度使用 | 计划使用 | 不可取代 | 难以取代 | ||
|---|---|---|---|---|---|---|
| 归纳类型（Inductive types） | ||||||
| 论域多态（Universe polymorphism） | ||||||
| 累进归纳类型（Cumulative inductive types） | ||||||
| 余归纳类型（Coinductive types） | ||||||
| SProp | ||||||
命令行-type-in-type选项、Universe Checking旗标或bypass_check(universes)标记 |
||||||
命令行-indices-matter选项 |
||||||
| 模块（Modules） | ||||||
| 函子模块类型（Module types, functors） | ||||||
| 类型类（Typeclasses） | ||||||
| 典型结构（Canonical structures） | ||||||
| 整数原语（Primitive integers） | ||||||
| 浮点数原语（Primitive floats） | ||||||
| 数组原语（Primitive arrays） |
| 熟练运用 | 一般程度使用 | 计划使用 | 不可取代 | 难以取代 | ||
|---|---|---|---|---|---|---|
| Bignums 大整数 | ||||||
| Coqdoc 注释文档 | ||||||
| coq_makefile | ||||||
| Equations | ||||||
| Function 递归函数定义 | ||||||
Micromega 算术求解（lia、nia、lra、nra、zify） |
||||||
| Nsatz | ||||||
| Program 程序验证 | ||||||
环（ring、ring_simplify、field） |
||||||
逻辑与等式求解（tauto、intuition、congruence、firstorder） |
| 熟练运用 | 一般程度使用 | 计划使用 | 不可取代 | 难以取代 | ||
|---|---|---|---|---|---|---|
| AAC 策略 | ||||||
| Alectryon | ||||||
| CompCert | ||||||
| coq-dpdgraph | ||||||
| CoqHammer | ||||||
| Dune | ||||||
| Hierarchy Builder | ||||||
| Interval | ||||||
| Ott | ||||||
| Paco | ||||||
| Paramcoq | ||||||
| PyCoq | ||||||
| QuickChick | ||||||
| SerAPI | ||||||
| SMTCoq | ||||||
| Unicoq |
| 熟练运用 | 一般程度使用 | 计划使用 | 不可取代 | 难以取代 | ||
|---|---|---|---|---|---|---|
| Coq-ExtLib 扩展库 | ||||||
| Coq-std++ | ||||||
| 数学类（Math Classes） | ||||||
| 数学组件（Mathematical Components） | ||||||
| TLC 经典逻辑库 |
| 熟练运用 | 一般程度使用 | 计划使用 | 不可取代 | 难以取代 | ||
|---|---|---|---|---|---|---|
| CoLoR | ||||||
| CoqEAL 代数结构库 | ||||||
| Coquelicot 实分析库 | ||||||
| CoRN | ||||||
| Fiat 密码学库 | ||||||
| Flocq 实数库 | ||||||
| 同伦类型论 HoTT | ||||||
| Iris | ||||||
| UniMath | ||||||
| 软件验证工具链（Verified Software Toolchain） |
| 熟练运用 | 一般程度使用 | 计划使用 | 不可取代 | 难以取代 | ||
|---|---|---|---|---|---|---|
| Logic：经典逻辑、依存型等价关系（dependent equality）、外延性（extensionality）、选择公理（choice axioms） | ||||||
| Structures：代数结构（等价类、有序类型等） | ||||||
| Bool：布尔类型（函数定义及定理） | ||||||
| Arith：基本皮亚诺演算 | ||||||
| PArith：二进制正整数 | ||||||
| NArith：二进制自然数 | ||||||
| ZArith：二进制数 | ||||||
| QArith：有理数 | ||||||
| Numbers：试验性模块化算术架构 | ||||||
| Relations：代数关系（定义及定理） | ||||||
| Sets：集合（经典集合、直觉主义集合、有限集、无限集、幂集等） | ||||||
| Classes：型类 | ||||||
| Lists：多态链表 | ||||||
| Streams：无穷序列 | ||||||
| Vectors：确定维度之向量依存型 | ||||||
| Sorting：公理化排序法 | ||||||
| Wellfounded：良基关系类 | ||||||
| MSets：有限集合基于链表或树的模块化实现，FSet 的现代版 | ||||||
| FSets：有限集合基于链表或树的模块化实现 | ||||||
| Strings：字符串基于 ASCII 字符链表的实现 | ||||||
| Reals：实数形式化 | ||||||
| Array：原生数组类型 |
| 熟练运用 | 一般程度使用 | 计划使用 | 不可取代 | 难以取代 | ||
|---|---|---|---|---|---|---|
| OCaml | ||||||
| Haskell | ||||||
| Scheme | ||||||
| JSON |
你希望将程序抽取到哪些新的目标语言？
| 熟练运用 | 一般程度使用 | 计划使用 | 不可取代 | 难以取代 | ||
|---|---|---|---|---|---|---|
| vio 编译 | ||||||
| vos / vok 编译 | ||||||
用par:选择证明目标 |
||||||
Add LoadPath命令 |
||||||
coqrc配置文件 |
如果你想分享你的coqrc配置，请删除其中个人信息后填入此处。
本节的问题涉及Coq的各种集成开发环境（IDE），内容取决于你在“你使用Coq的情况”中提及使用过的集成开发环境（IDE）。欲查看全部问题，不论涉及的集成开发环境（IDE）是否使用过，可修改下面第一个问题的答案。
针对下列Proof General诸功能，请说明您对该功能的认识和使用情况。对于您不知道和不感兴趣的功能，请选择"拒答"以跳过。
| 使用中 | 知道但不用 | 想要尝试使用 | |
|---|---|---|---|
| 自动对齐 | |||
| 支持Ltac调试模式 | |||
所需库的自动补全 （coq-compile-before-require选项） |
|||
所需库的快速/vos补全（coq-compile-vos选项） |
|||
在本地使用Proof General并在主服务器上运行Coq（通过Tramp实现） |
|||
在写证明的过程中，将证明可视化为树状结构（prooftree） |
|||
在处理大片代码时跳过整段证明（proof-omit-proof-option选项） |
|||
在*response*缓冲区中逐步显示证明项（coq-show-proof-stepwise选项） |
|||
显示各步骤之间证明目标的差别（Proof General菜单中的Set Diffs "on".选项，或Set Diffs "removed".功能） |
|||
按下点号或双点号时自动处理语句（proof-electric-terminator-enable或coq-double-hit-enable选项） |
|||
自动添加Proof using _.语句 |
proof-three-window-enable选项，或M-x proof-three-window-toggle命令）
您是否在~/.emacs中通过自定义项或补丁来修改Proof General/Company-Coq？
如有，请简述你修改了哪些部分，以及是否希望修改的部分成为默认配置？
本节问题仅当您在前文“你使用Coq的情况”中表明自己曾使用过持续集成（CI）时才会出现。请继续回答下一部分问卷。
因Coq在当代英语中的同音词“cock（在英语粗话中，指男性生殖器）”有冒犯性，故Coq社区时常讨论其更名问题。
2021年4月，该话题在Coq社区再次引发讨论，有用户表示其遇到骚扰、分享其身处尴尬的经历，并表示潜在用户因名称而离开此社区。
鉴于当前名称Coq对我们社区的发展与多元化的潜在影响，Coq开发团队在探索更名的可能性（https://coq.discourse.group/t/renaming-coq/1264）。
我们开辟了一个维基页面来收集更名的想法，并发布此调查来征求更名在内的多角度意见。
该调查的结果将供Coq开发团队参考，但并非投票表决。更名与否将由核心开发人员独立决定。
请坦诚作答，而非提交您认为我们想听到的内容，或您认为社会可接受的内容。
| 很喜欢 | 比较认可 | 可以接受 | 不认同 | 厌恶 | |
|---|---|---|---|---|---|
仅将读音改为C.O.Q. |
|||||
使名称更具法国特色 具体而言，您会如何评价以下三种方案？ |
|||||
| LPC（Le Prouveur Coq） | |||||
Le Coq Formel |
|||||
| Le Coq | |||||
把名字加长 具体而言，您会如何评价以下五种方案？ |
|||||
| CoqPIT （PIT 意为：Prouveur Interactif de Théorèmes，法语“交互式定理证明器”） |
|||||
Coquatrix |
|||||
| Coqqio （转写自朝鲜语“꼬끼오”——“Kkokkio”，公鸡叫声的拟声词“咕咕咕”） |
|||||
| Coqorico （法语“cocorico”的重新拼写，公鸡叫声的拟声词） |
|||||
| Copa (Coq Proof Assistant，Coq证明助理) | |||||
把名字改得跟现在大不相同 具体而言，您会如何评价以下四种方案？ |
|||||
| Rocq （“Inria Rocquencourt”的缩写，Coq起源的地方，同样也是一种神话中的鸟的重新拼写：https://en.wikipedia.org/wiki/Roc_(mythology)） |
|||||
| Gallo （公鸡的意大利语单词） |
|||||
| Chook （鸡的澳大利亚方言） |
|||||
| UP（Universal Prover，通用证明器） |
为了提高您使用Coq的工作效率，并鼓励其他人学习和使用Coq，以下诸改进有多重要？
（请基于现状评价改进的重要性，并跳过您没有意见或不了解的项。）
| 必须改进 | 值得改进 | 毋需改动 | 不宜改动 | |
|---|---|---|---|---|
| 新的主要功能 | ||||
| 改进现有语言特性使其更易用 | ||||
| 修复漏洞 | ||||
| 跨版本兼容性与移植 | ||||
| 集成开发环境（IDE） | ||||
| 其他开发工具 | ||||
| 库和软件包 | ||||
| 提升性能 | ||||
| 文档 | ||||
| 社区建设 | ||||
| 获取帮助的平台渠道 |
请阐述上述改进的重要性，以及你认为其他需要改进的方面。另外，如果你使用过其他证明辅助工具，请阐述Coq与之相比表现如何。
（请根据现状评价其重要性，并跳过您没有意见或不了解的项。）
| 必须改进 | 值得改进 | 毋需改动 | 不宜改动 | |
|---|---|---|---|---|
| 讲解各个策略（tactics）和命令（commands） | ||||
| 策略（tactics）和命令（commands）的用例（在文档中或单独的文件中） | ||||
| 解释Coq得报错信息 | ||||
| 讨论在什么情况下运用哪些策略（tactics）和命令（commands） | ||||
| 解释Coq的工作原理（例如：合一“unification”等） | ||||
| 讲解主要特性，如Ltac2和SSReflect | ||||
| 从更高层面概述证明技术，及其在Coq中的应用（例如：针对程序证明有哪些流行的技术和软件包） | ||||
| 讲解标准库 |
下列因素在多大程度上阻碍了您为Coq做贡献的能力或意愿？
| 严重阻碍 | 明显阻碍 | 有点阻碍 | 没有阻碍 | |
|---|---|---|---|---|
| 缺少内部文档 | ||||
| 代码很难理解 / 读起来过于复杂 | ||||
| 提问时得不到充分的帮助 | ||||
| 不知道什么改动会有帮助 | ||||
| 不知道推进改动的潜在难度有多大 | ||||
| 代码审核（Code Review）太久/太困难 |
如有任何不欢迎或不平等对待的情形，不论是过去还是正在发生，欢迎致信Coq行为准则执行团队（coq-conduct@inria.fr）反映情况。对于过去发生的此类情形，请告诉我们问题是否得到解决以及是如何解决的。
为保障举报的匿名性，此题不设回答框。
这是问卷的最后一部分。您需要按页面底部的“提交”按钮以发送回答。
在此之前，如果您能回答下列问题，我们将不胜感激。这将帮助我们可以更好地了解谁在使用Coq以及社区各部分成员的观点有何不同（尽管所有问题都非必答）。
您还可以通过页面底部的文本框，对本次调查提供反馈意见。
感谢你花宝贵的时间参与此项问卷调查。我们对此十分感激！我们将把统计数据发到Coq常见的信息平台上。