Coq Community Survey 2022 feedback

[Zimmi48]

Hello,

There were a few questions related to coq_jupyter in the Coq Community Survey 2022. Here is the information we gathered.

• To the question "Which editors or IDEs have you used for Coq?", 6 respondents said they have used "Executable notebook with coq_jupyter", although 3 more respondents who had answered "No" (probably because they don't use it anymore) provided feedback.

• One of the respondents that answered "No" to the previous question said they have used it for "1-2 years", that they were unsatisfied with it and wrote "It needs a lot of work I'm afraid.".

• Everyone else that answered to the question "How long have you used coq_jupyter?" said they used it for less "than 1 year".

  

• To the question "How satisfied are you with coq_jupyter?", besides the 1 "Unsatisfied", the other answers were 3 "Satisfied" and 4 "Neutral".

  

• To the question "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?", 1 (satisfied user) answered "I use it", 3 answered "I don't use it, but I have tried." and 3 answered "I don't use it and haven't tried."

  

• One user that answered "Neutral" to the satisfaction question and has tried to use it with third party hosting wrote:

  I have tried the Jupyter instance on Binder linked on the webpage, and it is very, very slow to make the server available.
  Also, I tried editing the example but was a bit lost with the feedback I could see. Since the interaction is very slow, it is difficult to provide a constructive feedback, I do not know if what I saw was due to a) incorrect treatment of dependencies between cells b) incorrect update of the output c) incorrect display of the output d) too slow update of the output, etc.

  and:

  May be is it too early to provide a detailed list. But I think this is a great project. For instance it would be awesome to use this to provide a friendly interface to tools like interval. They could thus be used by users less fluent in Coq.

• Finally, everybody that answered to "Have you used coq_jupyter collaboratively (meaning accessing the same instance of the kernel from different machines / by different users)?" said "No".