Stream: User interfaces devs & users

Topic: Next Coq UI researchers discussion: July 24


view this post on Zulip Benjamin Pierce (Jun 23 2023 at 17:52):

Looks like July 24th from 3-5 PM Paris time (= 9-11 US Eastern) is a good slot for our next discussion of user interface research in Coq. We'll use this Zoom link.

The current proposal is to use this meeting for community members to tell each other and the Coq team about research projects they are working on or contemplating. Jessica Shi (from Penn) can talk about her project on interface improvements for proof understanding.

Anybody else want to join in?

view this post on Zulip Karl Palmskog (Jun 23 2023 at 18:00):

we found out in a recent topic that there is a perception among (some) AI researchers that Coq is difficult to interface with for AI applications.

This is not about graphical UI at all, but it would be interesting to hear if people have ideas how to better market the various Coq low-level UI research (LSP, PyCoq, etc.) to the AI community.

So if this would be considered in scope for the meeting, I'd be happy to join.

view this post on Zulip bubble sort now (Jun 24 2023 at 01:33):

since this is a free speech forum my take is coq-lsp development is going well and as it uses the standard LSP protocol it is pretty easy to interact with. while I don't have any ideas to improve coq-lsp yet, I believe it should be marketed as a "platform for research". some folks should build a prototype using coq-lsp. it doesn't even have to be AI/ML, it can just be another user interface that is creative in one way or another. and that'll bring some attention to coq-lsp as a "platform for research" and not just a replacement for vscoq1 and coqide. I myself am doing a funny project that tries to connect coq-lsp and OpenAI API, I'm not sure how successful it will be but at least it'd be something that we can learn from

view this post on Zulip Jelle Wemmenhove (Jul 13 2023 at 13:55):

@Jim Portegies and me are developing a user interface for use in education. The current version (see https://github.com/impermeable/waterproof) uses Coq SerAPI, but we are finishing a new version that uses coq-lsp.

Perhaps we can talk about this project during the next discussion as well?

view this post on Zulip Benjamin Pierce (Jul 18 2023 at 20:17):

One of the projects that had planned to present on Monday wants to wait a few weeks, so I am wondering (a) whether anybody else wants to present on Monday or (b) whether a presentation of the new Waterproof version (plus one other short presentation) is enough to fill a useful hour. If either answer is yes, then let's go ahead as planned (next Monday, July 24, at 3PM Paris time). If both are no, perhaps we should reschedule for September...

Jim and Jelle, what do you think about (b)?

Does anybody else want to present their project to this group?

view this post on Zulip Théo Zimmermann (Jul 18 2023 at 20:38):

I won't be available on Monday, but I would be really interested to see a recorded demo of Waterproof.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 19 2023 at 12:15):

ccing @Jim Portegies @Jelle Wemmenhove so they do get notified.

view this post on Zulip Benjamin Pierce (Jul 20 2023 at 16:24):

Thanks, Emilio. Looks like Jim and Jelle may be offline this week. Since the short presentation that I had thought was queued up for Monday is also not quite ready, I propose that we skip this meeting and reschedule for September.

(Since people's plans for September might not be set yet, I'll wait a few weeks to post a new when2meet, aiming for second half of September.)

Any objections to this plan?

view this post on Zulip Enrico Tassi (Jul 20 2023 at 19:53):

No objection here.

view this post on Zulip Jim Portegies (Jul 24 2023 at 09:11):

I am sorry, I was indeed offline for a few days. We are okay with the plan to reschedule for September

view this post on Zulip Emilio Jesús Gallego Arias (Jul 24 2023 at 09:41):

Sounds good to me @Benjamin Pierce , thanks


Last updated: Oct 13 2024 at 01:02 UTC