Skip to content

The Coq proof assistant has been renamed into the Rocq Prover.#2883

Merged
Anteru merged 1 commit intopygments:masterfrom
Zimmi48:patch-1
Jul 26, 2025
Merged

The Coq proof assistant has been renamed into the Rocq Prover.#2883
Anteru merged 1 commit intopygments:masterfrom
Zimmi48:patch-1

Conversation

@Zimmi48
Copy link
Copy Markdown
Contributor

@Zimmi48 Zimmi48 commented Apr 16, 2025

Rename the lexer while keeping the coq alias for backward-compatibility.

See https://rocq-prover.org/about#Name for context on the renaming.

@Zimmi48 Zimmi48 mentioned this pull request Jun 17, 2025
Closed
@Zimmi48
Copy link
Copy Markdown
Contributor Author

Zimmi48 commented Jun 17, 2025

@Anteru Would you mind reviewing this trivial PR? People started to reimplement the same thing in another PR two months later (#2908).

@Villetaneuse
Copy link
Copy Markdown

Villetaneuse commented Jun 17, 2025

Is Coq disallowed as a name?
Does it prevent

\begin{minted}{Coq}
Check nat.
\end{minted}

to work?

@Villetaneuse
Copy link
Copy Markdown

Villetaneuse commented Jun 17, 2025

I suggest adding Rocq and Coq as aliases.

Zimmi48
Zimmi48 commented Jun 17, 2025
View reviewed changes
pygments/lexers/theorem.py
aliases = ['coq']
name = 'Rocq Prover'
url = 'https://rocq-prover.org/'
aliases = ['coq', 'rocq', 'rocq-prover']
Copy link
Copy Markdown
Contributor Author

@Zimmi48 Zimmi48 Jun 17, 2025

Choose a reason for hiding this comment

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

Suggested change
aliases = ['coq', 'rocq', 'rocq-prover']
aliases = ['coq', 'rocq', 'rocq-prover', 'Coq', 'Rocq']

Copy link
Copy Markdown
Contributor Author

@Zimmi48 Zimmi48 Jul 26, 2025

Choose a reason for hiding this comment

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

I had to revert this change, because aliases can only be lowercase.

@Zimmi48
Copy link
Copy Markdown
Contributor Author

Zimmi48 commented Jul 22, 2025

@Anteru Very sorry to insist, but it seems that this PR may have gone under your radar.

@Anteru
Copy link
Copy Markdown
Collaborator

Anteru commented Jul 22, 2025 •
edited
Loading

Yes, I've been swamped with stuff recently :( I'll earmark this for 2.22.0. Can you regenerate the mapfiles, for some reason it looks like GitHub actions is not picking this up.

@Zimmi48
Copy link
Copy Markdown
Contributor Author

Zimmi48 commented Jul 22, 2025

Thanks, done!

@Anteru
Copy link
Copy Markdown
Collaborator

Anteru commented Jul 24, 2025

Thanks. And all of a sudden the actions work again :)

@Zimmi48
The Coq proof assistant has been renamed into the Rocq Prover.
3f71947 
Rename the lexer while keeping the `coq` alias for backward-compatibility.
@Zimmi48
Copy link
Copy Markdown
Contributor Author

Zimmi48 commented Jul 26, 2025

Tests now confirmed to pass locally.

@Anteru Anteru merged commit 8cb01cc into pygments:master Jul 26, 2025
15 checks passed
@Anteru
Copy link
Copy Markdown
Collaborator

Anteru commented Jul 26, 2025

Merged, thanks a lot!

@Zimmi48
Copy link
Copy Markdown
Contributor Author

Zimmi48 commented Aug 4, 2025

Thanks!

@Zimmi48 Zimmi48 deleted the patch-1 branch August 4, 2025 14:14
@Anteru Anteru added this to the 2.20.0 milestone Mar 26, 2026
@Anteru Anteru added the A-lexing area: changes to individual lexers label Mar 26, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

A-lexing area: changes to individual lexers

Projects

None yet

Milestone

2.20.0

Development

Successfully merging this pull request may close these issues.

3 participants

@Zimmi48 @Villetaneuse @Anteru