[doc] [example] Example of a setup with multiple workspaces.

CHANGES.md

@@ -153,6 +153,8 @@
    and info messages appear as diagnostics
  - Display the continous/on-request checking mode in the status bar,
    allow to change it by clicking on it (@ejgallego, #721)
+ - Add an example of multiple workspaces (@ejgallego, @Blaisorblade,
+   #611)
 
 # coq-lsp 0.1.8.1: Spring fix
 -----------------------------

etc/doc/USER_MANUAL.md

@@ -98,7 +98,18 @@ A setting to have `coq-lsp` check documents continuously exists.
 You can tell the server to free up memory with the "Coq LSP: Free
 memory" command.
 
-## Advanced: Multiple workspaces
+## Advanced: Multiple Workspaces
+
+`coq-lsp` does support projects that combine multiple Coq project
+roots in a single workspace. That way, one can develop on several
+distinct Coq developments seamlessly.
+
+To enable this, use the "Add Folder" option in VSCode, where each root
+must be a folder containing a `_CoqProject` file.
+
+Check the example at
+[../../examples/multiple_workspaces/](../../examples/multiple_workspaces/)
+to see it in action!
 
 ## Interrupting coq-lsp
 

examples/multiple_workspaces/README.md

@@ -0,0 +1,42 @@
+# Multiple workspaces setup
+
+## How to run it:
+
+Try to load the `example.code-workspace` file in VSCode.
+
+You may need to compile the right `.vo` files for the imports to
+work. You can do that with the `Save VO command`; as of now, `coq-lsp`
+will require you do this before opening the depending files.
+
+`coq-lsp` will take care of this automatically in the next version,
+including the auto-update. You can also do:
+
+```sh
+$ coqc -R bar bar bar/barx.y
+$ coqc -R foo foo foo/foox.y
+```
+
+## `coq-lsp` workspace documentation
+
+One can add multiple folders or roots to a workspace — for instance
+via the "Add Folder to Workspace" command (or
+[alternatives](https://code.visualstudio.com/docs/editor/multi-root-workspaces#_adding-folders)).
+
+For each workspace added to a project, `coq-lsp` will try to configure
+it by searching for a `_CoqProject` file, then it will apply the
+options found there. In the near future, we will also detect
+`dune-project` files at the root too.
+
+`coq-lsp` does determine the workspace roots using the standard
+methods provided by the LSP protocol, in particular `wsFolders`,
+`rootURI`, and `rootPath` at initialiation, in this order; and by
+listening to the `workspace/didChangeWorkspaceFolders` notification
+after initialization.
+
+## Known problems
+
+When projects are using Coq plugins, `findlib` doesn't properly
+support having multiple roots in the same process. We are using a hack
+that seems to work (we reinitialize `findlib`), however the hack is
+very fragile; we should improve `findlib` upstream to support our use
+case.

examples/multiple_workspaces/bar/_CoqProject

@@ -0,0 +1 @@
+-R . bar

examples/multiple_workspaces/bar/barx.v

@@ -0,0 +1,3 @@
+Definition x := 3.
+
+Print x.

examples/multiple_workspaces/bar/bary.v

@@ -0,0 +1,3 @@
+From bar Require Import barx.
+
+Print x.

examples/multiple_workspaces/example.code-workspace

@@ -0,0 +1,27 @@
+{
+	"folders": [
+		{
+			"path": "bar"
+		},
+		{
+			"path": "foo"
+		}
+	],
+	"settings": {
+		"files.exclude": {
+			"**/*.vo": true,
+			"**/*.vok": true,
+			"**/*.vos": true,
+			"**/*.aux": true,
+			"**/*.glob": true,
+			"**/.git": true,
+			"**/.svn": true,
+			"**/.hg": true,
+			"**/CVS": true,
+			"**/.DS_Store": true,
+			"**/Thumbs.db": true,
+			"**/*.olean": true,
+			"out": false
+		}
+	}
+}

examples/multiple_workspaces/foo/_CoqProject

@@ -0,0 +1 @@
+-R . foo

examples/multiple_workspaces/foo/foox.v

@@ -0,0 +1,3 @@
+Definition x := 3.
+
+Print x.

examples/multiple_workspaces/foo/fooy.v

@@ -0,0 +1,3 @@
+From foo Require Import foox.
+
+Print x.