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"

@Karl Palmskog I think we also should have `coq`

tag on all coq-community projects.

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.

@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

for example, Google searches don't use GitHub tags

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?

yes, the org name is shown in the url, but the description doesn't mention Coq at all

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?

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: Apr 14 2024 at 11:02 UTC