CN server: use local switches for installation instructions and in CI

.github/workflows/server-ci.yml

@@ -31,34 +31,36 @@ jobs:
         with:
           ocaml-compiler: ${{ matrix.ocaml-version }}
 
+      - name: Link lockfile
+        working-directory: cn-lsp/server
+        run: ln -s cnlsp.opam.locked-${{ matrix.ocaml-version }} cnlsp.opam.locked
+
       - name: Restore `_opam`
         id: cache-opam-restore
         uses: actions/cache/restore@v4
         with:
-          path: _opam
-          key: ${{ matrix.ocaml-version }}
+          path: cn-lsp/server/_opam
+          key: ${{ matrix.ocaml-version }}-${{ hashFiles('cn-lsp/server/cnlsp.opam.locked') }}
 
       - name: Install server dependencies
-        working-directory: ./cn-lsp/server
-        run: |
-          eval $(opam env)
-          opam install . --deps-only --locked -y
+        working-directory: cn-lsp/server
+        # If we restored a `_opam` directory here, we need not (and should not)
+        # try to create a switch. The presence of `_opam` seems basically
+        # isomorphic to the presence of a switch, and opam will fail to `create`
+        # a new switch if one is already present.
+        run: ls _opam || opam switch create . ocaml.${{ matrix.ocaml-version }} --deps-only --locked -y
 
       - name: Cache `_opam`
         if: steps.cache-opam-restore.outputs.cache-hit != 'true'
         uses: actions/cache/save@v4
         with:
-          path: _opam
+          path: cn-lsp/server/_opam
           key: ${{ steps.cache-opam-restore.outputs.cache-primary-key }}
 
       - name: Build server
-        working-directory: ./cn-lsp/server
-        run: |
-          eval $(opam env)
-          dune build
+        working-directory: cn-lsp/server
+        run: eval $(opam env) && dune build
 
       - name: Run server tests
-        working-directory: ./cn-lsp/server
-        run: |
-          eval $(opam env)
-          dune test
+        working-directory: cn-lsp/server
+        run: eval $(opam env) && dune test

cn-lsp/client/README.md

@@ -31,8 +31,10 @@ the last step from VSCode's GUI:
 
 Running CN requires that the client be able to find and run a CN language
 server. [Our server's README](../server/README.md) has instructions for a basic
-installation. If you want to control the exact server the client uses, these are
-the locations the client will search (in order) for a server executable:
+installation. In the client, you'll be prompted to select the opam switch you
+created for the server. Your choice is preserved on a per-workspace basis, and
+can be changed by editing your workspace settings. If you don't choose, the
+client will search these locations (in order) for a server executable:
 - The `CN_LSP_SERVER` environment variable
 - On the current `PATH`, for an executable named `cn-lsp-server`
 

cn-lsp/client/package.json

@@ -6,7 +6,7 @@
         "url": "https://github.com/GaloisInc/VERSE-Toolchain",
         "type": "git"
     },
-    "version": "0.0.3",
+    "version": "0.0.4",
     "engines": {
         "vscode": "^1.75.0"
     },
@@ -34,10 +34,20 @@
         "configuration": {
             "title": "CN",
             "properties": {
+                "CN.cerbRuntime": {
+                    "type": "string",
+                    "default": null,
+                    "description": "Location of Cerberus runtime files"
+                },
                 "CN.runOnSave": {
                     "type": "boolean",
                     "default": false,
                     "description": "Run CN whenever a file is saved"
+                },
+                "CN.serverPath": {
+                    "type": "string",
+                    "default": null,
+                    "description": "Location of the LSP server"
                 }
             }
         },

cn-lsp/client/src/extension.ts

@@ -2,20 +2,41 @@ import * as vsc from "vscode";
 import * as ct from "vscode-languageclient/node";
 
 import child_process from "child_process";
+import fs from "fs";
+import path from "path";
 
 let client: ct.LanguageClient;
 
-type Maybe<T> = T | null;
+type Maybe<T> = T | undefined;
 
-export function activate(context: vsc.ExtensionContext): void {
-    const serverPath = findServer(context);
-    if (serverPath === null) {
+export async function activate(context: vsc.ExtensionContext): Promise<void> {
+    let serverContext = getConfiguredServerContext();
+
+    if (serverContext === undefined) {
+        serverContext = await newServerContext(context);
+    }
+
+    if (serverContext === undefined) {
         vsc.window.showErrorMessage("CN client: unable to find CN server");
         throw Error;
     }
+
+    await setConfiguredServerContext(serverContext);
+
+    let env = process.env;
+    if (serverContext.cerbRuntime !== undefined) {
+        env.CERB_RUNTIME = serverContext.cerbRuntime;
+    } else {
+        // TODO: we already tried to get ahold of the runtime when we generated
+        // or retrieved in a server configuration, should we try again?
+    }
+
     const serverOptions: ct.Executable = {
-        command: serverPath,
+        command: serverContext.serverPath,
         transport: ct.TransportKind.pipe,
+        options: {
+            env,
+        },
     };
 
     const clientOptions: ct.LanguageClientOptions = {
@@ -72,23 +93,96 @@ export function deactivate(): Thenable<void> | undefined {
     }
 }
 
-function findServer(context: vsc.ExtensionContext): Maybe<string> {
-    // Is it defined in $CN_LSP_SERVER?
+interface ServerContext {
+    serverPath: string;
+    cerbRuntime?: string;
+}
+
+async function newServerContext(
+    context: vsc.ExtensionContext
+): Promise<Maybe<ServerContext>> {
+    let switches = child_process.spawnSync("opam", ["switch", "list", "-s"], {
+        encoding: "utf-8",
+    });
+    if (switches.status === 0) {
+        let switchNames = switches.stdout.trim().split("\n");
+        let switchName = await vsc.window.showQuickPick(switchNames, {
+            placeHolder:
+                "Which opam switch contains your language server installation?",
+        });
+        if (switchName !== undefined) {
+            // Whether the switch is local or global determines how we find its
+            // opam directory
+            let opamDir: string;
+            if (path.isAbsolute(switchName)) {
+                // The switch is local
+                opamDir = path.join(switchName, "_opam");
+            } else {
+                opamDir = path.join("~", ".opam", switchName);
+            }
+
+            let serverPath = path.join(opamDir, "bin", "cn-lsp-server");
+            let cerbRuntime = path.join(opamDir, "lib", "cerberus", "runtime");
+
+            if (fs.existsSync(serverPath) && fs.existsSync(cerbRuntime)) {
+                return {
+                    serverPath,
+                    cerbRuntime,
+                };
+            }
+        }
+    }
+
     console.log("Looking in $CN_LSP_SERVER");
     console.log(process.env);
     let envPath = process.env.CN_LSP_SERVER;
     if (envPath !== undefined) {
-        return envPath;
+        return { serverPath: envPath };
     }
 
-    // Is it on $PATH?
     console.log("Looking on $PATH");
     const out = child_process.spawnSync("which", ["cn-lsp-server"], {
         encoding: "utf-8",
     });
     if (out.status === 0) {
-        return out.stdout.trim();
+        let serverPath = out.stdout.trim();
+        return { serverPath };
+    }
+
+    return undefined;
+}
+
+function getConfiguredServerContext(): Maybe<ServerContext> {
+    let conf = vsc.workspace.getConfiguration("CN");
+    let serverPath: Maybe<string> = conf.get("serverPath");
+    let cerbRuntime: Maybe<string> = conf.get("cerbRuntime");
+
+    // In practice, despite the type annotations, `conf.get` seems capable of
+    // returning `null` values, so we need to check them
+    if (
+        serverPath !== null &&
+        serverPath !== undefined &&
+        serverPath !== "" &&
+        cerbRuntime !== null &&
+        cerbRuntime !== undefined &&
+        cerbRuntime !== ""
+    ) {
+        return { serverPath, cerbRuntime };
+    } else {
+        return undefined;
     }
+}
 
-    return null;
+async function setConfiguredServerContext(serverContext: ServerContext) {
+    let conf = vsc.workspace.getConfiguration("CN");
+    await conf.update(
+        "cerbRuntime",
+        serverContext.cerbRuntime,
+        vsc.ConfigurationTarget.Global
+    );
+    await conf.update(
+        "serverPath",
+        serverContext.serverPath,
+        vsc.ConfigurationTarget.Global
+    );
 }

cn-lsp/server/README.md

@@ -1,48 +1,21 @@
 # Building and Installing
 
 Begin by installing OCaml and opam, if need be - here are
-[instructions](https://ocaml.org/docs/installing-ocaml) for how to do so. CN and
-Cerberus currently recommend, and build with, OCaml 4.14.1, and that version was
-used to generate the lockfile which this installation process relies on. (I've
-also been able to work with other versions as recent as 5.1.1, but your mileage
-may vary.)
+[instructions](https://ocaml.org/docs/installing-ocaml) for how to do so. This
+build process has been tested with OCaml 4.14.1 and 5.1.1, though other versions
+are likely to work as well.
 
-I recommend creating and using an opam switch to maintain an isolated dependency
-installation and development environment:
+With a choice of version in hand, the easiest way to build this package is with
+a local opam switch, like so:
 ```sh
-opam switch create <switch-name> ocaml.4.14.1
-eval $(opam env --switch=<switch-name> --set-switch)
+VERSION=4.14.1  # or 5.1.1
+ln -s cnlsp.opam.locked-$VERSION cnlsp.opam.locked
+opam switch create . ocaml.$VERSION --locked -y
+eval $(opam env)
 ```
 
-Next, you need to install this project's dependencies. This project depends on
-`cerberus`, `cerberus-lib`, and `cn`, which it will fetch and build from a
-particular commit to their repository. However, if you have previously built
- and/or installed `cn` locally, you may need to uninstall it before installing
-this project's dependencies, or else your existing version may shadow the
-version you're trying to install.
-```sh
-dune uninstall cn
-opam remove cn
-```
-
-Now, install this project's dependencies:
-```sh
-opam install . --deps-only --locked -y
-```
-
-Now, you can build and install the project:
-```sh
-dune build
-(cd bin && dune build)
-dune install
-```
-
-Assuming you're using a switch, this will install a `cn-lsp-server` into
-`$OPAM_SWITCH_PREFIX/bin`. I recommend manually expanding
-`$OPAM_SWITCH_PREFIX/bin` and adding it to your `$PATH` in e.g. `.zshrc`, since
-that's the easiest way for a client to locate a server binary. (The earlier
-`opam env` command will have done this, but only for your current shell.)
-
-If you're not using a switch, you'll need to say `dune install --bindir=$(pwd)`
-instead, which will install a `cn-lsp-server` binary into the current directory.
-You should still ensure the binary is available on your `$PATH`.
+If this command succeeds, it should install the server into your local switch.
+Any clients should run the binary from there. If a client is run outside the
+context of your local switch, it will also need to set `$CERB_RUNTIME` to point
+to Cerberus's runtime file dependencies, which are (currently) installed in the
+switch at `<opam-dir>/lib/cerberus/runtime`.

cn-lsp/server/cnlsp.opam.locked → cn-lsp/server/cnlsp.opam.locked-4.14.1

@@ -1,6 +1,6 @@
 opam-version: "2.0"
 name: "cnlsp"
-version: "~dev"
+version: "dev"
 synopsis: "CN Language Server"
 description: "A language server protocol implementation for the CN language"
 maintainer: "Sam Cowger"
@@ -16,23 +16,20 @@ depends: [
   "cmdliner" {= "1.3.0"}
   "cn" {= "b9daa22"}
   "conf-bash" {= "1"}
-  "conf-c++" {= "1.0"}
   "conf-findutils" {= "1"}
   "conf-gmp" {= "4"}
   "conf-pkg-config" {= "3"}
-  "conf-python-3" {= "9.0.0"}
-  "cppo" {= "1.6.9"}
+  "cppo" {= "1.7.0"}
   "csexp" {= "1.5.2"}
-  "dune" {= "3.16.0"}
-  "dune-configurator" {= "3.16.0"}
-  "fmt" {= "0.9.0"}
+  "dune" {= "3.16.1"}
+  "dune-configurator" {= "3.16.1"}
   "jsonrpc" {= "1.17.0"}
   "lem" {= "2022-12-10"}
   "linol" {= "0.6"}
   "linol-lwt" {= "0.6"}
   "logs" {= "0.7.0"}
   "lsp" {= "1.17.0"}
-  "lwt" {= "5.7.0"}
+  "lwt" {= "5.8.0"}
   "menhir" {= "20240715"}
   "menhirCST" {= "20240715"}
   "menhirLib" {= "20240715"}
@@ -51,21 +48,21 @@ depends: [
   "parsexp" {= "v0.16.0"}
   "pprint" {= "20230830"}
   "ppx_derivers" {= "1.2.1"}
-  "ppx_deriving" {= "6.0.2"}
+  "ppx_deriving" {= "6.0.3"}
+  "ppx_deriving_yojson" {= "3.9.0"}
   "ppx_sexp_conv" {= "v0.16.0"}
   "ppx_yojson_conv_lib" {= "v0.16.0"}
-  "ppxlib" {= "0.32.1"}
+  "ppxlib" {= "0.33.0"}
   "result" {= "1.5"}
   "seq" {= "base"}
   "sexplib" {= "v0.16.0"}
   "sexplib0" {= "v0.16.0"}
   "sha" {= "1.15.4"}
   "stdlib-shims" {= "0.3.0"}
   "topkg" {= "1.0.7"}
-  "trace" {= "0.7"}
+  "trace" {= "0.8"}
   "uutf" {= "1.0.3"}
   "yojson" {= "2.2.2"}
-  "z3" {= "4.13.0-3"}
   "zarith" {= "1.14"}
 ]
 build: [