Supplementary material for the ITP'23 article "Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users"

This artifact contains the supplementary files for the ITP'23 article "Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users". More specifically, it contains:

the Limesurvey structure exported file (Limesurvey/survey-structure.lss);

the HTML print of the survey in English and Chinese (Limesurvey/questionnaire_english.html and Limesurvey/questionnaire_chinese.html);

the Jupyter notebook (Coq-survey-analysis.ipynb) and the Stata code (regressions/Regressions_and_Romano-Wolf.do) that were used to produce the results;

the plots for the answers to all the closed questions, as well as plots for some interactions between answers to multiple closed questions in png and svg formats (assets/);

manual analysis of some open text questions (coded_answers/);

answers to open text questions (open_answers/).

This artifact does not contain the full raw data from the survey. These data have been deleted, following the GDPR compliance statement that was displayed at the beginning of the survey. The open text answers that are made available through this artifact have been sanitized to remove any personally identifiable element.

File listing

README.md: this README

Limesurvey

questionnaire_english.html: survey HTML print in English

questionnaire_chinese.html: survey HTML print in Chinese

survey-structure.lss: Limesurvey structure export

Coq-survey-analysis.ipynb: Jupyter notebook used to produce plots

regressions

Regressions_and_Romano-Wolf.do: Stata code used to do the regressions appearing in the article

assets

many png and svg files for plots showing quantitative results

coded_answers

renaming.md: manual analysis of the answers to the open text question "If you wish to elaborate on why Coq should / should not be renamed, feel free to do it here."

renaming_choices.md: manual analysis of the answers to the open text question "If you wish to share any specific arguments in favor or against some specific name choices, please do so here."

contributing_experience.csv: answers to the open text question "Feel free to elaborate on the contributing experience, what we can do better, or why you do not contribute." with manual analysis

doc_improvements-grouped.docx manual analysis of the answers to the open text question "Feel free to elaborate on any of the items listed above, their importance, etc. Are there other improvements that you think would be important?" (in the context of a question on "How important are improvements to the following aspects of the Coq documentation?")

open_answers: Each table has been reordered and has a different indexing, so relating answers from different tables is not possible. Furthermore, answers have been checked and sanitized to remove any personally identifiable elements.

ci_feedback.csv: answers to the question "If you have general feedback on CI in the Coq ecosystem, feel free to share it here." Also shared at: https://github.com/coq-community/manifesto/issues/141

contributing_experience.csv: answers to the question "Feel free to elaborate on the contributing experience, what we can do better, or why you do not contribute."

coqide_improvements.csv: answers to the question "What improvements, bug fixes and new features would you most like to see in CoqIDE?" Also shared at: https://github.com/coq/coq/issues/16580

coq_improvements.csv: answers to the question "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." (in the context of a question on "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?")

coqtail_improvements.csv: answers to the question "What improvements, bug fixes and new features would you most like to see in Coqtail?" Also shared at: https://github.com/whonore/Coqtail/issues/277

distracting_company_coq_features.csv

doc_improvements.csv: answers to the question "Feel free to elaborate on any of the items listed above, their importance, etc. Are there other improvements that you think would be important?" (in the context of a question on "How important are improvements to the following aspects of the Coq documentation?")

extraction_targets.csv: answers to the question "If you're interested in new extraction targets, which languages do you want?" Also analyzed quantitatively in: assets/extraction-targets-barplot.png

jscoq_improvements.csv: answers to the question "What improvements, bug fixes and new features would you most like to see in jsCoq?" Also shared at: https://github.com/jscoq/jscoq/issues/261

jupyter_improvements.csv: answers to the question "What improvements, bug fixes and new features would you most like to see in coq_jupyter?" Also shared at: https://github.com/EugeneLoy/coq_jupyter/issues/46

jupyter_support.csv: answers to the question "Have you had any issues or lack of support for coq_kernel for any service? If so, feel free to share here." Also shared at: https://github.com/EugeneLoy/coq_jupyter/issues/46

languages.csv: answers to the question "What languages would be the most useful to support?" Also analyzed quantitatively in: assets/languages-barplot.png

learning_experience.csv: answers to the question "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?"

proof_general_customizations.csv: answers to the question "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?" Also shared at: https://github.com/ProofGeneral/PG/issues/671

proof_general_improvements.csv: answers to the question "What improvements, bug fixes and new features would you most like to see in Proof General?" Also shared at: https://github.com/ProofGeneral/PG/issues/671

renaming.csv: answers to the question "If you wish to elaborate on why Coq should / should not be renamed, feel free to do it here."

renaming_choices.csv: answers to the question "If you wish to share any specific arguments in favor or against some specific name choices, please do so here."

survey_issues.csv: answers to the question "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?"

vim_compatibility.csv: answers to the question "What Vim / NeoVim features or plugins would you like to have better integrated with Coqtail? " Also shared at: https://github.com/whonore/Coqtail/issues/277

vscoq_improvements.csv: answers to the question "What improvements, bug fixes and new features would you most like to see in VsCoq?" Also shared at: https://github.com/coq-community/vscoq/issues/308