diff --git a/.github/workflows/server-ci.yml b/.github/workflows/server-ci.yml index 2ccdf83..0880b85 100644 --- a/.github/workflows/server-ci.yml +++ b/.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 diff --git a/cn-lsp/client/README.md b/cn-lsp/client/README.md index 96c2aaa..e08c136 100644 --- a/cn-lsp/client/README.md +++ b/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` diff --git a/cn-lsp/client/package-lock.json b/cn-lsp/client/package-lock.json index 1916756..6f3e616 100644 --- a/cn-lsp/client/package-lock.json +++ b/cn-lsp/client/package-lock.json @@ -1,12 +1,12 @@ { "name": "cn-client", - "version": "0.0.3", + "version": "0.0.4", "lockfileVersion": 3, "requires": true, "packages": { "": { "name": "cn-client", - "version": "0.0.3", + "version": "0.0.4", "dependencies": { "vscode-languageclient": "^9.0.1" }, diff --git a/cn-lsp/client/package.json b/cn-lsp/client/package.json index 84702e0..4976645 100644 --- a/cn-lsp/client/package.json +++ b/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" } } }, diff --git a/cn-lsp/client/src/extension.ts b/cn-lsp/client/src/extension.ts index 79655ad..a6639c2 100644 --- a/cn-lsp/client/src/extension.ts +++ b/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 | null; +type Maybe = T | undefined; -export function activate(context: vsc.ExtensionContext): void { - const serverPath = findServer(context); - if (serverPath === null) { +export async function activate(context: vsc.ExtensionContext): Promise { + 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 | undefined { } } -function findServer(context: vsc.ExtensionContext): Maybe { - // Is it defined in $CN_LSP_SERVER? +interface ServerContext { + serverPath: string; + cerbRuntime?: string; +} + +async function newServerContext( + context: vsc.ExtensionContext +): Promise> { + 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 { + let conf = vsc.workspace.getConfiguration("CN"); + let serverPath: Maybe = conf.get("serverPath"); + let cerbRuntime: Maybe = 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 + ); } diff --git a/cn-lsp/server/README.md b/cn-lsp/server/README.md index 1ca6e71..b96e680 100644 --- a/cn-lsp/server/README.md +++ b/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 ocaml.4.14.1 -eval $(opam env --switch= --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 `/lib/cerberus/runtime`. diff --git a/cn-lsp/server/cnlsp.opam.locked b/cn-lsp/server/cnlsp.opam.locked-4.14.1 similarity index 87% rename from cn-lsp/server/cnlsp.opam.locked rename to cn-lsp/server/cnlsp.opam.locked-4.14.1 index 214fe0c..a490ac0 100644 --- a/cn-lsp/server/cnlsp.opam.locked +++ b/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,10 +48,11 @@ 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"} @@ -62,10 +60,9 @@ depends: [ "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: [ diff --git a/cn-lsp/server/cnlsp.opam.locked-5.1.1 b/cn-lsp/server/cnlsp.opam.locked-5.1.1 new file mode 100644 index 0000000..3af3e03 --- /dev/null +++ b/cn-lsp/server/cnlsp.opam.locked-5.1.1 @@ -0,0 +1,98 @@ +opam-version: "2.0" +name: "cnlsp" +version: "dev" +synopsis: "CN Language Server" +description: "A language server protocol implementation for the CN language" +maintainer: "Sam Cowger" +authors: "Sam Cowger" +depends: [ + "base" {= "v0.17.1"} + "base-bigarray" {= "base"} + "base-bytes" {= "base"} + "base-domains" {= "base"} + "base-nnp" {= "base"} + "base-threads" {= "base"} + "base-unix" {= "base"} + "cerberus" {= "b9daa22"} + "cerberus-lib" {= "b9daa22"} + "cmdliner" {= "1.3.0"} + "cn" {= "b9daa22"} + "conf-findutils" {= "1"} + "conf-gmp" {= "4"} + "conf-pkg-config" {= "3"} + "cppo" {= "1.7.0"} + "csexp" {= "1.5.2"} + "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.8.0"} + "menhir" {= "20240715"} + "menhirCST" {= "20240715"} + "menhirLib" {= "20240715"} + "menhirSdk" {= "20240715"} + "monomorphic" {= "2.1.0"} + "num" {= "1.5-1"} + "ocaml" {= "5.1.1"} + "ocaml-base-compiler" {= "5.1.1"} + "ocaml-compiler-libs" {= "v0.12.4"} + "ocaml-config" {= "3"} + "ocaml-options-vanilla" {= "1"} + "ocaml_intrinsics_kernel" {= "v0.17.1"} + "ocamlbuild" {= "0.15.0"} + "ocamlfind" {= "1.9.6"} + "ocamlgraph" {= "2.1.0"} + "ocplib-endian" {= "1.2"} + "parsexp" {= "v0.17.0"} + "pprint" {= "20230830"} + "ppx_derivers" {= "1.2.1"} + "ppx_deriving" {= "6.0.3"} + "ppx_deriving_yojson" {= "3.9.0"} + "ppx_sexp_conv" {= "v0.17.0"} + "ppx_yojson_conv_lib" {= "v0.17.0"} + "ppxlib" {= "0.33.0"} + "ppxlib_jane" {= "v0.17.0"} + "result" {= "1.5"} + "seq" {= "base"} + "sexplib" {= "v0.17.0"} + "sexplib0" {= "v0.17.0"} + "sha" {= "1.15.4"} + "stdlib-shims" {= "0.3.0"} + "topkg" {= "1.0.7"} + "trace" {= "0.8"} + "uutf" {= "1.0.3"} + "yojson" {= "2.2.2"} + "zarith" {= "1.14"} +] +build: [ + ["dune" "subst"] {dev} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] +] +pin-depends: [ + [ + "cerberus.b9daa22" + "git+https://github.com/rems-project/cerberus.git#b9daa22" + ] + [ + "cerberus-lib.b9daa22" + "git+https://github.com/rems-project/cerberus.git#b9daa22" + ] + [ + "cn.b9daa22" + "git+https://github.com/rems-project/cerberus.git#b9daa22" + ] +]