Skip to content

Commit

Permalink
[doc] [example] Example of a setup with multiple workspaces.
Browse files Browse the repository at this point in the history
Thanks to Arthur Charguéraud for the example.

Co-authored-by: Paolo G. Giarrusso <[email protected]>
  • Loading branch information
ejgallego and Blaisorblade committed May 28, 2024
1 parent 7ba70bc commit 69906fa
Show file tree
Hide file tree
Showing 10 changed files with 97 additions and 1 deletion.
2 changes: 2 additions & 0 deletions CHANGES.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
-----------------------------
Expand Down
13 changes: 12 additions & 1 deletion etc/doc/USER_MANUAL.md
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
42 changes: 42 additions & 0 deletions examples/multiple_workspaces/README.md
Original file line number Diff line number Diff line change
@@ -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.
1 change: 1 addition & 0 deletions examples/multiple_workspaces/bar/_CoqProject
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
-R . bar
3 changes: 3 additions & 0 deletions examples/multiple_workspaces/bar/barx.v
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
Definition x := 3.

Print x.
3 changes: 3 additions & 0 deletions examples/multiple_workspaces/bar/bary.v
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
From bar Require Import barx.

Print x.
27 changes: 27 additions & 0 deletions examples/multiple_workspaces/example.code-workspace
Original file line number Diff line number Diff line change
@@ -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
}
}
}
1 change: 1 addition & 0 deletions examples/multiple_workspaces/foo/_CoqProject
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
-R . foo
3 changes: 3 additions & 0 deletions examples/multiple_workspaces/foo/foox.v
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
Definition x := 3.

Print x.
3 changes: 3 additions & 0 deletions examples/multiple_workspaces/foo/fooy.v
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
From foo Require Import foox.

Print x.

0 comments on commit 69906fa

Please sign in to comment.