search

coq / coq.github.io

Source files of the coq.inria.fr website
https://coq.inria.fr/
Other
15 stars 37 forks source link

Add a Coq-Team page #172

Closed mattam82 closed 3 years ago

mattam82 commented 3 years ago

I couldn't help but also correct the abnormally high text-indent's :)

mattam82 commented 3 years ago

I've no idea how to show the rendered file here, so here's a screenshot, taken with some zoom out

image

gares commented 3 years ago

May I suggest "current maintainers" or "maintainers", or actually check if they had some activity in the last, say, 2 years?

mattam82 commented 3 years ago

@gares My idea is that I will ping all the people here once we're ok, and see if anyone wants to get out of the "Maintainers" page, not appear, or fix a misatribution/date/...

mattam82 commented 3 years ago

@JasonGross accepted the invitation, we hence have a new member in the Coq Core Team. I would like this to get merged before the workshop on friday.

mattam82 commented 3 years ago

@YBertot @maximedenes @ejgallego @SkySkimmer @JasonGross @herbelin @silene @ppedrot @gares @Zimmi48 @fbesson @CyrilCohen @PierreCorbineau @Matafou @jfehrle @forestjulien @ggonthier @bgregoir @vbgl @amahboubi @erikmd @cpitclaudel @proux @pi8027 @VincentSe @aspiwack @MSoegtropIMC @thery @anton-trunov @Lysxia @tabareau @backtracking @barras @delahayd @letouzey @monate we are about to merge this page presenting present and past contributors to Coq. Please check your information here: https://github.com/coq/www/blob/b19613d9da8eaeec3c47c2437c6f711dffa09027/pages/coq-team.html (or look for the pages/coq-team.html diff in the Files tab) and suggest changes if we made a mistake/misattribution or if you do not want to appear there. Thanks for your help!

Zimmi48 commented 3 years ago

@mattam82 I guess it would make sense to include maintainers of the opam-coq-archive in the "Maintainers" section. This would mean in particular @clarus and @palmskog (if I'm not forgetting anyone).

mattam82 commented 3 years ago

@Zimmi48 right!

ybertot commented 3 years ago

I have been looking at the opam-coq-archive messages a lot, and I tend to think that Enrico Tassi and Guillaume Melquiond are also active maintainers.

Zimmi48 commented 3 years ago

@ybertot Yes, but these two are already listed as core devs on the team page. Note that I wasn't proposing to create a distinct category for opam-coq-archive maintainers, just suggesting to list all the maintainers of opam-coq-archive on the team page.

mattam82 commented 3 years ago

I added "opam" to myself, Enrico, Karl and both Guillaumes as related "components"

PierreCorbineau commented 3 years ago

Please link to https://www-verimag.imag.fr/~corbinea/ for my web page, not to P. Courtieu's ...

Thx.

Pierre

mattam82 commented 3 years ago

Thanks @mattam82! I left 2 other review comments.

BTW, I have a question for an English translation: there are many occurrences of Assistant professor in the page for translating Maître de conférences IINM, but I guess Associate professor would be a more precise translation? (albeit not fully precise; but if you think this is a concern, one might just leave the Maître de conférences phrasing instead?)

Indeed, associate professor seems more appropriate, I'll update that.

ejgallego commented 3 years ago

Note that @corwin-of-amber has done huge work on jsCoq [by extension some of it has reached Coq], so maybe if we wanna cover jsCoq here he should definitively appear.

erikmd commented 3 years ago

Note that corwin-of-amber has done huge work on jsCoq [by extension some of it has reached Coq], so maybe if we wanna cover jsCoq here he should definitively appear.

BTW in this case (if the idea is to also mention all current core maintainers of CoqIde / Proof-General / jsCoq / VsCoq ?),

we should definitely mention Hendrik Tews, for his significant contributions to Proof-General that he still actively maintains with Pierre Courtieu, Clément Pit-Claudel and me.

@mattam82, if the answer to my question above in italics is "yes", feel free to @-mention him as well 🙂 (his login is hendriktews)

mattam82 commented 3 years ago

I wonder what others think about including maintainers not of Coq itself but of extensions, I was thinking we wanted to restrict to the Coq proper maintainers. But that also feels overly restrictive to me as indeed interfaces are essential parts of the whole. @Zimmi48 @herbelin @maximedenes ?

Zimmi48 commented 3 years ago

I wonder what others think about including maintainers not of Coq itself but of extensions, I was thinking we wanted to restrict to the Coq proper maintainers. But that also feels overly restrictive to me as indeed interfaces are essential parts of the whole.

The problem with including external projects such as user interfaces is where do you stop? How do you decide which external maintainers should be on this page and which doesn't deserve? IMHO it's better to stop to coq officially maintained projects. You can add a generic sentence acknowledging that Coq wouldn't be what it is without many maintainers of ecosystem projects (user interfaces, libraries, plugins).

mattam82 commented 3 years ago

Indeed, we should stop here. Maybe we can have in addition a curated list of highlighted projects somewhere else

mattam82 commented 3 years ago

BTW, nothing prevents us from adding hyperlinks to the mentioned projects, which can have their own contributors lists

CohenCyril commented 3 years ago

@mattam82

@cyrilcohen

@CohenCyril

anton-trunov commented 3 years ago

Maybe we can have in addition a curated list of highlighted projects somewhere else

We kind of have it here: https://github.com/coq-community/awesome-coq.

Or maybe we could have a new list basing off of awesome-coq.

mattam82 commented 3 years ago

Yes, I was thinking of putting pretty pictures on awesome-coq, basically :)

mattam82 commented 3 years ago

While we don't have the consent of everyone, I think we got enough feedback now, so can any one of the @coq/website-maintainers merge?

Zimmi48 commented 3 years ago

Sure, I'll merge, and we can fix further issues in future PRs. But feel free to merge any website PR yourself :)

palmskog commented 3 years ago

awesome-coq is meant to cover the whole range of libraries, tools, verified software, and formalized math. Ideally, someone can distill a few projects from each category (say, 5-10 in total, along with their logos) and link them directly from the Coq website in a new PR, along with a link to awesome-coq. This would be my suggestion, at least. Since we want to follow the "awesome" template, I don't think there should be images such as logos on awesome-coq itself.

anton-trunov commented 3 years ago

Oh, yes, good point. The awesome people are very strict w.r.t the overall presentation.

MSoegtropIMC commented 3 years ago

Since it is merged now, should it appear on (coq.inria.fr/) - I somehow can't find it.

mattam82 commented 3 years ago

BTW, the page looks good to me, but there's probably some css adjustments to make https://coq.inria.fr/coq-team.html

Zimmi48 commented 3 years ago

Since it is merged now, should it appear on (coq.inria.fr/) - I somehow can't find it.

Try a hard-reload (Ctrl+Shift+R).

anton-trunov commented 3 years ago

@MSoegtropIMC The page is linked at the very bottom of the https://coq.inria.fr ('Contributing to Coq' section).

CohenCyril commented 3 years ago

Contributions of Assia Mahboubi and Georges Gonthier must also include "Ssreflect". (As for me I barely touched a single line of code of ssreflect if any... although I reviewed some code).

Zimmi48 commented 3 years ago

Contributions of Assia Mahboubi and Georges Gonthier must also include "Ssreflect". (As for me I barely touched a single line of code of ssreflect if any... although I reviewed some code).

@mattam82 Do you want to take care of fixing these minor issues by pushing new commits directly to master?

herbelin commented 3 years ago

Contributions of Assia Mahboubi and Georges Gonthier must also include "Ssreflect". (As for me I barely touched a single line of code of ssreflect if any... although I reviewed some code).

Maybe also a good time to remind that the "schism" between ssreflect and vanilla tactics is dommageable to the ecosystem and that we should seriously think at a development project around tactics which allows us to go in a common uniting direction!

CohenCyril commented 3 years ago

Contributions of Assia Mahboubi and Georges Gonthier must also include "Ssreflect". (As for me I barely touched a single line of code of ssreflect if any... although I reviewed some code).

Maybe also a good time to remind that the "schism" between ssreflect and vanilla tactics is dommageable to the ecosystem and that we should seriously think at a development project around tactics which allows us to go in a common uniting direction!

No, not a good time, your message is clearly off-topic.

mattam82 commented 3 years ago

@CohenCyril I fixed the attribution, adding Assia and Georges and removing you.

herbelin commented 3 years ago

Sorry for looking tarnishing this nice initiative of Matthieu! I think that it is important as a team, and this is the page of a team, that we are globally going in a common direction and I'm sad that we failed to do so in some situations. Leaving it to Matthieu (or whoever volunteers) to address these questions in appropriate places.

I'm otherwise very glad of the initiative of this page. Reminding that a few things are not working at best is in no way hiding the long list of all what is working well. On the contrary, this shows that we are a team which welcomes contradictory debates.

jfehrle commented 3 years ago

People's names are in two different fonts, how about fixing that? Eg:

image

The boldface on this one seems inconsistent with the other entries:

image

Also, more trivially, "Coq-community manager" is capitalized differently for @Zimmi48 and @palmskog

Matafou commented 3 years ago

And this guy has a strange face too... Ho, wait, it's me.

gares commented 3 years ago

I suggest you change your hairdresser ;-)

Matafou commented 3 years ago

No pull request please :-) it hurts.

gares commented 3 years ago

About the page, I had some difficulties finding it in the website

pi8027 commented 3 years ago

Should we remove the following wiki page just not to maintain two similar lists in two places? https://github.com/coq/coq/wiki/Coq-development-team

Zimmi48 commented 3 years ago

Should we remove the following wiki page just not to maintain two similar lists in two places? https://github.com/coq/coq/wiki/Coq-development-team

:+1: Done.

mattam82 commented 3 years ago

People's names are in two different fonts, how about fixing that? Eg:

image

The boldface on this one seems inconsistent with the other entries:

image

Also, more trivially, "Coq-community manager" is capitalized differently for @Zimmi48 and @palmskog

Good catch!

mattam82 commented 3 years ago

About the page, I had some difficulties finding it in the website

@gares I added it on the front page (bottom link), Community and About Coq. Maybe we should use framework links to make it more apparent in this one, would that satisfy you?

Zimmi48 commented 3 years ago

What we could also do if we really want to put it forward is to put it in the top bar.

gares commented 3 years ago

I've no clue, I suck at websites. I was just acknowledging that the current website is messy.

gares commented 3 years ago

I mean, it's a job to organize contents so that people find it. Putting on the top bar a thing every time someone complains it is hard to find is not really scalable.

gares commented 3 years ago

So forget about my comment and let's hope the whole website gets "revamped" soon