Email Gateway (Mar 07 2026 at 01:01): Email Gateway (Mar 07 2026 at 01:01):From: Andreas Kurz via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>
Hello,
While testing the Isabelle2025-2 with the VSCode Language Server, I
encountered a crash in the Dynamic_Output session consumer. The error
reported in the LSP logs is:
[ERROR] "rpc" "isabelle" "stderr" '*** Session consumer failure:
"isabelle.vscode.Dynamic_Output"\n*** Bad JSON value:
isabelle.vscode.LSP$$$Lambda/...\n'
Problem:
In isabelle.vscode.LSP.Dynamic_Output, the decorations field is
constructed using decorations.map(_.json). In the current Scala
environment, this appears to trigger an unintended eta-expansion,
because of the definition of Decoration.json(file: JFile). Passing a
lambda function to the JSON serializer rather than evaluating the
underlying data. This results in an error where the Output window would
never be filled.
Fix:
Make the file input in the Decoration Optional and pass a None in case
of the Dynamic_Ouput which will then evaluate to a json null inside of
Decoration.json.
The other use locations of Decoration.json got changed to pass
Some(file).
I have attached the patch to fix this issue to this email.
Kind regards,
Andreas Kurz
Email Gateway (Mar 07 2026 at 13:06):From: Makarius <makarius@sketis.net>
On 07/03/2026 01:51, Andreas Kurz via isabelle-dev wrote:
While testing the Isabelle2025-2 with the VSCode Language Server, I
encountered a crash in the Dynamic_Output session consumer. The error reported
in the LSP logs is:[ERROR] "rpc" "isabelle" "stderr" '*** Session consumer failure:
"isabelle.vscode.Dynamic_Output"\n*** Bad JSON value: isabelle.vscode.LSP$$
$Lambda/...\n'
Thanks for the hint. How did you get this problem? I could not guess on the
spot how to trigger it.
It is mandatory to have a reproducible error situation, before applying any
"fixes" blindy.
I have attached the patch to fix this issue to this email.
Again the ugly word "to fix". I've inspected your change wrt. the history, and
found this spot where I introduced the potential problem:
changeset: 83555:b2857541a531
user: wenzelm
date: Fri Nov 14 22:18:37 2025 +0100
files: src/Tools/VSCode/src/lsp.scala
src/Tools/VSCode/src/pretty_text_panel.scala
src/Tools/VSCode/src/vscode_rendering.scala
description:
clarified signature: more explicit types;
minor performance tuning: postpone ("text_" + colot.toString) after filtering
and grouping;
misc tuning;
So to amend that properly, I need a reproducible error situation, and then
do a change that relates to b2857541a531.
Makarius
Email Gateway (Mar 07 2026 at 23:08):From: Andreas Kurz via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>
While testing the Isabelle2025-2 with the VSCode Language Server, I
encountered a crash in the Dynamic_Output session consumer. The error
reported in the LSP logs is:[ERROR] "rpc" "isabelle" "stderr" '*** Session consumer failure:
"isabelle.vscode.Dynamic_Output"\n*** Bad JSON value:
isabelle.vscode.LSP$$ $Lambda/...\n'Thanks for the hint. How did you get this problem? I could not guess on
the spot how to trigger it.It is mandatory to have a reproducible error situation, before applying
any "fixes" blindy.
I worded this actually very badly. I tested it in Neovim with a plugin
and recieved this above error. I later tried running VSCode to check if
the LSP is still working there.
I ran the VSCode Extension now and there everything seemed to work with
no issues even with this serialization bug. But why?
Server start command for VSCode: isabelle vscode_server -l HOL -o
show_results=false
Server start command for Neovim: isabelle vscode_server -o
vscode_pide_extensions -o vscode_html_output=false -o
editor_output_state
So to amend that properly, I need a reproducible error situation, and
then do a change that relates to b2857541a531.
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@38e3ab38
Then 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 file src/Tools/VSCode/src/pretty_text_panel.scala
if html_output is true it calls
json_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 calls json_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 to LSP.Dynamic_Output.apply in
src/Tools/VSCode/src/dynamic_output.scala:49
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.
Andreas
Last updated: Mar 17 2026 at 17:04 UTC