Karl Palmskog (Sep 08 2020 at 09:51): Karl Palmskog (Sep 08 2020 at 09:51):For marketing reasons, I think all our projects should have "Coq" in the GitHub description (even if it's already in the project name). Descriptions show up in GitHub and Google searches, so it helps boost the signal.
On this note, @Christian Doczkal do you mind if I change:
"Graph Theory" -> "Graph theory in Coq"
"Completeness and Decidability of Modal Logic Calculi" -> "Completeness and decidability of modal logic calculi in Coq"
Anton Trunov (Sep 08 2020 at 11:07):@Karl Palmskog I think we also should have coq tag on all coq-community projects.
Christian Doczkal (Sep 08 2020 at 12:06):I am in favor of adding a Coq tag or anything else that makes repositories show up when searching for coq. However, I am firmly against putting a redundant "in Coq" in the description of every coq-community project. This is the Coq community, every project/repository uses Coq.
Karl Palmskog (Sep 08 2020 at 12:10):@Christian Doczkal my point is that these descriptions show up in random searches, like if you search for "exact real arithmetic" on Google, the coq-community project is one of the top hits, but there is nothing shown that ties the project to Coq
Karl Palmskog (Sep 08 2020 at 12:14):for example, Google searches don't use GitHub tags
Christian Doczkal (Sep 08 2020 at 12:21):If I carry out your search, I get the following entry on the first page:
github.com › coq-community › exact-real-arithmetic
coq-community/exact-real-arithmetic: Exact Real ... - GitHub
Exact Real Arithmetic [maintainers=@ybertot,@magaud] - coq-community/exact-real-arithmetic.
There are three mentions of coq-community, so what exactly is the problem here?
Karl Palmskog (Sep 08 2020 at 12:22):yes, the org name is shown in the url, but the description doesn't mention Coq at all
Christian Doczkal (Sep 08 2020 at 12:28):I still don't get the point of doing this. If someone wants things done in Coq he will add this to the search and get coq-community reasults among his first results. If the person doesn't care about Coq, then I see no point in adding some "Coq" to the title. It might even discourage people from outside the community. So what exactly are you trying to achieve here?
Karl Palmskog (Sep 08 2020 at 12:30):I'm trying to make our metadata searchable easily in search engines and databases, without having to know the context. Let's say you're making a list of verification projects on the web. Do you want to do URL analysis to figure that something is a Coq project?
Last updated: Jun 03 2023 at 18:01 UTC