coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Théo Zimmermann <theo AT irif.fr>
- To: Coq Club <coq-club AT inria.fr>
- Subject: [Coq-Club] Summary of results from the Coq Community Survey 2022
- Date: Fri, 9 Sep 2022 11:56:04 +0200
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=theo AT irif.fr; spf=Pass smtp.mailfrom=theo AT irif.fr; spf=None smtp.helo=postmaster AT korolev.univ-paris7.fr
- Ironport-data: A9a23:oDTlfKq9nQjceK5EOaCpSpkE7gVeBmI5YxIvgKrLsJaIsI4StFCzt garIBnXOP+CYGajctF2YY+1oBkB6sLczoJlSQJvri49Qi1B+OPIVI+TRqvSF3PLf5ebFCqLz O1HN4KedJhsJpP4jk3wWlQ0hSAkjclkfpKlVKicfHoZqTZMEE/Nszo68wICqtMu0IPR7z+l4 4uo+ZWOYA79glaYD0pNg069gEM31BjNkGhA1rAOTagjUIj2yhH5pLpGTU2AByOQrrt8RoZWd M6fpF2NxV41yj92Yj+TfhkXRWVRKlLaFVDmZnO7wMFOiDAazsA5+v5T2Pbx9S67hh3R9+2dx umhurS7ZjwTE6mSm9gPWjp0N35XF4pgoJ3YdC3XXcy7lyUqclPvxO9pCEwoe5Ae+/gyGWhU9 OdHbj4XBvyBr7vnnPThF7Uq2J1ldZK7VG8ckikIITXxEfYrRrjCWaTEo9FCtNs1rp0URamCO ZtAAdZpRFfjPwxWGmoyNL8dzLulmn7PYnpHgV3A8MLb5ECKkF0gj+iyWDbPQfSBQtwQlUKFr Erd7mHhC1cbMsaewHyL6BqRavTnniThX4YfCvul8P90xUWa3G0IV1sYTzNXvMVVlGa1dOllB khK+RY8pIse0BOCZP7bBz+n9SvsUgEnZ/JcFOgz6Qeow6XS4hqECmVscgOteODKp+dqFWxxj AXhc8fBX2A37+D9pWe1rO/MxQ5eLxT5OkcsX0fopyM96sPiu+nfZTqQE446TMZZYvVe/zX9h jyH6QYkjrMYgKY2O0SHEbLv3WLESnvhF15dCuDrsoSNtVMRiGmNO9bA1LQjxawcRLt1t3HY1 JT+p+CQ7foVEbaGnzGXTeMGEdmBvqjbamOC2A40QMhwr1xBHkJPm6gOulmSw283b645lcPBO h6L0e+szMMDbCXwMvUfj3yZWp93k8AM6ugJptiNMosfPcguHON21DtjY0eM0nqFraTfuf9XB HtvSu71VSxyIf0/klKeHr5NuZd2mHxW7T6NFPjTkU/9uZLAPyH9dFvwGADTBgzPxPjY+1q9H hc2H5fi9iizp8WiPHaMqdNIcg5iwLpSLcmelvG7v9WremJOcFzNwdeImdvNoqRpwPZYkPnm5 Ha4VhMKwVbznyKVKB+LZDZtcuq3D5p4qHs6Ow0qPEqpgiR4ONv1vPtGJpZnL6M68OFDzOJvS 6VXccu3BPkSGC/M/C4QbMWgoYE7LEariAuCMjCLej86e5I8FQXF9sW7LAr19SdIADDu7Zkyp Lip1wX6R5sfRl0+V5+LMqLzlgK85CFPlvhzUk3EJshoVH/tqIU6eTbsivIXIt0XLUmRzDWt0 QvLUwwTovPAotNo/dTE2fKEooOuH7csF0ZWBTOBv7WxLy7e83Tl3IlBTqOQdCrcTzyy9r/7P bdZyPT1MfsmmldWstMkSuw7k/lgv4Pi9+1A0wBpPHTXdFD1WLluFXmxwpUdvKN6wLIE6xC9X ViC+4QENOzRat/lClMYOCEscv+HiaMPgjDX4Plpcl/24jR7oOiOXUlIZUPeiytHK794LsU4x +Y//dYf8Q2k1VwkKI/e3CxT8m2NKF0GUrkm78lDWt+10VRzklwSM4bBDiLW4Y2Ub4seOEcdI giL2PjIiYNayxeQaHE0D3XMgLRQ3MxcpBBQwVYeDF2Vgd6Z1OQv1Rhc/Dlfot65FfmbPzaf+ 1SHNnGZ4Y2N+C1vgMVdGX2qGh8EHBSD+1eujVUT/IEco49ESUSVRFDR+87UlKzaz46YVjlB/ b/exnyNvfPCYpTqxiVrMaJ6g6WLcDGynzEuXOimBcWLWZcgCdYgbmlCekJQwyba7QgNaIEra AWkECucqUE2CMLIn5AGNg==
- Ironport-hdrordr: A9a23:kqbEoKFVgAync70EpLqEW8eALOsnbusQ8zAXPiFKOGFom6mj+/ xG885rsyMc5AxhP03I+urwXJVoI0msjaKdiLN5VdzJMWeG2FdAR7sSlrcKrQeQYREWNdQttp tIQuxRDNXxCBxdlsb14A6xFpIFzMOc+K6lwcfypk0dND2Cp5sQjTuQhWugYzEGOzVuNN4cFJ +A6tFKqlObCApnH/hTz0N1OtQreOelqLvWJR1DDR8k7AGPiHeF76H3Fh6Axxt2aUI+sMQf2F mAkEjy56emu/G/jiXX0XTehq4m6qqV9vJzQM/JgMkWLj3tj0KTeYx9R6fqhkFA0ZaS1Go=
- Ironport-phdr: A9a23:Eex9KByN+upR3FTXCzLdwVBlVkEcU1XcAAcZ59Idhq5Udez7ptK+Z heZvq0wxwWTFazgqNt8w9LMtK7hXWFSqb2gi1slNKJ2ahkelM8NlBYhCsPWQWfyLfrtcjBoV J8aDAwt8H60K1VaF9jjbFPOvHKy8SQSGhLiPgZpO+j5AIHfg9q52uyo9ZDffwVFiDWjbb9sM R67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84T aFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QKsqUjq+8 ahkVB7oiD8GNzEn9mHXltdwh79frB64uhBz35LYbISTOfFjfK3SYMkaSHJOUchRWSJPAZ6yY ZUTAOcaJ+lUs5PwqkESoReiBwShAv7kxD9Shn/x2K03y/ovEQHc2wwnB90Bs3XUrNDwNKgMS +C1ybPHzTPFb/hL3jr99IjIfQ4mofyXXLJwa8vRyUc1GwPLlFWdsIroNC6a2eoRqWaU9fZgV f6xhG49rQF8ujyiyMgihIXVmo8YylDJ+DlkzIs6ONC1VVJ3bN+qHpdMuSyXM4R4T8A/T2x2t is31qMKtJC1ciUIyJoqxxDRZvKBfoOV7BzjU+ORLi15hHJjYL+wmhey8VO8xe37S8m0yk1Ko TRfntnDrHAN0AHT6tCBR/Bg/UmhwS6C2x3X5+xLO0w4i6rWJpE7zrMxi5Yfq1nPEyH1lUnuk qOaakEp9vKr5unneLnquIGQO5Fuhg3jMakih8qyCvkiPAcURWiU4+G82aXj/ULnRLVKieU7k qresJDAIsQborC2AxFP3oY+7Ra/Dimm3M0AnXYdNlJFeQmHgorzN1HAOvD0Ffa/g1Kynzd33 /3KI7nsD5rXInTdkLrscqxx5k9BxAYp0NxS6ZFZBqkEIP3pW0/xsNLYDgU+Mwyx2+vnFNV92 Z0ZWW+UA6+ZKqLSsVGS6uIhOemAfIkVty3lJPg/+/HulWM5mUMafaSxwJcbcGq4Eeh+I0WFf Xrshc8MHnsNvgonVeDllFmCUSNIaHupRKI95jQ7CJq8AovZR4CthqaB3CahEZFMaGBGEAPEL XC9XIKdE9wIdSjadsRmi3kPUaWrY44nzxCn8gHgnelJNO3RrxEYNJXU5tlw4uDJkBg083QgE 8SQ1EmMVWB62G0SEWxllJtjqFBwnw/QmZNzhOZVQJkKv6shumYSMJfdy7Y/ENXuQkfbedzPT l+6Q9KgCDV3T9QrwtZIbVwuU866gEXl2CynS6QQi6TNHIY9p77c0n/ZJtx8xTDIzvpplEEoF /NGLnbunatj707WDo/NnV+ekvO2dakb9C/X9WnFw3Dd9FpAXltWVqPIFWsaelOQrdn94RbaS KSyDL08LgZb4c2FMKxOZ8OvkFNHWrL7Mc7feD33lX3Y6Q+g4LSKYcKqfmwc2H+YE00Yi0UJ+ n3AMwEiByCnqmaYDTp0FFupbVm+ue954Gi2SEM51WToJwVoyqa19xgJhPedV+Jb37QKvz0ko il1G1D11szfCt6JrQ5sNKtGZtZ17FBC3GPf/wtzW/7oZ7xii1k2ch52sQXgzVQ/C4lNl9Qrs GJ/1BB7euqT1FJMcS/d3IilY+yLbDOvoFbxMuiPgQGNtbTesr0C4/k5tVj56QSgF054tm5iz 8EQyXyXoJPDEAsVV5v1FEcx7Rlz4b/AMUxfr8vZ02NhNa6sv3rMwdUsUaE5yhunV9ZFMa3CG hW4QIUKQtOjLuAngQ3jchIJO8hT7q86ec28PajjuubjLKNrmzSoin5C6YZ23xeX9iZyfeXP2 o4M3/CS2gbvuy7UtF66qYi3nIlFYWtXBW+j0W3+A4UXYKRufIENAGPoIsutx9w4iYS/E3Jf8 VeiARsB1qrLMVKOb1H69QxK1EpRr2bvlSajzjNymi0kteLGjXCImbm+MkRefDcQFCFrlh/0L JKxjswGUUTgdAUvmBa/pCOYj+BaqKl5M2jPUBJNdinyIXtlV/j4vb6DbshTrZIw5HwGDKLmP AzcFOe7+kBKgEaBVyNEyTs2di+noMD8lh1+0ieGKWpr6WDecod2zAve49rVQbhQ2CAHTW92k 2qyZBD0Mt+38NGTj5qGvPq5UjfrSp1edgHq14KO8iWhrz4iEVikkva/l8eyWxQ63CjT1sNrW 2PGtlyvB+ujn7T/OuVhcE5yAVb64McvAYBynLw7g5QI0GQbjJGYrjIX1H3+OtJB1efifWIAE HQVlsXN7lGviygBZjqZgpj0XXKHzo59asmmNykIjzkl4ZkCDbfcu7VAmWEdTkOQiwXXbLA9m z4czaFr83sGm6QTvwFryCyBA7cUFE0ePCr2lh3O4crs5KNQLH2id7S9zi8c1ZioEa2CrwdAW X34ZoZqHCl+6d96OU7N13u745/ted3ZZ9Ye/hOOlBKIg+9QIZM33v0E4EgvcXr6pmEgwvUng AZG3pagu4yKNSNw+qOnRwZRLDzuOIUd4HCljKpTmNqXw5H6HphlHWZuPtOgRvapHTQO8PX/Y l/fTHtm9yvdR+OZRFTPuyIE5zrVHpumNm+aPiwcxNRmHlyGIVBHxRoTV3M8l4I4EQajwIrgd l1473Yf/A2dyFMEx+R2Oh34Smqaqh2vb2J+VJiSKzJX9ABMoUnPe5/7jKo7D2RD85utoRbYY HScfBhNBHoVV1asBFf5Ob2j+5/d9emGQ/K3NfrVPvOAs6YNMpXAjYLq2Yxg8TGWM8yJNXQ3F Pw31H1IWnVhEtjYkTECI8TyvyPXbsDdqg3uokWfT+i89+7sXA/xo5aJCqUXKdx1+gvpx6mZZ bb4bMlRKCxZ2NUC3y2RoIU=
- Ironport-sdr: jRwugUDpOoTseWotLYLkrCOwMvdtKa3ScmZyiXaySP09KfThtI994iTkjPHKFlr0qiVwltiDlr wIJV6Drf1mUqJb8WL+nWahAumwFJx71GnvAVNFsjvErN40189W+UbgbBtRsjjHeAFESnTX/oHa JC6wI+w3LeXEEKN+SqYeXwaSq8jRqCtaHM+UnXYY0UHRbM6PYKn/q1O6Muhc5/4BGSFOF81XYv Wlxj9dtoT5763PBQZsLy/MWjXAUKGImlQ8963pS14YGvuu6AQkxKZlC0DWQqA474g3MrZOSFFS FOaj3ZRcTsoqYj5ikU8Qvvfa
Dear Coq-Club subscribers,
The Coq Community Survey 2022 was an online public survey conducted during February 2022. Its main goal was to get an updated picture of the Coq user community and inform future decisions made by the Coq team and other Coq ecosystem participants. The survey was advertised to Coq users primarily via the Coq Discourse forum, the Coq Zulip chat, Coq-club mailing list, Coq Twitter, and the Coq website. On behalf of the Coq Community Survey working group, I would like to thank everyone that participated by responding to the survey.
The survey was available in English and Chinese, and had 109 questions, some of which were only visible depending on answers to previous questions. Answering was optional for all survey questions, and most questions allowed free-text answers. The survey received 466 responses, and the survey working group (WG) has collaboratively produced three posts that summarize responses.
Post 1: Who is using Coq and in what context? (https://coq.discourse.group/t/coq-community-survey-2022-results-part-i/1730)
This post examines the demographics of the Coq users who took the survey, and in what context they are using Coq. "Context" here means users' experience before they started to use Coq, their reasons for using Coq, and their experience with related languages and tools.
The demographic responses suggest that the Coq community is tilted toward computer science, not least in educational background and application areas. France and the United States are where half of the respondents are located, but we observed more diversity in the locations of newcomers.
Post 2: How people are using Coq (https://coq.discourse.group/t/coq-community-survey-2022-results-part-ii/1746)
This post examines how respondents use Coq on a daily (or weekly or yearly) basis. This includes the Coq version and IDE, and software infrastructure such as operating system and package management.
The responses suggest that most Coq users run Linux-based systems and directly use the opam package manager. Emacs (with ProofGeneral) remains the most popular Coq code editor, but is closely followed by CoqIDE and VS Code.
Post 3: Usage of Coq features, tools, and libraries (https://coq.discourse.group/t/coq-community-survey-2022-results-part-iii/1777)
This post examines responses related to Coq features, Coq-related plugins and tools, and Coq libraries, in particular their respective popularity and criticality.
The responses suggest that Coq's typeclasses are relatively popular (trailing inductive types and modules as a language feature), that the Dune build system is gaining users, and that Mathematical Components is the most popular general library besides Coq's standard library. In addition, proof automation tools such as CoqHammer and SMTCoq, and modern tactic languages such as Ltac2, currently have few users, but many prospective users.
The Coq Community Survey 2022 was an online public survey conducted during February 2022. Its main goal was to get an updated picture of the Coq user community and inform future decisions made by the Coq team and other Coq ecosystem participants. The survey was advertised to Coq users primarily via the Coq Discourse forum, the Coq Zulip chat, Coq-club mailing list, Coq Twitter, and the Coq website. On behalf of the Coq Community Survey working group, I would like to thank everyone that participated by responding to the survey.
The survey was available in English and Chinese, and had 109 questions, some of which were only visible depending on answers to previous questions. Answering was optional for all survey questions, and most questions allowed free-text answers. The survey received 466 responses, and the survey working group (WG) has collaboratively produced three posts that summarize responses.
Post 1: Who is using Coq and in what context? (https://coq.discourse.group/t/coq-community-survey-2022-results-part-i/1730)
This post examines the demographics of the Coq users who took the survey, and in what context they are using Coq. "Context" here means users' experience before they started to use Coq, their reasons for using Coq, and their experience with related languages and tools.
The demographic responses suggest that the Coq community is tilted toward computer science, not least in educational background and application areas. France and the United States are where half of the respondents are located, but we observed more diversity in the locations of newcomers.
Post 2: How people are using Coq (https://coq.discourse.group/t/coq-community-survey-2022-results-part-ii/1746)
This post examines how respondents use Coq on a daily (or weekly or yearly) basis. This includes the Coq version and IDE, and software infrastructure such as operating system and package management.
The responses suggest that most Coq users run Linux-based systems and directly use the opam package manager. Emacs (with ProofGeneral) remains the most popular Coq code editor, but is closely followed by CoqIDE and VS Code.
Post 3: Usage of Coq features, tools, and libraries (https://coq.discourse.group/t/coq-community-survey-2022-results-part-iii/1777)
This post examines responses related to Coq features, Coq-related plugins and tools, and Coq libraries, in particular their respective popularity and criticality.
The responses suggest that Coq's typeclasses are relatively popular (trailing inductive types and modules as a language feature), that the Dune build system is gaining users, and that Mathematical Components is the most popular general library besides Coq's standard library. In addition, proof automation tools such as CoqHammer and SMTCoq, and modern tactic languages such as Ltac2, currently have few users, but many prospective users.
The WG welcomes feedback from the Coq community, in particular on suggestions for improvements or questions that could be answered with the survey data. Other blog posts as well as more formal publications may follow to complete the analysis of the results.
Théo Zimmermann, for the Coq Community Survey 2022 working group
- [Coq-Club] Summary of results from the Coq Community Survey 2022, Théo Zimmermann, 09/09/2022
Archive powered by MHonArc 2.6.19+.