Stream: Coq devs & plugin devs

Topic: WG about namespaces


view this post on Zulip Enrico Tassi (Nov 09 2020 at 08:58):

https://rdv2.rendez-vous.renater.fr/coq-ns seems super unstable today

view this post on Zulip Enrico Tassi (Nov 09 2020 at 09:00):

CC @Cyril Cohen @Guillaume Melquiond @Hugo Herbelin

view this post on Zulip Guillaume Melquiond (Nov 09 2020 at 09:03):

It seems to work fine for me. Maybe a transient issue?

view this post on Zulip Guillaume Melquiond (Nov 09 2020 at 09:04):

Actually, no, forget what I said.

view this post on Zulip Cyril Cohen (Nov 09 2020 at 09:04):

Not working for me

view this post on Zulip Enrico Tassi (Nov 09 2020 at 09:06):

Let's try visio.inria.fr

view this post on Zulip Enrico Tassi (Nov 09 2020 at 09:07):

https://visio.inria.fr/invited.sf?secret=_Bp6SsB7rqONgIqDCOfFrA&id=327218302

view this post on Zulip Cyril Cohen (Nov 09 2020 at 09:07):

I have another meeting that I forgot about in 20 min...

view this post on Zulip Cyril Cohen (Nov 09 2020 at 09:08):

Sorry about that...

view this post on Zulip Enrico Tassi (Nov 09 2020 at 09:10):

Does visio work for you guys?

view this post on Zulip Guillaume Melquiond (Nov 12 2020 at 08:17):

Sorry, I messed my planning, I have another meeting this morning. I won't be able to attend this one.

view this post on Zulip Enrico Tassi (Nov 12 2020 at 08:21):

Hugo was busy as well, maybe it's better to reschedule. Moreover, thinking about the topics, I think I would have just proposed to make examples of the NS manipulation primitives we want (in addition to open). IMO it would work better if we all came at the WG with some of these examples.

view this post on Zulip Enrico Tassi (Nov 12 2020 at 09:00):

Here a framadate https://framadate.org/IKkcEPIKlbk36pl4PeIT6Qln (I'm on holidays on tuesday)
maybe also @Jason Gross can be interested in this

view this post on Zulip Guillaume Melquiond (Nov 12 2020 at 09:18):

"Ce sondage n'existe pas !"

view this post on Zulip Enrico Tassi (Nov 12 2020 at 12:57):

https://framadate.org/IKkcEPIKlbk36pl4

view this post on Zulip Enrico Tassi (Nov 12 2020 at 12:57):

that was the admin link :-/

view this post on Zulip Enrico Tassi (Nov 12 2020 at 14:24):

@Cyril Cohen are you available on Monday at 4PM?

view this post on Zulip Cyril Cohen (Nov 12 2020 at 14:29):

Yes!

view this post on Zulip Enrico Tassi (Nov 12 2020 at 16:38):

Monday 4PM then

view this post on Zulip Jason Gross (Nov 12 2020 at 18:34):

I can show up if you think my input is important, but otherwise I'm inclined to skip this one so I have a bit more time in my schedule to prepare for my upcoming PhD defense

view this post on Zulip Enrico Tassi (Nov 12 2020 at 20:26):

I just wanted to keep you in the loop, if you have more pressing issues to deal with it's not a problem at all.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 12 2020 at 22:02):

Thanks @gares, I'd try to join too, tho I'm not very knowledgeable about namespaces myself, I'd like to get an understanding on what the new proposal means for UI tooling.

Couple of questions after reading https://github.com/coq/ceps/pull/25#issuecomment-723988445:

view this post on Zulip Cyril Cohen (Nov 16 2020 at 15:02):

I'm coming, which channel?

view this post on Zulip Enrico Tassi (Nov 16 2020 at 15:03):

https://rdv2.rendez-vous.renater.fr/coq-ns

view this post on Zulip Enrico Tassi (Dec 08 2020 at 08:38):

We should present something tomorrow at the Coq call. I'll try to find some time to work on the CEP document this afternoon, but I also want to prepare a few slides about the release. So if someone else has time to update the CEP... that would be welcome

view this post on Zulip Enrico Tassi (Dec 08 2020 at 16:10):

I've updated the draft: https://github.com/coq/ceps/blob/7df4fd8ad86935a0ef1bcb1673777b055691f2da/text/025-namespaces.md


Last updated: Oct 21 2021 at 20:02 UTC