@Rob In this end this is what I went for; the request to add custom highlighting was status-declined. Posts tagged lean3 now use haskell highlighting by default. I don't know what the appropriate choice for Coq is, so haven't made one.

@Eric Thanks! - Now that highlighting is turned on for the site, as-is, I guess this question (linked below) is now status completed (we have as much as we are going to get, without another request; that adds previously declined languages):

Thanks @NikeDattani ^

PS: I wish the first place answer had twice as many votes as the second place answer, but we have nearly 400 views; it seems unlikely.

@PA_Moderators what will be the outcome of this question? Change the chatroom name.

@Rob , I don't really know what you're saying, but this message from @NikeDattani is completely wrong; the request was rejected because there is development work for Stack Exchange.

@Eric Nike (and myself) are saying that there's nothing else needing doing (and no Dev for SE) to have it work as it does today - which is "as-is" (they won't be adding anything). --- If there's a different question about highlighting (on PA) that you'd prefer to mark as SC that's OK too, we have as much as we can expect for the foreseeable future; as per the prior discussion.

Eric's sentence here is "completely wrong". JNat literally said that the reason why it was rejected was because the request was for something that would only serve one site rather than the wider network. Requests that require development work do get accepted on many occasions, for example when they benefit the whole network.

Back to work, nice seeing you Nike.

@NikeDattani You're right, I oversimplified. It was rejected due to being low priority (as it only impacts one site), and due to the high priority threshold that development work requires.

@Eric Yea, I don't quite understand why there's been so much emphasis on how "wrong" people are with this. Even your Meta post says "the previous question incorrectly concluded that there's no development work", which was wording that I thought was unnecessarily antagonistic. My understanding from the accepted answer to the first question on this topic was: SE relies on highlight.js, so the burden of the "development work" is on the developers of highlight.js rather than SE.

If we want something that highlight.js doesn't natively support, then we'll have to do the development work ourselves, but SE is unlikely to do that. There's some basic packages that SE won't even activate for MathJax, even though they'd involve just adding 1 line to the MathJax call, and even though they'd be useful for several of the sites with high traffic (Math.SE, MathOverflow, Stats.SE, etc.).

You raised a good point that they activated syntax highlighting for Mathematica in 2012. However the SE network had a lot less maintenance work to do in 2012 compared to 2022.