Merge branch 'main' into v8.16

.envrc

@@ -0,0 +1 @@
+use flake

.github/workflows/build.yml

@@ -90,8 +90,8 @@ jobs:
       - run: npm ci
       - run: npx --yes vsce ls
 
-  fmt-ocamlfmt:
-    name: Format with ocamlfmt
+  treefmt:
+    name: Format
     runs-on: ubuntu-latest
     steps:
       - name: 🔭 Checkout code
@@ -100,21 +100,5 @@ jobs:
           submodules: recursive
       - name: ❄️ Setup Nix
         uses: cachix/install-nix-action@v18
-      - name: 📐 Format with ocamlfmt
-        run: nix develop .#fmt -c make fmt
-
-  fmt-prettier:
-    name: Format with prettier
-    runs-on: ubuntu-latest
-    defaults:
-      run:
-        working-directory: ./editor/code
-    steps:
-      - name: 🔭 Checkout code
-        uses: actions/checkout@v3
-      - name: 🚀 Setup node
-        uses: actions/setup-node@v3
-        with:
-          node-version: 16
-      - run: npm ci
-      - run: npx prettier -c .
+      - name: 📐 Format with alejandra, ocamlformat, prettier
+        run: nix fmt

.gitignore

@@ -5,3 +5,8 @@ _opam
 .git-ps
 
 *.cache
+
+.direnv
+# Nix build will produce this
+result
+

CHANGES.md

@@ -16,7 +16,7 @@
  - Server is now more strict w.r.t. what URIs it will accept for
    documents, see protocol documentation (@ejgallego, #286, reported
    by Alex Sanchez-Stern)
- - Hypothesis with bodies are now correctly displayed (@ejgallego,
+ - Hypotheses with bodies are now correctly displayed (@ejgallego,
    #296, fixes #293, report by Ali Caglayan)
  - `coq-lsp` incorrectly required the optional `rootPath`
    initialization parameter, moreover it ignored `rootUri` if present
@@ -43,7 +43,29 @@
    #314, fixes #308)
  - Goal display handles background goals better, showing preview,
    goals stack, and focusing information (@ejgallego, #290, fixes
-   #288, based on jsCoq code by Shachar Itzhaky)
+   #288, fixes #304, based on jsCoq code by Shachar Itzhaky)
+ - Warnings are now printed in the info view messages panel
+   (@ejgallego, #315, fixes #195)
+ - Info protocol messages now have location and level
+   (@ejgallego, #315)
+ - Warnings are not printed in the info view messages panel
+   (@ejgallego, #, fixes #195)
+ - Improved `documentSymbol` return type for newer `DocumentSymbol[]`
+   hierarchical symbol support. This means that sections and modules
+   will now be properly represented, as well as constructors for
+   inductive types, projections for records, etc...  (@ejgallego,
+   #174, fixes #121, #122)
+ - [internal] Error recovery can now execute full Coq commands as to
+   amend states, required for #319 (@ejallego, #320)
+ - Auto-admit the previous bullet goal when a new bullet cannot be
+   opened due to an unsolved previous bullet. This also works for {}
+   focusing operators. This is very useful when navigating bulleted
+   proofs (@ejgallego, @Alizter, #319, fixes #300)
+ - Store Ast.Info.t incrementally (@ejgallego, #337, fixes #316)
+ - Basic jump to definition support; due to lack of workspace
+   metadata, this only works inside the same file (@ejgallego, #318)
+ - Show type of identifiers at point on hover (@ejgallego, #321, cc:
+   #164)
 
 # coq-lsp 0.1.4: View
 ---------------------

CONTRIBUTING.md

@@ -78,17 +78,22 @@ You can also use the regular `dune build @check` etc... targets.
 
 #### Nix
 
-We have a Nix flake that you can use. For development, simply run `nix develop`.
+We have a Nix flake that you can use. For development, in the case of the server, simply run `nix develop`.
+In the case of the client, we expose separate shells, e.g client-vscode, would be `nix develop .#client-vscode` (this can be done on top of the original `nix develop`)
 
-If you wish to do `nix build` or compose this flake from another project, you
+You can view the list of packages and devShells that are exposed
+by running `nix flake show`.
+
+If you wish to do `nix build`, you
 will need to use the .?submodules=1` trick, since we use submodules here for
 vendoring. For example, building requires:
 
 ```
 nix build .?submodules=1
 ```
 
-You can use this flake in other flakes or Nix derivations.
+This currently only applies to building the default package (coq-lsp), which is the server. 
+Clients don't have specific submodules as of yet.
 
 #### Releasing