Coq Community Survey 2022 feedback.

[Zimmi48]

The Coq Community Survey 2022 included some questions on IDEs.

40 people have checked the "jsCoq" box in the question "Which editors or IDEs have you used for Coq?". Of those, 35 provided more info in the IDE-specific section + 2 who had not checked the box (one of them being a user who uses it only for teaching, and the other one being a non-user who would like to use it for teaching with UniMath).

To the question "How satisfied are you with jsCoq?", the answers were:

• 5 very satisfied
• 18 satisfied
• 10 neutral
• 1 unsatisfied

To the question "How long have you used jsCoq?", the answers were:

• 19 "less than 1 year"
• 8 "1-2 years"
• 8 "2-5 years"

To the question "What have you used jsCoq for?", the answers were:

• 13 "Casual proof development" (including one who adds "Learning Coq online")
• 7 "Casual proof development" + "Sharing snippets" (including one who adds "Using Coq impromptu on mobile device")
• 3 "Teaching" (including one whose exact answer is "introduce people to Coq within hours")
• 2 "Sharing snippets"
• 2 "Sharing snippets" + "Embedding in HTML documents"
• 2 "Casual proof development" + "Embedding in HTML documents"
• 2 "Casual proof development" + "Sharing snippets" + "Embedding in HTML documents"
• 1 "UI/UX Research"
• 1 "Casual proof development" + "Sharing snippets" + "Embedding in HTML documents" + "Teaching SF"
• 1 "Embedding in HTML documents"
• 1 "Embedding in HTML documents" + "Teaching"

Note that "Teaching" was not among the predefined answers, so it's likely that even more people would have selected it if it had been.

Here is the general feedback that was shared on jsCoq (the question was "What improvements, bug fixes and new features would you most like to see in jsCoq?"):

• I think the tool has a lot of potential, but at this time I do not use for larger projects

• I would like to be able to load the UniMath library with jsCoq for teaching

• support for mutiple-file projects

• Much more intuitive user interface. It took me weeks until I understood where can I write and how to submit that to Coq.

• The sharing feature is super difficult to find!

• Ability to store Coq files locally.

• I have kept up with jsCoq even less than with PG. But it would be great if it could work on entire projects uploaded by the user.

• Just performance

• Difficult to load and save files, but very handy to discover complex frameworks without fighting with installation issues.

• Speed

• This is more of a broad idea / dream than a concrete issue, but I think jsCoq could become (part of) an even more powerful tool for teaching and popularization if it could one day support Markdown cells as well as Coq cells, in the vein of Jupyter Notebooks for Python code, or also "Observable" notebooks.

  I should say I have not yet tried embedding in HTML documents but a user interface that would allow you to directly start writing (like notebooks) rather than having to go into HTML mode, could be a great asset.

• One VERY important thing: it should be fully compatible with coqdoc.

  For example, it should understand proofs hidden through (* begin hide *) and (* end hide *), so that these proofs can be displayed when they are hidden and they need to be checked when skipping them and going forward. I once had something that was written with the intent of coqdoc converting it to a static HTML page and tried to make it work with jsCoq and it failed precisely because jsCoq didn't correctly handle (* begin hide *) and (* end hide *)

• Still in beta, can improve lots of stuff, including persistence

[corwin-of-amber]

@ejgallego this is valuable feedback that we should store somewhere, although perhaps an issue thread is no the best location. Should we make a subdir of docs and place such documents there? In particular, the coqdoc hide directives can be its own issue.

[ejgallego]

Indeed, I guess it makes sense to move to documentation the bits that are documentation, and turn into issues the items that are actionable.