Unicode highlight in Coq (or other lang)

[Huxpro]

This issue is similar to #621 or #831 where the Unicodes are highlighted with a bold concrete background (I guess it's an error?).
It looks like #621 is fixed by manually accepting more alphabet symbols.
Could there be a unified fix for deemphasizing the lex errors on Unicode?

Noted that using Unicode here in Coq is actually syntactically invalid but yet a common way in writing (say the Software Foundation books). Trying to highlight Agda code (where Unicode is universally used) with Haskell will encounter a similar issue.

[pyrmont]

@Huxpro Yeah, a way to deemphasise errors is an interesting idea. The difficulty is how to do that? The simplest way I can think of would be to insert an additional class into the generated HTML that users could then use to affect the styling.

Oh, and could you copy and paste the example text you tried to lex? Sorry the dingus isn't accepting new saves at the moment :(

[Huxpro]

Thx @pyrmont. I guess brutely override .highlight .err as whatever in user-land could workaround but I agreed how to do it elegantly is tricky.

here is the code:

Theorem ev_plus4 : ∀n, even n → even (4 + n).
Proof.
  intros n H. simpl.
  apply ev_SS.
  apply ev_SS.
  apply H.
Qed.

[pyrmont]

@Huxpro I would also like to have a fix for the Coq lexer that allows the types of characters commonly used in the community.

The difficulty I'm having is finding a regular expression that doesn't match symbols that are used as punctuation or as operators (there are alternatives to this approach but this is my preferred solution). The ∀ character, for example, is part of the 'Math Symbol' general category but so is the + character.

Are there a common set of additional characters used that we want to (effectively) whitelist? Or do people use any old Unicode character they feel like?

[jneen]

you can actually put those characters literally in a regex, if they're common enough we may want to add them to haskell/coq.

[pyrmont]

@jneen Yeah, that's kind of where my mind was going too :)

[Huxpro]

@pyrmont Coq has some meta-programming power so it might be tricky to cover all cases... essentially, math symbols commonly used in logic and set theory are most used and might be sufficient:

A tentative list could be

• def/implications ⇒ → ↔ ⇔ ≔ ≡
• quantification ∀ ∃
• logical connectives /\ \/ ∧ ∨ ¬
• top/bottom ⊤ ⊥
• proof/entail ⊢ ⊨
• set ∈...

A code example could be:

Theorem progress : ∀t T,
  empty ⊢ t ∈ T →
  value t ∨ ∃t', t --> t'.

I just realized Rouge used by Jekyll is version-frozen and my tentative uses were for Github Pages so my temporary workaround (in less) is:

.language-coq .highlight .err {
  &:extend(.highlight .k);
  background-color: transparent;
}

[tomtomjhj]

Some coq projects make heavy use of unicode indentifiers and notations and their highlighting is severely broken on gitlab. Example: https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris_heap_lang/adequacy.v

Github's highlighter seems to ignore everything it doesn't recognize, and I think that is much more readable in general.

[pyrmont]

@tomtomjhj I'm no longer maintaining Rouge but have reopened the issue.

[stale]

This issue has been automatically marked as stale because it has not had any activity for more than a year. It will be closed if no additional activity occurs within the next 14 days.
If you would like this issue to remain open, please reply and let us know if the issue is still reproducible.