Stream: Coq Hackathon and Working Group, Winter 2022

Topic: Upcoming workgroup session: jsCoq and CoqDB

Hanneli Tavante (Mar 22 2022 at 14:28):

Hi everyone,

We are organizing an upcoming Coq Hackathon and workgroup session to work on two topics: jsCoq (see the Wiki section here) and the initial implementation of "CoqDB", an attempt to develop a unified framework where information about Coq objects and metadata can be handled (see the Wiki section here).

At this time, we would like to define the date for this upcoming event. Please use this Doodle to select the option(s) that is (are) most convenient for you.

We are looking forward to seeing you in our next work session!

Hanneli Tavante (Mar 24 2022 at 13:04):

I sent a reminder to see if we get a few more answers for the poll, but it looks like next Thurs, March 31st, is going to be the winner.

Hanneli Tavante (Mar 25 2022 at 15:46):

@Emilio Jesús Gallego Arias Is there any pre-established platform for these workgroup sessions? Shall we use the same settings from last session (BBB)? Thanks!

Emilio Jesús Gallego Arias (Mar 28 2022 at 12:53):

Hi @Hanneli Tavante , I am not so happy with BBB, I am wondering if we should instead use Zoom, what do you think?

Emilio Jesús Gallego Arias (Mar 28 2022 at 12:53):

For example BBB videos have been a pain to put in youtube

Hanneli Tavante (Mar 28 2022 at 13:04):

@Emilio Jesús Gallego Arias I agree BBB does not have the best interface, and if uploading the recording to YT is painful, then we probably should use something else.
I think zoom is fine - I'm assuming we'll mainly work in a breakout-room style?

Emilio Jesús Gallego Arias (Mar 28 2022 at 13:08):

If you like Zoom too, I'd say zoom it is going to be. Yes, we can have a main session and breakout rooms

Emilio Jesús Gallego Arias (Mar 28 2022 at 13:08):

Yes BBB can't export video, I think that's a dealbreaker. Pity

Emilio Jesús Gallego Arias (Mar 28 2022 at 13:09):

@Hanneli Tavante I propose I do a reminder today, then we announce the date tomorror afternoon for example?

Hanneli Tavante (Mar 28 2022 at 13:09):

Cool, shall I create a link using my own Zoom account?
I'm happy to do that + update the Wiki and send out session info on Twitter + Mailing list

Hanneli Tavante (Mar 28 2022 at 13:10):

Sorry, I think we need to announce it all right away, bc the winner was this Thursday, Mar 31st
(I kinda realized there was not much time left, sorry about the bad planning)

Emilio Jesús Gallego Arias (Mar 28 2022 at 13:24):

Give me 20 mins @Hanneli Tavante

Théo Zimmermann (Mar 28 2022 at 13:27):

Do you have a paid Zoom account Hanneli? Otherwise, Emilio can do it from his university Zoom account.

Hanneli Tavante (Mar 28 2022 at 13:30):

I also have a premium account from my university. I think the only difference would be having a zoom link with the name of my local institution vs a zoom link holding the name of your institution

Emilio Jesús Gallego Arias (Mar 28 2022 at 13:33):

Ok then we can use the zoom you prefer. So I suggest:

• I send a coq-club reminder right now.
• We announce later today, I'll be online tonight so maybe afternoon your time @Hanneli Tavante you can do the full announce?

Hanneli Tavante (Mar 28 2022 at 13:37):

I have a draft message; I can share it here in about 10min @Emilio Jesús Gallego Arias

Hanneli Tavante (Mar 28 2022 at 13:41):

Hi everyone,

Our next Coq Hackathon and [workgroup session](https://github.com/coq/coq/wiki/jsCoq--and-CoqDB-Working-Day) is happening this **Thursday, March 31st, 14h00 Paris time** (08h00 NYC time - 05h00 Seattle time). Please join us! We'll be focusing on two topics: [jsCoq](https://github.com/jscoq/jscoq) (see the Wiki section [here](https://github.com/coq/coq/wiki/jsCoq--and-CoqDB-Working-Day#jscoq-general-discussion)) and the initial implementation of "CoqDB", an attempt to develop a unified framework where information about Coq objects and metadata can be handled (see the Wiki section [here](https://github.com/coq/coq/wiki/jsCoq--and-CoqDB-Working-Day#coqdb)).

This will be an entirely virtual session held at Zoom. Meeting link will be shortly added to the event's Wiki. Meanwhile, please add your name to the participants' list, and fill the respective sessions with topics you'd like to discuss and work on.

We are looking forward to seeing you in our next work session! If you have any questions, do not hesitate to ask them at [Zulip](https://coq.zulipchat.com/#narrow/stream/256336-jsCoq/topic/jsCoq.20Hacking.20event).

Hanneli Tavante (Mar 28 2022 at 13:42):

WDYT?

Emilio Jesús Gallego Arias (Mar 28 2022 at 13:50):

Thanks @Hanneli Tavante will do a pass later today

Hanneli Tavante (Mar 28 2022 at 13:50):

Thanks @Emilio Jesús Gallego Arias

Emilio Jesús Gallego Arias (Mar 28 2022 at 13:56):

Are you Ok with me sending a quick reminder now?

Emilio Jesús Gallego Arias (Mar 28 2022 at 13:57):

for additional people to complete the poll?

Hanneli Tavante (Mar 28 2022 at 13:58):

Hm, do we need that? The poll has dates like tomorrow

Hanneli Tavante (Mar 28 2022 at 13:59):

I am not super sure if more people will vote

Emilio Jesús Gallego Arias (Mar 28 2022 at 14:25):

I don't know, I guess it can't hurt

Hanneli Tavante (Mar 28 2022 at 14:27):

Sure, so if you do that I think I have to edit the Wiki; I was taking Thursday as the winner

Emilio Jesús Gallego Arias (Mar 28 2022 at 14:28):

Umm good point, let me see

Hanneli Tavante (Mar 28 2022 at 14:28):

I can revert the text, 1 sec

Hanneli Tavante (Mar 28 2022 at 14:30):

Okay, I reverted it

Emilio Jesús Gallego Arias (Mar 28 2022 at 14:31):

Ok, maybe indeed the reminder is not fully a good idea, not sure indeed. In case we want to send it I propose this text:

Dear all,

this is a reminder that today is the last day to fill out the availability poll for the upcoming JsCoq + CoqDB hackaton. We will announce the definitive date later today.

Kind regards,
Hanneli and Emilio

Emilio Jesús Gallego Arias (Mar 28 2022 at 14:32):

What do you think?

Hanneli Tavante (Mar 28 2022 at 14:36):

I don't have strong opinions on it; I just think it might not be effective. Especially bc we'd be sending multiple emails on the list, and hence maybe more folks will ignore us (?)

Emilio Jesús Gallego Arias (Mar 28 2022 at 14:39):

I would have thought that sending (concise) emails would be actually a good way to remind people to participate.

Emilio Jesús Gallego Arias (Mar 28 2022 at 14:39):

But indeed maybe that logic makes sense

Emilio Jesús Gallego Arias (Mar 28 2022 at 14:39):

I dunno

Hanneli Tavante (Mar 28 2022 at 14:40):

Well, I don't think sending a reminder hurts, so I think you can go for it. Worst case it that it won't be super effective

Emilio Jesús Gallego Arias (Mar 28 2022 at 14:40):

ok, will proceed, what time is good for you to sync 10 mins again today?

Hanneli Tavante (Mar 28 2022 at 14:41):

I'm teaching until 14h30 EST. So anytime after 20h30 Paris time :) Would it work for you?

Emilio Jesús Gallego Arias (Mar 28 2022 at 15:14):

I think around that time will work great, thanks and have a good class

Hanneli Tavante (Mar 28 2022 at 18:30):

@Emilio Jesús Gallego Arias I'm back

Emilio Jesús Gallego Arias (Mar 28 2022 at 18:34):

Hi

Hanneli Tavante (Mar 28 2022 at 18:35):

Schedule suggestion (Paris time):
14h00 - 15h20 - CoqDB (maybe introduce what you have in mind and come up with features to be implemented?). Maybe do a 15min intro and move to breakout rooms?
15h20 - 15h40 - Break
15h40 - 17h00 - jsCoq - possibly refresh some ideas we collected from the previous workgroup (15min) and then move to breakout rooms?

Emilio Jesús Gallego Arias (Mar 28 2022 at 18:35):

Sounds good, tho for the first topic, I'm not sure we'll need a breakout room?

Hanneli Tavante (Mar 28 2022 at 18:35):

True, maybe it'll be a collective discussion

Hanneli Tavante (Mar 28 2022 at 18:37):

I'll go ahead and add this draft to the wiki then.

Emilio Jesús Gallego Arias (Mar 28 2022 at 18:37):

Thanks

Emilio Jesús Gallego Arias (Mar 28 2022 at 18:37):

I guess we can wait a few hours to announce the final time if that's ok for you

Emilio Jesús Gallego Arias (Mar 28 2022 at 18:37):

let me see if my messsage arrived

Hanneli Tavante (Mar 28 2022 at 18:40):

Sure, by announcing do you mean sending another email to the list + twitter + discourse?

Emilio Jesús Gallego Arias (Mar 28 2022 at 19:05):

I guess so, mainly setting the date

Emilio Jesús Gallego Arias (Mar 28 2022 at 19:05):

and the program

Hanneli Tavante (Mar 28 2022 at 19:06):

Cool, I'll wait a few more hours and then update the Wiki + send the announcements

Hanneli Tavante (Mar 28 2022 at 19:08):

@Emilio Jesús Gallego Arias Am I forgetting anything else that is important?

Emilio Jesús Gallego Arias (Mar 28 2022 at 19:08):

Thanks a lot! I don't think so, I'm still a bit slow

Emilio Jesús Gallego Arias (Mar 28 2022 at 19:09):

as I finished with grant writing Friday, and I am going thru piles of email

Emilio Jesús Gallego Arias (Mar 28 2022 at 19:09):

but IMHO we are good

Hanneli Tavante (Mar 28 2022 at 19:09):

Cool, thanks.
Thursday still seems to be the winner.
Do you think you could do the CoqDB intro?

Emilio Jesús Gallego Arias (Mar 28 2022 at 19:10):

Yes I can!

Hanneli Tavante (Mar 28 2022 at 19:10):

I can help with jsCoq if needed.

Emilio Jesús Gallego Arias (Mar 28 2022 at 19:10):

Cool

Hanneli Tavante (Mar 28 2022 at 19:11):

All right then, please let me know if you need any help.
Otherwise, I'll go ahead and send the announcements later on.
Thanks a lot @Emilio Jesús Gallego Arias

Emilio Jesús Gallego Arias (Mar 28 2022 at 19:14):

I will let you know tomorrow, thanks to you!

Emilio Jesús Gallego Arias (Mar 29 2022 at 16:30):

Hi @Hanneli Tavante so we are all good, right?

Emilio Jesús Gallego Arias (Mar 29 2022 at 16:31):

Did you send to coq-club too? If not I can just copy the twitter message

Hanneli Tavante (Mar 29 2022 at 16:33):

I think we are all set
Ah crap, my email for coq-club failed
Maybe you can try to resend it?

Hi everyone,

Our next Coq Hackathon and [workgroup session](https://github.com/coq/coq/wiki/jsCoq--and-CoqDB-Working-Day) is happening this **Thursday, March 31st, 14h00 Paris time** (08h00 NYC time - 05h00 Seattle time). Please join us! We'll be focusing on two topics: [jsCoq](https://github.com/jscoq/jscoq) (see the Wiki section [here](https://github.com/coq/coq/wiki/jsCoq--and-CoqDB-Working-Day#jscoq-general-discussion)) and the initial implementation of "CoqDB", an attempt to develop a unified framework where information about Coq objects and metadata can be handled (see the Wiki section [here](https://github.com/coq/coq/wiki/jsCoq--and-CoqDB-Working-Day#coqdb)).

This will be an entirely virtual session held at Zoom. Meeting link can be found on the event's Wiki. Meanwhile, please add your name to the participants' list, and fill the respective sessions with topics you'd like to discuss and work on.

We are looking forward to seeing you in our next work session! If you have any questions, do not hesitate to ask them at [Zulip](https://coq.zulipchat.com/#narrow/stream/314095-Coq-Hackathon-and-Working-Group.2C-Winter-2022/topic/Upcoming.20workgroup.20session.3A.20jsCoq.20and.20CoqDB).

Best,

WDYT?

Hanneli Tavante (Mar 29 2022 at 16:33):

(Discourse message worked fine tho)

Emilio Jesús Gallego Arias (Mar 29 2022 at 16:34):

Yes I can take care of sending it, thanks. I will do a pass on the program.

Hanneli Tavante (Mar 29 2022 at 16:35):

Thanks @Emilio Jesús Gallego Arias !

Emilio Jesús Gallego Arias (Mar 29 2022 at 16:35):

Thanks to you!

Hanneli Tavante (Mar 29 2022 at 16:36):

Maybe tomorrow you could retweet my tweet as a final reminder; wdyt?

Emilio Jesús Gallego Arias (Mar 29 2022 at 16:36):

Sure

Hanneli Tavante (Mar 29 2022 at 16:37):

cool, thanks!

Hanneli Tavante (Mar 30 2022 at 15:56):

:megaphone::rooster: Our next Coq Hackathon and workgroup session is happening online tomorrow, Thursday, March 31st, 14h00 Paris time (08h00 NYC time - 05h00 Seattle time). Join us! Please add your name to the participants' list, and fill the respective sessions with topics you'd like to discuss and work on.

Hanneli Tavante (Mar 31 2022 at 11:52):

Reminder: we have a workgroup session starting in 10 min! Zoom link

Ali Caglayan (Mar 31 2022 at 15:21):

meeting_saved_chat.txt

Hanneli Tavante (Mar 31 2022 at 15:21):

Thanks for joining!
Some notes here ; I'll transfer a better version for the Wiki.

Hanneli Tavante (Mar 31 2022 at 16:09):

@Emilio Jesús Gallego Arias Session recording video https://drive.google.com/file/d/1oIPvfB9y47cGBqFYPI6tpAhB_aTD7-5r/view?usp=sharing

Karl Palmskog (Mar 31 2022 at 20:28):

so if anyone wonders about my current setup for dependency graph generation with SVG images and links, I use a fork of dpdgraph and a lot of Makefile hacking:

• https://github.com/palmskog/rvdpdgraph/
• https://github.com/runtimeverification/vlsm/blob/master/Makefile.coq.local

Samples of generated SVG with links into other SVG and coqdoc:

• https://runtimeverification.github.io/vlsm-docs/latest/coqdoc/map.svg
• https://runtimeverification.github.io/vlsm-docs/latest/coqdoc/VLSM.Core.Equivocators.EquivocatorReplay.svg

The reason for a fork is that I don't think the general dpdgraph users may want this setup.

Karl Palmskog (Mar 31 2022 at 20:29):

I'll try to separate out the part that makes dpdgraph code use fully qualified names and submit as dpdgraph PR, now that I know Yves is interested in this

Last updated: Jun 10 2023 at 23:01 UTC