Benjamin Pierce (Feb 05 2023 at 22:32): Benjamin Pierce (Feb 05 2023 at 22:32):At the end of the recent discussion at the Coq Working Group about the future of Coq UIs, we decided to meet every few weeks for a while, for a couple of hours at a time, to delve deeper into ongoing technical developments in this area.
If you'd like to join in the first of these discussions, please fill in your availability here before next weekend (Feb 11), so we can choose a time that works for as many people as possible.
See you there!
- Benjamin
Jim Fehrle (Feb 12 2023 at 01:44):Benjamin Pierce said:
At the end of the recent discussion at the Coq Working Group about the future of Coq UIs, we decided to meet every few weeks for a while, for a couple of hours at a time, to delve deeper into ongoing technical developments in this area.
If you'd like to join in the first of these discussions, please fill in your availability here before next weekend (Feb 11), so we can choose a time that works for as many people as possible.
Potentially this discussion is very interesting since I've made some UI enhancements to CoqIDE (proof diffs, the visual Ltac debugger) and I've done a lot of GUI work in my career. But I've been in the dark about these meetings and there was no response to my query in this thread on Oct 17. Perhaps someone would fill me in at least a little bit?
Benjamin Pierce (Feb 12 2023 at 20:35):@Jim Fehrle wrote:
Potentially this discussion is very interesting since I've made some UI enhancements to CoqIDE (proof diffs, the visual Ltac debugger) and I've done a lot of GUI work in my career. But I've been in the dark about these meetings and there was no response to my query in this thread on Oct 17. Perhaps someone would fill me in at least a little bit?
Sorry for not responding to your earlier query, Jim. The discussion at the Coq WG was pretty informal -- mainly just people giving each other high-level overviews of what they are working on and interested in. Here are the people that gave short presentations:
Introductions
Maxime Dénès, Romain Tetley, Enrico Tassi
VsCoq2
Emilio Gallego
LSP, etc.
Yves Bertot
various
Nick Behr
CoREACT ANR project, starting in March 2023 (with Emilio and Yves)
Clément Pit-Claudel
Plans for Coq UI research
Jessica Shi
Demos and part of an upcoming PLATEAU talk
Jesper Bengtson
Merging IDEs for proof assistants and programming languages
Benjamin Pierce said:
Sorry for not responding to your earlier query, Jim. The discussion at the Coq WG was pretty informal -- mainly just people giving each other high-level overviews of what they are working on and interested in. Here are the people that gave short presentations:
No worries. If this was an online meeting, is there a recording available? Was that the Jan 31 meeting? Were there more than 2 meetings? If possible, I'd like to briefly present my interests and share a few related thoughts. Are there any goals for the discussions beyond a sharing of information?
Benjamin Pierce (Feb 13 2023 at 20:25):No worries. If this was an online meeting, is there a recording available? Was that the Jan 31 meeting? Were there more than 2 meetings? If possible, I'd like to briefly present my interests and share a few related thoughts. Are there any goals for the discussions beyond a sharing of information?
Yes, this was Jan 31. There has only been one meeting on this topic so far. The goal of that one was to make sure that all the people both in the core coq dev team and in the larger academic universe know about each other's activities. The goal of the next couple (starting March 21) is for the core devs to explain relevant infrastructure like LSP so that others can take advantage of it.
If you or anyone else that wasn't at Jan 31 want to make short presentations (5-10 min) during the second hour of the March 21 meeting, that would be fantastic. I'll be assembling the schedule again, I guess.
Jim Fehrle (Feb 13 2023 at 21:06):There's no recording of the Jan 31 meeting?
Enrico Tassi (Feb 13 2023 at 21:11):We used webex, which is capable of recording. I believe @Matthieu Sozeau was hosting the session, if there is a recording, he has access to it.
Matthieu Sozeau (Feb 13 2023 at 21:56):There are links to the recordings on the wiki page, they’re on YouTube
Tomás Díaz (Feb 14 2023 at 03:25):I was watching it myself, so here it is for anyone interested : https://www.youtube.com/watch?v=xo90TbokgW4
Jim Fehrle (Feb 15 2023 at 19:01):Benjamin Pierce said:
If you or anyone else that wasn't at Jan 31 want to make short presentations (5-10 min) during the second hour of the March 21 meeting, that would be fantastic. I'll be assembling the schedule again, I guess.
The WG session was titled "Research topics ..." I have no plans to do anything I'd consider research. If I give a short talk, it would be about identifying and addressing some of the obvious unsupported use cases and bugs in CoqIDE and other IDEs. Some of these may helpful or necessary for others' efforts. (I'd like to create a prioritized list of the most-needed improvements with input from others.) And I'll have a few other thoughts. Would that be of interest?
Benjamin Pierce (Feb 17 2023 at 18:49):The WG session was titled "Research topics ..." I have no plans to do
anything I'd consider research. If I give a short talk, it would be about
identifying and addressing some of the obvious unsupported use cases and
bugs in CoqIDE and other IDEs. Some of these may helpful or necessary for
others' efforts. (I'd like to create a prioritized list of the most-needed
improvements with input from others.) And I'll have a few other thoughts.
Would that be of interestThe WG session was called that because the hope was to bring together core
folks working on developing Coq with others doing longer-range
researchy stuff in the UI domain. We had presentations from both sides,
and I'm sure people would like to hear your thoughts, whichever side they
fall on. :-)
>
Last updated: Oct 13 2024 at 01:02 UTC