lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard

feat: server -> client requests

Open mhuisi opened this issue 1 year ago • 1 comments

This PR adds support for requests from the server to the client in the language server. It is based on #3014 and was developed during an experiment for #3247 that unfortunately did not go anywhere.

mhuisi avatar Feb 07 '24 10:02 mhuisi

Mathlib CI status (docs):

  • ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. (2024-02-07 10:29:57)
  • ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ea665de4536061cb8b6a1b32f5b69f09d50ac335 --onto 8b8e001794e6a8b481d37f24fa77bb07797682a1. (2024-02-23 08:58:37)
  • ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 68eaf33e86689e3f303d38e2f071b5e8b7fd172f --onto 317adf42e92a4dbe07295bc1f0429b61bb8079fe. (2024-03-14 15:53:15)