Stream: Coq Hackathon and Working Group, Winter 2022

Topic: Software for the Hacktathon


view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2022 at 18:53):

Hi folks, @Ali Caglayan and I were discussing about what software to use for the Hackathon; we both think Discord is interesting: it has a lot of features to do breakout sessions, and we think it would be cool to try a new platform; it was used for the HoTT school last year.

On the other hand, we don't know how it would interact with Zulip, so maybe BBB + Zulip is a safer choice?

What do you think folks ? cc: @nicolas tabareau

view this post on Zulip Karl Palmskog (Feb 08 2022 at 19:12):

personally, I really don't like Discord

view this post on Zulip Karl Palmskog (Feb 08 2022 at 19:13):

so vote for BBB + Zulip here any day of the week

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2022 at 21:04):

Thanks for the feedback @Karl Palmskog , actually we discussed a bit more and indeed our excitement for Discord has toned down quite a bit, so we will do as in the Coq Workshop I think

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2022 at 21:04):

I still like the idea tho of using Discord, but for another time

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2022 at 21:04):

there is a reason is so popular

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2022 at 21:04):

I prefer different systems, but Discord provides something no other system provides

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2022 at 21:04):

a very smooth _integral_ experience

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2022 at 21:05):

imagine Zulip had phone and video calls, that'd be a gamechanger

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2022 at 21:05):

plus the bots are top-notch

view this post on Zulip Karl Palmskog (Feb 08 2022 at 21:07):

Discord is completely proprietary and for all we know they log/distribute all communication to a bunch of parties for commercial and other gain

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2022 at 21:08):

I wasn't aware of the last part, I know it is propietary

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2022 at 21:08):

But as an experiment I'm OK with that as it can be used from the browser

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2022 at 21:09):

and as of today it is hard to imagine anyone does steer clear of propietary websites (very unfortunately)

view this post on Zulip Karl Palmskog (Feb 08 2022 at 21:10):

I think Inria-hosted BBB is a reasonable tradeoff (OSS, so probably no covert channels, etc.)

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2022 at 21:22):

I was not aware the Discord used data that way, seems pretty bad!

view this post on Zulip Karl Palmskog (Feb 08 2022 at 21:23):

I mean, I don't have proof that they sell anything or whatever, but if you have a proprietary solution in the cloud, there is no possible way to say they don't/won't

view this post on Zulip Karl Palmskog (Feb 08 2022 at 21:25):

I know for sure they monitor/check all communication, and who can say for how long they store it? Obviously they have everyone's IP and so on.

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2022 at 21:27):

That's easy to check as they should be clear what kind of end-to-end encryption use

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2022 at 21:27):

well something is to log, which can be done with reasonable privacy

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2022 at 21:27):

a very different thing is to sell the content itself

view this post on Zulip Karl Palmskog (Feb 08 2022 at 21:27):

but how do you tell the difference?

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2022 at 21:27):

I thought you were affirming it, now that I think of it I'd be very surprised if they didn't promise something like Zoom

view this post on Zulip Gaëtan Gilbert (Feb 08 2022 at 21:27):

they don't have end to end encryption

view this post on Zulip Gaëtan Gilbert (Feb 08 2022 at 21:28):

unless you count their servers as an end

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

Anyways we changed our minds after writing the post, sorry for the noise folks

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

tho it is good to learn a bit more

view this post on Zulip Karl Palmskog (Feb 08 2022 at 21:29):

but I think it's important to choose trusted parties. We don't have resources to analyze clients and so on, and we already implicitly include Inria in our trusted base.

view this post on Zulip Karl Palmskog (Feb 08 2022 at 21:31):

so I think any solution for chat/video/etc. should be hosted by Inria or OSS+cloud

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2022 at 21:31):

For this event where all communciation is public

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2022 at 21:31):

while I agree with you in spirit

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2022 at 21:31):

I also consider alternatives if that's gonna make the life of newcomers easier

view this post on Zulip Karl Palmskog (Feb 08 2022 at 21:31):

are private BBB breakout rooms considered public?

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2022 at 21:32):

that's more important for me, and I fully support your views against propietary software

view this post on Zulip Karl Palmskog (Feb 08 2022 at 21:32):

I thought participants could have private sessions if they wished

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2022 at 21:32):

Karl Palmskog said:

are private BBB breakout rooms considered public?

that's a good point now that you mention it, I guess people may assume privacy on them and talk bad for example of the person that developed the Dune support for Coq and how lazy he's been

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2022 at 21:33):

they better don't as that guy will find a way to know XD

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2022 at 21:33):

Karl Palmskog said:

I thought participants could have private sessions if they wished

yes that's a very good point, it is reasonable to expect privacy in these rooms

view this post on Zulip Karl Palmskog (Feb 08 2022 at 21:34):

there are so many ways these days to be misunderstood in public communication, so for some collaborations I prefer talking privately for sure

view this post on Zulip Karl Palmskog (Feb 08 2022 at 21:35):

the hypothetical lazy dev stuff is just the tip of the iceberg...

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2022 at 21:36):

Karl Palmskog said:

there are so many ways these days to be misunderstood in public communication, so for some collaborations I prefer talking privately for sure

I was kidding of course, as it seems lots of interest in dune and none of the promises of improvement so far, but yes to both

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2022 at 21:36):

and yes communication is super difficult!

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2022 at 21:36):

in general

view this post on Zulip Emilio Jesús Gallego Arias (Feb 08 2022 at 21:37):

for me so difficult that I got inscribed into a program to improve it

view this post on Zulip Emilio Jesús Gallego Arias (Feb 09 2022 at 01:16):

Actually files don't make a lot of sense for ITP

view this post on Zulip Emilio Jesús Gallego Arias (Feb 09 2022 at 01:16):

are just IMO, a historical implementation detail that we will soon get rid of

view this post on Zulip Emilio Jesús Gallego Arias (Feb 09 2022 at 01:16):

(famous last words (TM))


Last updated: Jan 29 2023 at 16:02 UTC