need help setting up lean4-infoview

Stream: lean4

[Lua Viana Reis]

Hi! I'm trying to make the browser infoview work with emacs (more about it in #Emacs > ✔ Development: Maintainership @ 💬). I have some questions about the javascript/react side of things that are a struggle to debug for me.

I implemented the editor API and a jsonrpc websocket connection to emacs that are working well, but I'm confused because even after sending the subscribed notifications and calling apis like serverRestarted with the version, nothing happens and I still see "Waiting for Lean server to start...". Perhaps people who have worked in the VSCode or Intellij implementations have helpful suggestions?

[Lua Viana Reis]

See here for the browser application that hosts the infoview

[Lua Viana Reis]

(should I have asked this in #general?)

[Lua Viana Reis]

If I understood the react source well, this message should be gone once serverRestarted is called?

[Lua Viana Reis]

my current approach for debugging what is going on is having the @leanprover/infoview source opened, insert some console.log statements, build it again and make the app use this 'debug version'

[Lua Viana Reis]

but it would be great if there is a better way, this back-and-forth takes time

[Lua Viana Reis]

I solved part of the issues and now the "Waiting for Lean server..." disappears, but now I'm getting errors
image.png

[Lua Viana Reis]

solved as well! they turned out to be silly errors, it's just that it's a pain to figure out what is wrong in js

[Lua Viana Reis]

lots of debug stuff and zero css, but got a working version today!
image.png

[Lua Viana Reis]

now I need to make it pretty

[Lua Viana Reis]

output-2025-05-18-23:47:43.gif

[Lua Viana Reis]

as seen in the gif, there are still two errors when navigating around:

• lean4 server complains it has no handler for $/lean/rpc/release, not sure what is the cause (browsing the lean source, the handler seems to be defined?!)
• json serialization depth exceeded, which is coming from emacs

[Lua Viana Reis]

the problem with the "depth exceeded" error is that the maximum depth is hardcoded in the emacs serializer. I need to investigate what messages are triggering this, and if there is no issue with them, then perhaps I could silence the error

[Lua Viana Reis]

except from proper css, popus are working too 2025-05-19 00-26-29.mp4

[Marc Huisinga]

Lua Viana Reis said:

as seen in the gif, there are still two errors when navigating around:

• lean4 server complains it has no handler for $/lean/rpc/release, not sure what is the cause (browsing the lean source, the handler seems to be defined?!)
• json serialization depth exceeded, which is coming from emacs

$/lean/rpc/release is a notification, not a request. Are you somehow emitting a request by accident?

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

This is very cool! Are you aware of lean4#737? The proposal there was to use emacs-webkit. But if you get this working with an external browser, I think we could consider that issue closed as well.

[Lua Viana Reis]

@Marc Huisinga it's sending a request. This is the exact JSON message that is sent by the LSP connection to the Lean server and its response:

[jsonrpc] e[14:39:46.831] --> $/lean/rpc/release[518] {"jsonrpc":"2.0","id":518,"method":"$/lean/rpc/release","params":{"uri":"file:///home/lua/dados/projetos/codigo/lean/BirkhoffErgodicThm/BirkhoffErgodicThm.lean","sessionId":"11464218239556183073","refs":[{"p":"745"},{"p":"2023"},{"p":"1228"},{"p":"451"},{"p":"1721"},{"p":"206"},{"p":"2706"},{"p":"1115"},{"p":"2401"},{"p":"1604"},{"p":"816"},{"p":"2096"},{"p":"62"},{"p":"1300"},{"p":"1793"},{"p":"2777"},{"p":"2473"},{"p":"411"},...HUNDREDS OF SIMILAR OBJECTS...,{"p":"903"},{"p":"2185"},{"p":"140"},{"p":"1389"},{"p":"609"},{"p":"1880"},{"p":"3171"},{"p":"319"},{"p":"2867"},{"p":"2562"},{"p":"975"},{"p":"2257"},{"p":"247"},{"p":"1461"},{"p":"678"},{"p":"1952"},{"p":"3243"},{"p":"1157"},{"p":"1648"},{"p":"102"},{"p":"3431"},{"p":"2634"},{"p":"1046"},{"p":"2329"},{"p":"1533"}]}}
[jsonrpc] e[14:39:46.833]   <-- $/lean/rpc/release[518] #[0 "\300\301\302\303\304F\305\306\307\310\257\6\207" [:error :code -32601 :message "No request handler found for '$/lean/rpc/release'" :id 518 :jsonrpc "2.0"] 14]

[Lua Viana Reis]

aha, thank you, that was exactly the problem

[Lua Viana Reis]

thank you, it would be very hard for me to find this kind of mistake otherwise

[Lua Viana Reis]

As for the other problem, it happens when trying to serialize this big elisp object: https://gist.github.com/estradilua/d09a7cd2604b52c25f44c50870fe7525

[Lua Viana Reis]

I can't think of a proper fix other than sending an email to emacs-devel asking for them to increase the hardcoded limit of mere 50 nesting levels

[Lua Viana Reis]

but here is a workaround: use json-encode if json-serialize throws an error

(defalias 'jsonrpc--json-encode
  (progn
    (require 'json)
    (defvar json-false)
    (defvar json-null)
    (declare-function json-encode "json" (object))
    (if (fboundp 'json-serialize)
        (lambda (object)
          (condition-case nil
              (json-serialize object
                              :false-object :json-false
                              :null-object nil)
            (error (let ((json-false :json-false)
                         (json-null nil))
                     (json-encode object)))))
      (lambda (object)
        (let ((json-false :json-false)
              (json-null nil)))
        (json-encode object))))
  "Encode OBJECT into a JSON string.")

[Lua Viana Reis]

𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒 said:

This is very cool! Are you aware of lean4#737? The proposal there was to use emacs-webkit. But if you get this working with an external browser, I think we could consider that issue closed as well.

Thanks! The problem with emacs-webkit is that it is unmantained, and the upstream xwidgets build of emacs is broken (explanation). So, right now the only simple way is to have the view in a browser outside of emacs. But the good thing is, if webkit support is brought back in the future, it would already work. (and if you really want it, there are other ways to open a browser inside like eaf)