Coq has been renamed into the Rocq Prover. by Zimmi48 · Pull Request #7297 · github-linguist/linguist · GitHub
Skip to content

Coq has been renamed into the Rocq Prover.#7297

Merged
lildude merged 1 commit into
github-linguist:mainfrom
Zimmi48:rocq-prover
Apr 20, 2025
Merged

Coq has been renamed into the Rocq Prover.#7297
lildude merged 1 commit into
github-linguist:mainfrom
Zimmi48:rocq-prover

Conversation

@Zimmi48

@Zimmi48 Zimmi48 commented Mar 31, 2025 •
edited
Loading

Copy link
Copy Markdown
Contributor

Context: https://rocq-prover.org/about#Name
The old official website https://coq.inria.fr/ now redirects to https://rocq-prover.org/.
I'm part of the official core team of the Rocq Prover (https://rocq-prover.org/rocq-team/core).

Description

This commit does not yet:

  • Change the color associated with the language (will be done after consulting with the community).
  • Change the grammar used for the language (a new official grammar using the Rocq Prover colors is expected to be published, but it is not yet available).

Checklist:

  • I am adding a new extension to a language.

    • The new extension is used in hundreds of repositories on GitHub.com
    • I have included a real-world usage sample for all extensions added in this PR:
      • Sample source(s):
        • [URL to each sample source, if applicable]
      • Sample license(s):
    • I have included a change to the heuristics to distinguish my language from others using the same extension.

  • I am adding a new language.

    • The extension of the new language is used in hundreds of repositories on GitHub.com.
    • I have included a real-world usage sample for all extensions added in this PR:
      • Sample source(s):
        • [URL to each sample source, if applicable]
      • Sample license(s):
    • I have included a syntax highlighting grammar: [URL to grammar repo]
    • I have added a color
      • Hex value: #RRGGBB
      • Rationale:
    • I have updated the heuristics to distinguish my language from others using the same extension.

  • I am fixing a misclassified language

    • I have included a new sample for the misclassified language:
      • Sample source(s):
        • [URL to each sample source, if applicable]
      • Sample license(s):
    • I have included a change to the heuristics to distinguish my language from others using the same extension.

  • I am changing the source of a syntax highlighting grammar

    • Old: [URL to grammar repo]
    • New: [URL to grammar repo]

  • I am updating a grammar submodule

  • I am adding new or changing current functionality

    • I have added or updated the tests for the new or changed functionality.

  • I am changing the color associated with a language

    • I have obtained agreement from the wider language community on this color change.
      • [URL to public discussion]
      • [Optional: URL to official branding guidelines for the language]

@Zimmi48 Zimmi48 requested a review from a team as a code owner March 31, 2025 15:09
lildude
lildude requested changes Mar 31, 2025
View reviewed changes

@lildude lildude left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We never remove support for an extension. Once included, it remains, regardless of whether it's an official extension or not or a project decides to drop support for an extension. Why? Because files with those extensions will almost certainly always exist on GitHub and we don't want to degrade this experience if we can avoid it, regardless of how small.

Please put back the .coq extension.

@Zimmi48

Zimmi48 commented Mar 31, 2025

Copy link
Copy Markdown
Contributor Author

@lildude

lildude commented Apr 1, 2025

Copy link
Copy Markdown
Member

Changed.

🤨 I'm not sure what you changed as you rewrote your history (we don't care about all the commits you may use in a PR as we squash commits on merging) but you've still not added the .coq extension to the extensions section.

If it's no longer correct to have it as the primary extension, by all means put it after the .v extension (alphabetical order only applies after the first extension which is considered the primary extension of a language - see the comments at the top of the languages.yml file).

@LibraGenX80

This comment was marked as spam.

Sign in to view
@LibraGenX80

This comment has been minimized.

Sign in to view
@LibraGenX80

This comment was marked as spam.

Sign in to view
@Zimmi48

Zimmi48 commented Apr 2, 2025

Copy link
Copy Markdown
Contributor Author

Changed.

🤨 I'm not sure what you changed as you rewrote your history (we don't care about all the commits you may use in a PR as we squash commits on merging) but you've still not added the .coq extension to the extensions section.

If it's no longer correct to have it as the primary extension, by all means put it after the .v extension (alphabetical order only applies after the first extension which is considered the primary extension of a language - see the comments at the top of the languages.yml file).

Thanks for catching that, and my apologies for the mistake (I did a git commit --amend, but I forgot the -a, so I had only changed the commit message). This is fixed now.

I also changed the order of the extension as you recommended, since indeed .v should be considered as the primary extension.

@Zimmi48 Zimmi48 requested a review from lildude April 7, 2025 14:59
@Zimmi48
Coq has been renamed into the Rocq Prover.
7565bde 
- Change the name of the language to Rocq Prover.
- Add a new key for code blocks while preserving the coq one for
  backward compatibility.

This commit does not yet:

- Change the color associated with the language (will be done after
  consulting with the community).
- Change the grammar used for the language (a new official grammar
  using the Rocq Prover colors is expected to be published, but it is
  not yet available).
@Zimmi48

Zimmi48 commented Apr 16, 2025

Copy link
Copy Markdown
Contributor Author

lildude
lildude approved these changes Apr 20, 2025
View reviewed changes

@lildude lildude left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM. Thanks.

Important

The changes in this PR will not appear on GitHub until the next release has been made and deployed. See here for more details.

@lildude lildude added this pull request to the merge queue Apr 20, 2025
Merged via the queue into github-linguist:main with commit 4b9ec28 Apr 20, 2025
@github-linguist github-linguist locked as resolved and limited conversation to collaborators Aug 9, 2025
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Reviewers

@lildude lildude lildude approved these changes

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@Zimmi48 @lildude @LibraGenX80