9
$\begingroup$

This follows on from Syntax highlighting for proof assistants, which establishes that it would be nice to have syntax highlighting, but incorrectly concludes that the ball is not in StackExchange's court.

As mentioned in an answer there, the tool StackExchange uses for highlighting, highlight.js, supports Coq (natively) and Lean (via a third-party extension, highlightjs-lean). Note that highlight.js is no longer accepting new languages, so the Lean extension will always be third-party.

The list in the "What is syntax highlighting and how does it work?" meta post mentions that among the enabled languages is:

  • Mathematica / Wolfram Language: lang-mathematica, lang-mma, (lang-wl)
    (Mathematica SE only)

A little more digging reveals that this feature was enabled on Mathematica.SE on 2012-01-18, which was during the Mathematica.SE Private Beta (which ended on 2012-01-25). Inspecting the source reveals this has been done by including an additional https://cdn.sstatic.net/Js/third-party/highlight.js/additional-langs/lang-mma.min.js file that is not present on most SE sites.

Since there is precedent for enabling niche highlighters on other StackExchange sites during their beta phases, can lang-coq () and lang-lean () highlighters be enabled on Proof Assistants? Or is this something that should wait for Beta to end?

Edit: I'm aware that the request to add Julia syntax highlighting is , but thought the situation might be different here since this is not a request for a new site-wide highlighter but just for one SE site, and ProofAssistants certainly does not have the traffic considerations that StackOverflow does!

$\endgroup$
8
  • 2
    $\begingroup$ Thanks for explaining in more detail, what you were possibly trying to convey to me in the comments on ky question! It's much more clear to me now :) $\endgroup$
    – Nike Dattani
    Commented Mar 22, 2022 at 16:47
  • $\begingroup$ @Rob: That's not true any more, if you look at the network traffic for mathematica.stackexchange.com you can see it loads https://cdn.sstatic.net/Js/third-party/highlight.js/additional-langs/lang-mma.min.js?v=5 which is clearly highlight.js and not Prettify. $\endgroup$
    – Eric Mod
    Commented Mar 28, 2022 at 12:27
  • $\begingroup$ It's status-deferred and Coq is not working on SO. $\endgroup$
    – Rob
    Commented Mar 28, 2022 at 13:03
  • $\begingroup$ @Rob: It's not clear to me that either link is relevant. Regarding your first link; that's referring to Julia and StackOverflow, and the considerations for including a new language on SO are clearly quite different than including it on a more niche and low-traffic site like this one. Regarding the second; Mathematica does not work on SO, but does work on Mathematica.SE, so whether things are enabled on SO appears not to be relevant. This question is a request to enable Coq / Lean on Proof Assistants, not network-wide. $\endgroup$
    – Eric Mod
    Commented Mar 28, 2022 at 13:30
  • $\begingroup$ There are languages that are supported (you can see it at work on SO), and a decision that nothing is being changed/added - that doesn't imply that we don't support your request, just that such requests are being refused by staff. --- Also, for us (at PA.SE), it's not just a couple of languages but a number of more site-specific ones (Mizar / ACL2) that all should be included. $\endgroup$
    – Rob
    Commented Mar 28, 2022 at 14:30
  • $\begingroup$ "There are languages that are supported" - yes, I link to that in my question! I think it would be best to wait for a staff opinion on this specific post rather than extrapolate from network-wide requests elsewhere. $\endgroup$
    – Eric Mod
    Commented Mar 28, 2022 at 15:35
  • $\begingroup$ "but a number of more site-specific ones (Mizar / ACL2) that all should be included." - Mizar seems to indeed be supported by highlight.js, but we have no mizar questions right now. If you want to request ACL2, you'll need to write a highlighter for it. I requested coq and lean because those both do have lots of questions, and are supported by highlight.js. $\endgroup$
    – Eric Mod
    Commented Mar 28, 2022 at 15:36
  • $\begingroup$ ACL2 might get by using "Lisp" while we wait; someone more knowledgeable about it than I could probably explain how much of a shortfall there would be. $\endgroup$
    – Rob
    Commented Apr 30, 2022 at 2:23

2 Answers 2

Reset to default
2
$\begingroup$

I'm aware that the request to add Julia syntax highlighting is , but thought the situation might be different here since this is not a request for a new site-wide highlighter but just for one SE site, and ProofAssistants certainly does not have the traffic considerations that StackOverflow does!

Unfortunately, the fact that this is a request that would affect a single site is something that reduces the request's impact and priority. As I mentioned here:

Note that features that need dev time and that are only applicable to your site are unlikely to be given a high priority (...).

For that reason, I'm declining this request.

$\endgroup$
4
  • 4
    $\begingroup$ That's a shame, but thanks for the official reply. As a compromise, would it be possible to enable the default syntax highlighting without any customization? I believe then moderators would have the power to associate lean3 with the lang-haskell highlighter, which is usually a good approximation. $\endgroup$
    – Eric Mod
    Commented May 5, 2022 at 15:13
  • 4
    $\begingroup$ Can do, @Eric — you should be able to make that change yourself now. $\endgroup$
    – JNat StaffMod
    Commented May 5, 2022 at 15:48
  • 1
    $\begingroup$ Thanks @JNat, I've gone ahead and made that change. Hopefully if the Julia situation is eventually revisited, we can maybe revisit this decision. I guess Mathematica had the benefit of being grandfathered in! $\endgroup$
    – Eric Mod
    Commented May 6, 2022 at 15:06
  • $\begingroup$ Downvoting (as it's usual in meta) in order to show disagreement. $\endgroup$
    – Pedro Sánchez Terraf
    Commented Mar 19, 2023 at 23:13
2
$\begingroup$

Update: as can be seen in the accepted answer, this request was rejected.

As a compromise, syntax highlighting is now enabled for the stardard list of languages. Furthermore, has been associated with the haskell syntax highlighter, as this acts as a reasonable approximation.

On questions not tagged with lean3, you can still enable lean-approximation syntax highlighting with

```lean3
def my_lean3_code : sorry := sorry
```

If users of Coq, Agda, or other unsupported languages have recommendations for approximations of useful highlighting via supported languages, then please ask a new question on this meta site; this is something that the moderators for ProofAssistants.SE can handle without needing to escalate to staff.

$\endgroup$
1
  • 1
    $\begingroup$ I added ml highlighting for coq and haskell highlighting for agda. $\endgroup$
    – Couchy
    Commented May 8, 2022 at 17:20

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .