Zulip Chat Archive

Stream: general

Topic: adding highlight.js for hugo site

Siddhartha Gadgil (Jan 20 2022 at 09:26):

I just saw that there is lean support for highlight.js, and tried adding it to a static site built with Hugo. Unfortunately nothing was highlighted. Can someone tell me what is wrong? I tried to follow the instructions on the Github repository for the lean-highlight package.

My header includes the following, and I checked all the links are valid.

<script type="text/javascript" src="{{ .Site.BaseURL }}js/highlight.pack.js"></script>
    <script type="text/javascript" charset="UTF-8" src="{{ .Site.BaseURL }}js/lean.min.js"></script>
    <link rel="stylesheet" href="{{ .Site.BaseURL }}css/zenburn.css">
    <script type="text/javascript">
      hljs.initHighlightingOnLoad();
    </script>

The generated code from markdown includes, for example, the following:

<pre><code class="language-lean" data-lang="lean">def sat{dom n: Nat}(clauses : FinSeq dom (Clause (n + 1))) :=
          ∃ valuat : Valuat (n + 1),
           ∀ (p : Nat), ∀ pw : p &lt; dom,
              ∃ (k : Nat), ∃ (kw : k &lt; n + 1),
                (clauses p pw k kw) = some (valuat k kw)
</code></pre>

However, even def is not highlighted.

Thanks.

Eric Wieser (Jan 20 2022 at 09:38):

Is the static site that's failing hosted somewhere publicly?

Eric Wieser (Jan 20 2022 at 09:39):

This looks relevant: https://highlightjs.readthedocs.io/en/latest/api.html#inithighlightingonload

Siddhartha Gadgil (Jan 20 2022 at 09:48):

I see in the console the error hljs.registerLanguage(...) is not a function - perhaps my version of highlight is too old.
I will update and try.

Siddhartha Gadgil (Jan 20 2022 at 09:52):

With the latest version via CDN, I get a different error:

highlight.min.js:290 Uncaught TypeError: Cannot assign to read only property 'name' of function 'e=>{var s={
$pattern:/\w+|\u03bb|\u2200|\u03a0|\u2203|:=?/u,
keyword:"theorem|10 lemma|10 definition def class ...<omitted>...}}'
    at Object.registerLanguage (highlight.min.js:290)
    at lean.min.js:1

Eric Wieser (Jan 20 2022 at 09:52):

See my link above - that function was removed (edit: sorry, I misread the function name in the error message as initHighlightingOnLoad)

Eric Wieser (Jan 20 2022 at 09:53):

I think the lean package is written for highlight.js 10.x

Siddhartha Gadgil (Jan 20 2022 at 09:53):

Unfortunately that function is in lean.min.js, the language package. Should I make an issue there?

Siddhartha Gadgil (Jan 20 2022 at 09:53):

Thanks. Let me try highlight.js 10.x

Eric Wieser (Jan 20 2022 at 09:54):

But also, hljs.initHighlightingOnLoad doesn't exist any more, it's now called hljs.highlightAll()

Siddhartha Gadgil (Jan 20 2022 at 10:00):

Randomly trying a 10.1 package gave the same error. I will make an issue.

Eric Wieser (Jan 20 2022 at 10:04):

I just made a PR to update the readme

Siddhartha Gadgil (Jan 20 2022 at 11:23):

Unfortunately the error persists. There seem to be some similar errors reported for highlight.js, so this may be from upstream. In any case, there is a sample page where the error is visible in the chrome javascript console.

Eric Wieser (Jan 20 2022 at 12:19):

Does it work if you use the "minified" file at the bottom of https://github.com/leanprover-community/highlightjs-lean/actions/runs/1722732424?

Eric Wieser (Jan 20 2022 at 12:19):

sounds like it was an upstream bug, but we can fix it by just rerunning the upstream build tool

Siddhartha Gadgil (Jan 20 2022 at 13:10):

Yes it runs. Thanks a lot.

Eric Wieser (Jan 20 2022 at 13:46):

leanprover-community/highlightjs-lean#12

Bryan Gin-ge Chen (Jan 20 2022 at 14:41):

Thanks Siddhartha and Eric! I'll try and review these today.

Last updated: Dec 20 2023 at 11:08 UTC