Email Gateway (Mar 09 2026 at 12:55): Email Gateway (Mar 09 2026 at 12:55):From: Makarius <makarius@sketis.net>
[This thread has a new subject to capture the true situation better.]
On 08/03/2026 00:07, Andreas Kurz wrote:
To reproduce this issue in VSCode you have to set
vscode_html_output=false
in settings.
[Info - 11:54:53 PM] Welcome to Isabelle/HOL (Isabelle2025-2)
*** Session consumer failure: "isabelle.vscode.Dynamic_Output"
*** Bad JSON value: isabelle.vscode.LSP$$$Lambda/0x00007ff0244844c0@38e3ab38Then I get the same error as I do in Neovim.
I also have a good guess why it does fail with html_output=false, but not with
html_output=true.
In filesrc/Tools/VSCode/src/pretty_text_panel.scala
- if html_output is true it callsjson_output(HTML.source(html).toString, None)(line 60), the decorations parameter is None it will not include the
"decorations" key in json.
- if html_output is false it callsjson_output(converted_text, Some(LSP.Decoration(entries)))(line 81), the decorations are not None and
therefore they are serialized to a eta expansion.
where json_output is set toLSP.Dynamic_Output.applyinsrc/Tools/VSCode/ src/dynamic_output.scala:49
That is really bad. The deeper problem is that the author, Thomas Lindae, has
made variants of the Isabelle/LSP implementation, specifically for his private
Neovim experiments. The details, and expectations of the other side, are left
implicit, though.
So we have an unmaintainable situations, or "bogs" instead of "bugs".
While I know Neovim falls outside the officially supported environments, this
bug affects the LSP servers JSON serialization under certain configurations,
so it would be great if this could be addressed.
Can you point to the relevant Neovim sources, presumably also by Thomas Lindae?
We need explicit proof that it is worth keeping it for now, and not remove the
bad code paths in Isabelle/LSP, to avoid such problems.
Note that Isabelle has this principle of "garbage collection on sources" for
unused/unmaintained material.
Makarius
Email Gateway (Mar 09 2026 at 15:18):From: Andreas Kurz via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>
On 2026-03-09 13:46, Makarius wrote:
While I know Neovim falls outside the officially supported
environments, this bug affects the LSP servers JSON serialization
under certain configurations, so it would be great if this could be
addressed.Can you point to the relevant Neovim sources, presumably also by Thomas
Lindae?
So the Neovim plugin that I use is this one:
https://github.com/Treeniks/isabelle-lsp.nvim
The initialization of the server or rather the definition of the command
is done here:
https://github.com/Treeniks/isabelle-lsp.nvim/blob/master/lua/utils.lua#L9
ofcourse with the option vscode_html_output=false set to false, then
rendering the content directly with the decorations in the terminal.
We need explicit proof that it is worth keeping it for now, and not
remove the bad code paths in Isabelle/LSP, to avoid such problems.Note that Isabelle has this principle of "garbage collection on
sources" for unused/unmaintained material.
This makes total sense, reduce the complexity and simplify to the actual
needed things.
If you plan to create a general LSP that works for editors outside of
VSCode then a JSON protocol would be prefered. (I see that this is a big
undertaking for a (currently) small reward.)
Email Gateway (Mar 09 2026 at 15:53):From: Makarius <makarius@sketis.net>
On 09/03/2026 16:17, Andreas Kurz wrote:
On 2026-03-09 13:46, Makarius wrote:
While I know Neovim falls outside the officially supported environments,
this bug affects the LSP servers JSON serialization under certain
configurations, so it would be great if this could be addressed.Can you point to the relevant Neovim sources, presumably also by Thomas Lindae?
So the Neovim plugin that I use is this one: https://github.com/Treeniks/
isabelle-lsp.nvim
The initialization of the server or rather the definition of the command is
done here: https://github.com/Treeniks/isabelle-lsp.nvim/blob/master/lua/
utils.lua#L9
ofcourse with the optionvscode_html_output=falseset to false, then
rendering the content directly with the decorations in the terminal.
I've looked through this briefly. Thomas Lindae boldly claims "This plugin
requires changeset aa77be3e8329 or later of Isabelle to work." as if there
would be a global principle of monotonicity on the changeset history, without
any precautions to actually get there.
I will not give a lecture on proper software design and maintenance. Instead,
I have now produced this change:
changeset: 84196:f9bed2fc64c8
tag: tip
user: wenzelm
date: Mon Mar 09 16:40:21 2026 +0100
files: src/Tools/VSCode/src/lsp.scala
src/Tools/VSCode/src/vscode_resources.scala
description:
recover json_entries from b2857541a531: required for unproven Neovim
experiments, see also isabelle.vscode.Pretty_Text_Panel with
vscode_html_output=false;
renamed "json" to "notification", to emphasize its semantics;
That does not mean that the Neovim experiment will still work for the next
Isabelle release, it can easily break again the way it has been done. Someone
who cares about it needs to actively support its case within the specified
time window: https://sketis.net/2025/plan-for-isabelle2026-october-2026
If you plan to create a general LSP that works for editors outside of VSCode
then a JSON protocol would be prefered.
We don't plan that, because LSP, despite its popularity, needs to be counted
as a failure. It covers too few aspects of what is really required. And the
JSON wrapping for the protocol messages is a performance bottle-neck.
Whenever we redo Isabelle/VSCode seriously, there will be a more direct,
non-JSON protocol.
Makarius
Last updated: Mar 17 2026 at 17:04 UTC