Stream: Coq Hackathon and Working Group, Winter 2022

Topic: Upcoming workgroup session: jsCoq and CoqDB


view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2022 at 12:53):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2022 at 13:08):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2022 at 13:24):

Give me 20 mins @Hanneli Tavante

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2022 at 13:33):

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

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip Hanneli Tavante (Mar 28 2022 at 13:42):

WDYT?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2022 at 13:50):

Thanks @Hanneli Tavante will do a pass later today

view this post on Zulip Hanneli Tavante (Mar 28 2022 at 13:50):

Thanks @Emilio Jesús Gallego Arias

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2022 at 13:56):

Are you Ok with me sending a quick reminder now?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2022 at 13:57):

for additional people to complete the poll?

view this post on Zulip Hanneli Tavante (Mar 28 2022 at 13:58):

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

view this post on Zulip Hanneli Tavante (Mar 28 2022 at 13:59):

I am not super sure if more people will vote

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2022 at 14:25):

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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2022 at 14:28):

Umm good point, let me see

view this post on Zulip Hanneli Tavante (Mar 28 2022 at 14:28):

I can revert the text, 1 sec

view this post on Zulip Hanneli Tavante (Mar 28 2022 at 14:30):

Okay, I reverted it

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2022 at 14:32):

What do you think?

view this post on Zulip 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 (?)

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2022 at 14:39):

But indeed maybe that logic makes sense

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2022 at 14:39):

I dunno

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Hanneli Tavante (Mar 28 2022 at 18:30):

@Emilio Jesús Gallego Arias I'm back

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2022 at 18:34):

Hi

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Hanneli Tavante (Mar 28 2022 at 18:35):

True, maybe it'll be a collective discussion

view this post on Zulip Hanneli Tavante (Mar 28 2022 at 18:37):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2022 at 18:37):

Thanks

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2022 at 18:37):

let me see if my messsage arrived

view this post on Zulip Hanneli Tavante (Mar 28 2022 at 18:40):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2022 at 19:05):

I guess so, mainly setting the date

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2022 at 19:05):

and the program

view this post on Zulip Hanneli Tavante (Mar 28 2022 at 19:06):

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

view this post on Zulip Hanneli Tavante (Mar 28 2022 at 19:08):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2022 at 19:09):

but IMHO we are good

view this post on Zulip 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?

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2022 at 19:10):

Yes I can!

view this post on Zulip Hanneli Tavante (Mar 28 2022 at 19:10):

I can help with jsCoq if needed.

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2022 at 19:10):

Cool

view this post on Zulip 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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 28 2022 at 19:14):

I will let you know tomorrow, thanks to you!

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2022 at 16:30):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Hanneli Tavante (Mar 29 2022 at 16:33):

(Discourse message worked fine tho)

view this post on Zulip 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.

view this post on Zulip Hanneli Tavante (Mar 29 2022 at 16:35):

Thanks @Emilio Jesús Gallego Arias !

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2022 at 16:35):

Thanks to you!

view this post on Zulip Hanneli Tavante (Mar 29 2022 at 16:36):

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

view this post on Zulip Emilio Jesús Gallego Arias (Mar 29 2022 at 16:36):

Sure

view this post on Zulip Hanneli Tavante (Mar 29 2022 at 16:37):

cool, thanks!

view this post on Zulip 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.

view this post on Zulip Hanneli Tavante (Mar 31 2022 at 11:52):

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

view this post on Zulip Ali Caglayan (Mar 31 2022 at 15:21):

meeting_saved_chat.txt

view this post on Zulip Hanneli Tavante (Mar 31 2022 at 15:21):

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

view this post on Zulip 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

view this post on Zulip 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:

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

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

view this post on Zulip 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: Jan 29 2023 at 15:02 UTC