Skip to content

[web worker] WASM-based Web Worker#1008

Merged
ejgallego merged 1 commit intomainfrom
wasm
Sep 16, 2025
Merged

[web worker] WASM-based Web Worker#1008
ejgallego merged 1 commit intomainfrom
wasm

Conversation

@ejgallego
Copy link
Collaborator

@ejgallego ejgallego commented Sep 4, 2025 •
edited
Loading

We use Shachar's Itzhaky waCoq/waRocq and OCaml port to WASM to build coq-lsp's WASM worker.

The worker is, for now, tuned to work under VSCode WASM enviroment, but we support a regular browser-based WASM build too.

This makes the extension fully usable in vscode.dev and github.dev, without a Rocq install.

Notes and changes compared to waCoq:

  • we are using OCaml 4.12 for the WASM build. This is quite inconvenient, but we need to update the ocaml-wasm package to 4.14 (or 5.4)

  • due to this, the JSOO build doesn't work due to a bug in the OCaml 4.12 compiler for 32 bits

  • fully working WASM artifact is built in CI

  • a new tool build_fs will build the base filesystem for the workers (fixes [web] Web extension download the Coq filesystem uncompressed. #913)

  • we had to perform some adjustments in the JS bundling setup to make VSCode happy

  • we provide an additional library stub for bigstringaf

  • we have developed an experimental idle loop system, using setTimeout (fixes [js worker] Scheduling and interruption problems #907)

Differences wrt waCoq can be observed in the waCoq PR porting these updates back.

Thanks to Pim J. Otte for very careful testing.

Fixes #907 fixes #908 fixes #913 fixes #931 cc #833

@ejgallego ejgallego added this to the 0.2.4 milestone Sep 4, 2025
@ejgallego ejgallego force-pushed the wasm branch 5 times, most recently from 6735e1c to 5a51593 Compare September 4, 2025 17:10
@ejgallego ejgallego mentioned this pull request Sep 4, 2025
Closed
@ejgallego ejgallego force-pushed the wasm branch 2 times, most recently from 2d51960 to 40f60e3 Compare September 8, 2025 10:51
@ejgallego ejgallego mentioned this pull request Sep 8, 2025
Open
ejgallego added a commit that referenced this pull request Sep 8, 2025
@ejgallego
[internal] Move binaries to lsp-server directory.
51b9bc6 
This will help to have a better source code org for #1008
@ejgallego ejgallego mentioned this pull request Sep 8, 2025
Merged
@ejgallego ejgallego force-pushed the wasm branch 8 times, most recently from 1610083 to 878cc73 Compare September 15, 2025 10:27
@ejgallego
[web worker] WASM-based Web Worker
87f509e 
We use Shachar's Itzhaky waCoq/waRocq and OCaml port to WASM to build
coq-lsp's WASM worker.

The worker is, for now, tuned to work under VSCode WASM enviroment,
but we support a regular browser-based WASM build too.

This makes the extension fully usable in vscode.dev and github.dev,
without a Rocq install.

Notes and changes compared to waCoq:

- we are using OCaml 4.12 for the WASM build. This is quite
  inconvenient, but we need to update the ocaml-wasm package
  to 4.14 (or 5.4)

- due to this, the JSOO build doesn't work due to a bug in the OCaml
  4.12 compiler for 32 bits

- fully working WASM artifact is built in CI

- a new tool `build_fs` will build the base filesystem for the workers
  (fixes #913)

- we had to perform some adjustments in the JS bundling setup to make
  VSCode happy

- we provide an additional library stub for bigstringaf

- we have developed an experimental idle loop system, using
 `setTimeout` (fixes #907)

Differences wrt waCoq can be observed in the waCoq PR porting these
updates back.

Thanks to Pim J. Otte for very careful testing.

Fixes #907 #913

[wip] fix ci for new layout
@ejgallego ejgallego merged commit 58042b7 into main Sep 16, 2025
13 checks passed
@ejgallego ejgallego deleted the wasm branch September 16, 2025 09:42
This was referenced Sep 16, 2025
Closed
Merged
ejgallego added a commit to ejgallego/opam-repository that referenced this pull request Sep 16, 2025
@ejgallego
[new release] coq-lsp (0.2.4+9.0)
50f08b7 
CHANGES:

------------------------------

 - [js] [deps] Bump to findlib 1.9.8, use vanilla API for loading and
   remove our own local wrapper (@ejgallego, rocq-community/rocq-lsp#975).
 - [petanque] New `petanque/ast` and `petanque/ast_at_pos`
   (@ejgallego, @JulesViennotFranca, rocq-community/rocq-lsp#980)
 - [serlib] Support for generic Ast analyzers. This opens the door to
   many feature requests such as syntax coloring, dependency
   extraction, etc... (@ejgallego, @JulesViennotFranca, rocq-community/rocq-lsp#981)
 - [fleche] Support "rocq" markdown delimiters in .mv files
   (@ejgallego, rocq-community/rocq-lsp#987)
 - [workspace] Support _RocqProject (@ejgallego, rocq-community/rocq-lsp#988, fixes rocq-community/rocq-lsp#934)
 - [lsp] [getDocument] Allow to get goals in one shot. We also
   refactor the response type to accommodate different
   meta-data. Note: (!) breaking change. (@ejgallego, rocq-community/rocq-lsp#985, fixes
   rocq-community/rocq-lsp#862, thanks to the Alectryon team)
 - [lsp] Better error handling in URI parsing (@ejgallego, rocq-community/rocq-lsp#994, thanks to
   Adrien from Zulip)
 - [lsp] Better protocol-level handling for our non-standard `Lang.Point`
   and `Lang.Diagnostic` types, via global flags that allow us to
   choose the input/output representation for non-standard field such
   as [Point.offset]. This ensures that leaks of these non-standard
   fields are rarer. (@ejgallego, rocq-community/rocq-lsp#995, cc rocq-community/rocq-lsp#279, cc rocq-community/rocq-lsp#2, thanks to
   Adrien from Zulip)
 - [lsp] [completion] Rework completion configuration into a
   `coq-lsp.completion` json object. The `unicode_completion` setting
   is now deprecated, and has been replaced by
   `completion.unicode.enable` (@ejgallego, rocq-community/rocq-lsp#993)
 - [lsp] [completion] [vscode] Unicode completion commit characters
   are now configurable via the server setting variable
   `completion.unicode.commit_chars`. (@Durbatuluk1701, rocq-community/rocq-lsp#993)
 - [goals] [config] New (global) option for goal display method
   `proof/goals`: `messages_follow_goal`. If `true`, `proof/goals`
   will show errors and messages for the same sentence goals are
   shown; if `false`, it will always show errors and messages for the
   specified `position`, if there is a Rocq sentence at hand
   (@jpoiret, @ejgallego, rocq-community/rocq-lsp#999, fixes: rocq-community/rocq-lsp#941)
 - [coq] Install full state before parsing. Before we did only
   `Pcoq.unfreeze` but that is not enough, in particular the call to
   `get_default_proof_mode` will not be correct (@ejgallego, @pimotte,
   rocq-community/rocq-lsp#1011, fixes rocq-community/rocq-lsp#656)
 - [misc] Don't depend on Jane Street's base (@patrick-nicodemus
   @ejgallego, rocq-community/rocq-lsp#1004)
 - [wasm worker] Add WebAssembly based worker based on waCoq. This is
   now the default for the .vsix binary build. For now, we include
   Rocq's Stdlib and Waterproof (@corwin-of-amber, @ejgallego,
   @pimotte, rocq-community/rocq-lsp#1008, cc rocq-community/rocq-lsp#833, fixes rocq-community/rocq-lsp#907, fixes rocq-community/rocq-lsp#908, fixes rocq-community/rocq-lsp#913)
 - [opam] Added `x-maintenance-intent` intent field. (@ejgallego,
   rocq-community/rocq-lsp#1020)
 - [lsp] [didOpen] `languageId` now takes priority over uri extension
   in LSP `didOpen`. (@ejgallego, rocq-community/rocq-lsp#1021, fixes rocq-community/rocq-lsp#1005)
 - [coq] incorporate experimental `coq-layout-engine` printer, both in
   client and server parts (@ejgallego, rocq-community/rocq-lsp#668, see also rocq-community/rocq-lsp#72 and
   jscoq/jscoq#282 )
 - [lsp] [code] New notification `$/coq/executionInformation` which
   will signal clients when rocq-lsp does intent to start to execute a
   sentence. Experimentally, this is used to provide a red glow on
   long-running commands in coq-lsp/VSCode, to provide better user
   feedback on long-running commands (@ejgallego, suggested by
   @jpoiret, rocq-community/rocq-lsp#1002)
 - [lsp] [outline] Support `Notation`, `Ltac` and `Ltac Notation` in
   outline entries (@ejgallego, rocq-community/rocq-lsp#1025, fixes rocq-community/rocq-lsp#632)
@ejgallego ejgallego mentioned this pull request Sep 16, 2025
Merged
ejgallego added a commit to ejgallego/opam-repository that referenced this pull request Sep 16, 2025
@ejgallego
[new release] coq-lsp (0.2.4+9.1)
88717b7 
CHANGES:

------------------------------

 - [js] [deps] Bump to findlib 1.9.8, use vanilla API for loading and
   remove our own local wrapper (@ejgallego, rocq-community/rocq-lsp#975).
 - [petanque] New `petanque/ast` and `petanque/ast_at_pos`
   (@ejgallego, @JulesViennotFranca, rocq-community/rocq-lsp#980)
 - [serlib] Support for generic Ast analyzers. This opens the door to
   many feature requests such as syntax coloring, dependency
   extraction, etc... (@ejgallego, @JulesViennotFranca, rocq-community/rocq-lsp#981)
 - [fleche] Support "rocq" markdown delimiters in .mv files
   (@ejgallego, rocq-community/rocq-lsp#987)
 - [workspace] Support _RocqProject (@ejgallego, rocq-community/rocq-lsp#988, fixes rocq-community/rocq-lsp#934)
 - [lsp] [getDocument] Allow to get goals in one shot. We also
   refactor the response type to accommodate different
   meta-data. Note: (!) breaking change. (@ejgallego, rocq-community/rocq-lsp#985, fixes
   rocq-community/rocq-lsp#862, thanks to the Alectryon team)
 - [lsp] Better error handling in URI parsing (@ejgallego, rocq-community/rocq-lsp#994, thanks to
   Adrien from Zulip)
 - [lsp] Better protocol-level handling for our non-standard `Lang.Point`
   and `Lang.Diagnostic` types, via global flags that allow us to
   choose the input/output representation for non-standard field such
   as [Point.offset]. This ensures that leaks of these non-standard
   fields are rarer. (@ejgallego, rocq-community/rocq-lsp#995, cc rocq-community/rocq-lsp#279, cc rocq-community/rocq-lsp#2, thanks to
   Adrien from Zulip)
 - [lsp] [completion] Rework completion configuration into a
   `coq-lsp.completion` json object. The `unicode_completion` setting
   is now deprecated, and has been replaced by
   `completion.unicode.enable` (@ejgallego, rocq-community/rocq-lsp#993)
 - [lsp] [completion] [vscode] Unicode completion commit characters
   are now configurable via the server setting variable
   `completion.unicode.commit_chars`. (@Durbatuluk1701, rocq-community/rocq-lsp#993)
 - [goals] [config] New (global) option for goal display method
   `proof/goals`: `messages_follow_goal`. If `true`, `proof/goals`
   will show errors and messages for the same sentence goals are
   shown; if `false`, it will always show errors and messages for the
   specified `position`, if there is a Rocq sentence at hand
   (@jpoiret, @ejgallego, rocq-community/rocq-lsp#999, fixes: rocq-community/rocq-lsp#941)
 - [coq] Install full state before parsing. Before we did only
   `Pcoq.unfreeze` but that is not enough, in particular the call to
   `get_default_proof_mode` will not be correct (@ejgallego, @pimotte,
   rocq-community/rocq-lsp#1011, fixes rocq-community/rocq-lsp#656)
 - [misc] Don't depend on Jane Street's base (@patrick-nicodemus
   @ejgallego, rocq-community/rocq-lsp#1004)
 - [wasm worker] Add WebAssembly based worker based on waCoq. This is
   now the default for the .vsix binary build. For now, we include
   Rocq's Stdlib and Waterproof (@corwin-of-amber, @ejgallego,
   @pimotte, rocq-community/rocq-lsp#1008, cc rocq-community/rocq-lsp#833, fixes rocq-community/rocq-lsp#907, fixes rocq-community/rocq-lsp#908, fixes rocq-community/rocq-lsp#913)
 - [opam] Added `x-maintenance-intent` intent field. (@ejgallego,
   rocq-community/rocq-lsp#1020)
 - [lsp] [didOpen] `languageId` now takes priority over uri extension
   in LSP `didOpen`. (@ejgallego, rocq-community/rocq-lsp#1021, fixes rocq-community/rocq-lsp#1005)
 - [coq] incorporate experimental `coq-layout-engine` printer, both in
   client and server parts (@ejgallego, rocq-community/rocq-lsp#668, see also rocq-community/rocq-lsp#72 and
   jscoq/jscoq#282 )
 - [lsp] [code] New notification `$/coq/executionInformation` which
   will signal clients when rocq-lsp does intent to start to execute a
   sentence. Experimentally, this is used to provide a red glow on
   long-running commands in coq-lsp/VSCode, to provide better user
   feedback on long-running commands (@ejgallego, suggested by
   @jpoiret, rocq-community/rocq-lsp#1002)
 - [lsp] [outline] Support `Notation`, `Ltac` and `Ltac Notation` in
   outline entries (@ejgallego, rocq-community/rocq-lsp#1025, fixes rocq-community/rocq-lsp#632)
@ejgallego ejgallego mentioned this pull request Sep 16, 2025
Merged
ejgallego added a commit to ejgallego/opam-repository that referenced this pull request Sep 19, 2025
@ejgallego
[new release] coq-lsp (0.2.4+8.20)
49ec508 
CHANGES:

------------------------------

 - [js] [deps] Bump to findlib 1.9.8, use vanilla API for loading and
   remove our own local wrapper (@ejgallego, rocq-community/rocq-lsp#975).
 - [petanque] New `petanque/ast` and `petanque/ast_at_pos`
   (@ejgallego, @JulesViennotFranca, rocq-community/rocq-lsp#980)
 - [serlib] Support for generic Ast analyzers. This opens the door to
   many feature requests such as syntax coloring, dependency
   extraction, etc... (@ejgallego, @JulesViennotFranca, rocq-community/rocq-lsp#981)
 - [fleche] Support "rocq" markdown delimiters in .mv files
   (@ejgallego, rocq-community/rocq-lsp#987)
 - [workspace] Support _RocqProject (@ejgallego, rocq-community/rocq-lsp#988, fixes rocq-community/rocq-lsp#934)
 - [lsp] [getDocument] Allow to get goals in one shot. We also
   refactor the response type to accommodate different
   meta-data. Note: (!) breaking change. (@ejgallego, rocq-community/rocq-lsp#985, fixes
   rocq-community/rocq-lsp#862, thanks to the Alectryon team)
 - [lsp] Better error handling in URI parsing (@ejgallego, rocq-community/rocq-lsp#994, thanks to
   Adrien from Zulip)
 - [lsp] Better protocol-level handling for our non-standard `Lang.Point`
   and `Lang.Diagnostic` types, via global flags that allow us to
   choose the input/output representation for non-standard field such
   as [Point.offset]. This ensures that leaks of these non-standard
   fields are rarer. (@ejgallego, rocq-community/rocq-lsp#995, cc rocq-community/rocq-lsp#279, cc rocq-community/rocq-lsp#2, thanks to
   Adrien from Zulip)
 - [lsp] [completion] Rework completion configuration into a
   `coq-lsp.completion` json object. The `unicode_completion` setting
   is now deprecated, and has been replaced by
   `completion.unicode.enable` (@ejgallego, rocq-community/rocq-lsp#993)
 - [lsp] [completion] [vscode] Unicode completion commit characters
   are now configurable via the server setting variable
   `completion.unicode.commit_chars`. (@Durbatuluk1701, rocq-community/rocq-lsp#993)
 - [goals] [config] New (global) option for goal display method
   `proof/goals`: `messages_follow_goal`. If `true`, `proof/goals`
   will show errors and messages for the same sentence goals are
   shown; if `false`, it will always show errors and messages for the
   specified `position`, if there is a Rocq sentence at hand
   (@jpoiret, @ejgallego, rocq-community/rocq-lsp#999, fixes: rocq-community/rocq-lsp#941)
 - [coq] Install full state before parsing. Before we did only
   `Pcoq.unfreeze` but that is not enough, in particular the call to
   `get_default_proof_mode` will not be correct (@ejgallego, @pimotte,
   rocq-community/rocq-lsp#1011, fixes rocq-community/rocq-lsp#656)
 - [misc] Don't depend on Jane Street's base (@patrick-nicodemus
   @ejgallego, rocq-community/rocq-lsp#1004)
 - [wasm worker] Add WebAssembly based worker based on waCoq. This is
   now the default for the .vsix binary build. For now, we include
   Rocq's Stdlib and Waterproof (@corwin-of-amber, @ejgallego,
   @pimotte, rocq-community/rocq-lsp#1008, cc rocq-community/rocq-lsp#833, fixes rocq-community/rocq-lsp#907, fixes rocq-community/rocq-lsp#908, fixes rocq-community/rocq-lsp#913)
 - [opam] Added `x-maintenance-intent` intent field. (@ejgallego,
   rocq-community/rocq-lsp#1020)
 - [lsp] [didOpen] `languageId` now takes priority over uri extension
   in LSP `didOpen`. (@ejgallego, rocq-community/rocq-lsp#1021, fixes rocq-community/rocq-lsp#1005)
 - [coq] incorporate experimental `coq-layout-engine` printer, both in
   client and server parts (@ejgallego, rocq-community/rocq-lsp#668, see also rocq-community/rocq-lsp#72 and
   jscoq/jscoq#282 )
 - [lsp] [code] New notification `$/coq/executionInformation` which
   will signal clients when rocq-lsp does intent to start to execute a
   sentence. Experimentally, this is used to provide a red glow on
   long-running commands in coq-lsp/VSCode, to provide better user
   feedback on long-running commands (@ejgallego, suggested by
   @jpoiret, rocq-community/rocq-lsp#1002)
 - [lsp] [outline] Support `Notation`, `Ltac` and `Ltac Notation` in
   outline entries (@ejgallego, rocq-community/rocq-lsp#1025, fixes rocq-community/rocq-lsp#632)
ejgallego added a commit to ejgallego/opam-repository that referenced this pull request Sep 19, 2025
@ejgallego
[new release] coq-lsp (0.2.4+9.0)
4e7e7cd 
CHANGES:

------------------------------

 - [js] [deps] Bump to findlib 1.9.8, use vanilla API for loading and
   remove our own local wrapper (@ejgallego, rocq-community/rocq-lsp#975).
 - [petanque] New `petanque/ast` and `petanque/ast_at_pos`
   (@ejgallego, @JulesViennotFranca, rocq-community/rocq-lsp#980)
 - [serlib] Support for generic Ast analyzers. This opens the door to
   many feature requests such as syntax coloring, dependency
   extraction, etc... (@ejgallego, @JulesViennotFranca, rocq-community/rocq-lsp#981)
 - [fleche] Support "rocq" markdown delimiters in .mv files
   (@ejgallego, rocq-community/rocq-lsp#987)
 - [workspace] Support _RocqProject (@ejgallego, rocq-community/rocq-lsp#988, fixes rocq-community/rocq-lsp#934)
 - [lsp] [getDocument] Allow to get goals in one shot. We also
   refactor the response type to accommodate different
   meta-data. Note: (!) breaking change. (@ejgallego, rocq-community/rocq-lsp#985, fixes
   rocq-community/rocq-lsp#862, thanks to the Alectryon team)
 - [lsp] Better error handling in URI parsing (@ejgallego, rocq-community/rocq-lsp#994, thanks to
   Adrien from Zulip)
 - [lsp] Better protocol-level handling for our non-standard `Lang.Point`
   and `Lang.Diagnostic` types, via global flags that allow us to
   choose the input/output representation for non-standard field such
   as [Point.offset]. This ensures that leaks of these non-standard
   fields are rarer. (@ejgallego, rocq-community/rocq-lsp#995, cc rocq-community/rocq-lsp#279, cc rocq-community/rocq-lsp#2, thanks to
   Adrien from Zulip)
 - [lsp] [completion] Rework completion configuration into a
   `coq-lsp.completion` json object. The `unicode_completion` setting
   is now deprecated, and has been replaced by
   `completion.unicode.enable` (@ejgallego, rocq-community/rocq-lsp#993)
 - [lsp] [completion] [vscode] Unicode completion commit characters
   are now configurable via the server setting variable
   `completion.unicode.commit_chars`. (@Durbatuluk1701, rocq-community/rocq-lsp#993)
 - [goals] [config] New (global) option for goal display method
   `proof/goals`: `messages_follow_goal`. If `true`, `proof/goals`
   will show errors and messages for the same sentence goals are
   shown; if `false`, it will always show errors and messages for the
   specified `position`, if there is a Rocq sentence at hand
   (@jpoiret, @ejgallego, rocq-community/rocq-lsp#999, fixes: rocq-community/rocq-lsp#941)
 - [coq] Install full state before parsing. Before we did only
   `Pcoq.unfreeze` but that is not enough, in particular the call to
   `get_default_proof_mode` will not be correct (@ejgallego, @pimotte,
   rocq-community/rocq-lsp#1011, fixes rocq-community/rocq-lsp#656)
 - [misc] Don't depend on Jane Street's base (@patrick-nicodemus
   @ejgallego, rocq-community/rocq-lsp#1004)
 - [wasm worker] Add WebAssembly based worker based on waCoq. This is
   now the default for the .vsix binary build. For now, we include
   Rocq's Stdlib and Waterproof (@corwin-of-amber, @ejgallego,
   @pimotte, rocq-community/rocq-lsp#1008, cc rocq-community/rocq-lsp#833, fixes rocq-community/rocq-lsp#907, fixes rocq-community/rocq-lsp#908, fixes rocq-community/rocq-lsp#913)
 - [opam] Added `x-maintenance-intent` intent field. (@ejgallego,
   rocq-community/rocq-lsp#1020)
 - [lsp] [didOpen] `languageId` now takes priority over uri extension
   in LSP `didOpen`. (@ejgallego, rocq-community/rocq-lsp#1021, fixes rocq-community/rocq-lsp#1005)
 - [coq] incorporate experimental `coq-layout-engine` printer, both in
   client and server parts (@ejgallego, rocq-community/rocq-lsp#668, see also rocq-community/rocq-lsp#72 and
   jscoq/jscoq#282 )
 - [lsp] [code] New notification `$/coq/executionInformation` which
   will signal clients when rocq-lsp does intent to start to execute a
   sentence. Experimentally, this is used to provide a red glow on
   long-running commands in coq-lsp/VSCode, to provide better user
   feedback on long-running commands (@ejgallego, suggested by
   @jpoiret, rocq-community/rocq-lsp#1002)
 - [lsp] [outline] Support `Notation`, `Ltac` and `Ltac Notation` in
   outline entries (@ejgallego, rocq-community/rocq-lsp#1025, fixes rocq-community/rocq-lsp#632)
ejgallego added a commit to ejgallego/opam-repository that referenced this pull request Oct 14, 2025
@ejgallego
[new release] coq-lsp (0.2.4+9.1)
5aca7b1 
CHANGES:

------------------------------

 - [js] [deps] Bump to findlib 1.9.8, use vanilla API for loading and
   remove our own local wrapper (@ejgallego, rocq-community/rocq-lsp#975).
 - [petanque] New `petanque/ast` and `petanque/ast_at_pos`
   (@ejgallego, @JulesViennotFranca, rocq-community/rocq-lsp#980)
 - [serlib] Support for generic Ast analyzers. This opens the door to
   many feature requests such as syntax coloring, dependency
   extraction, etc... (@ejgallego, @JulesViennotFranca, rocq-community/rocq-lsp#981)
 - [fleche] Support "rocq" markdown delimiters in .mv files
   (@ejgallego, rocq-community/rocq-lsp#987)
 - [workspace] Support _RocqProject (@ejgallego, rocq-community/rocq-lsp#988, fixes rocq-community/rocq-lsp#934)
 - [lsp] [getDocument] Allow to get goals in one shot. We also
   refactor the response type to accommodate different
   meta-data. Note: (!) breaking change. (@ejgallego, rocq-community/rocq-lsp#985, fixes
   rocq-community/rocq-lsp#862, thanks to the Alectryon team)
 - [lsp] Better error handling in URI parsing (@ejgallego, rocq-community/rocq-lsp#994, thanks to
   Adrien from Zulip)
 - [lsp] Better protocol-level handling for our non-standard `Lang.Point`
   and `Lang.Diagnostic` types, via global flags that allow us to
   choose the input/output representation for non-standard field such
   as [Point.offset]. This ensures that leaks of these non-standard
   fields are rarer. (@ejgallego, rocq-community/rocq-lsp#995, cc rocq-community/rocq-lsp#279, cc rocq-community/rocq-lsp#2, thanks to
   Adrien from Zulip)
 - [lsp] [completion] Rework completion configuration into a
   `coq-lsp.completion` json object. The `unicode_completion` setting
   is now deprecated, and has been replaced by
   `completion.unicode.enable` (@ejgallego, rocq-community/rocq-lsp#993)
 - [lsp] [completion] [vscode] Unicode completion commit characters
   are now configurable via the server setting variable
   `completion.unicode.commit_chars`. (@Durbatuluk1701, rocq-community/rocq-lsp#993)
 - [goals] [config] New (global) option for goal display method
   `proof/goals`: `messages_follow_goal`. If `true`, `proof/goals`
   will show errors and messages for the same sentence goals are
   shown; if `false`, it will always show errors and messages for the
   specified `position`, if there is a Rocq sentence at hand
   (@jpoiret, @ejgallego, rocq-community/rocq-lsp#999, fixes: rocq-community/rocq-lsp#941)
 - [coq] Install full state before parsing. Before we did only
   `Pcoq.unfreeze` but that is not enough, in particular the call to
   `get_default_proof_mode` will not be correct (@ejgallego, @pimotte,
   rocq-community/rocq-lsp#1011, fixes rocq-community/rocq-lsp#656)
 - [misc] Don't depend on Jane Street's base (@patrick-nicodemus
   @ejgallego, rocq-community/rocq-lsp#1004)
 - [wasm worker] Add WebAssembly based worker based on waCoq. This is
   now the default for the .vsix binary build. For now, we include
   Rocq's Stdlib and Waterproof (@corwin-of-amber, @ejgallego,
   @pimotte, rocq-community/rocq-lsp#1008, cc rocq-community/rocq-lsp#833, fixes rocq-community/rocq-lsp#907, fixes rocq-community/rocq-lsp#908, fixes rocq-community/rocq-lsp#913)
 - [opam] Added `x-maintenance-intent` intent field. (@ejgallego,
   rocq-community/rocq-lsp#1020)
 - [lsp] [didOpen] `languageId` now takes priority over uri extension
   in LSP `didOpen`. (@ejgallego, rocq-community/rocq-lsp#1021, fixes rocq-community/rocq-lsp#1005)
 - [coq] incorporate experimental `coq-layout-engine` printer, both in
   client and server parts (@ejgallego, rocq-community/rocq-lsp#668, see also rocq-community/rocq-lsp#72 and
   jscoq/jscoq#282 )
 - [lsp] [code] New notification `$/coq/executionInformation` which
   will signal clients when rocq-lsp does intent to start to execute a
   sentence. Experimentally, this is used to provide a red glow on
   long-running commands in coq-lsp/VSCode, to provide better user
   feedback on long-running commands (@ejgallego, suggested by
   @jpoiret, rocq-community/rocq-lsp#1002)
 - [lsp] [outline] Support `Notation`, `Ltac` and `Ltac Notation` in
   outline entries (@ejgallego, rocq-community/rocq-lsp#1025, fixes rocq-community/rocq-lsp#632)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment