diff --git a/.vscodeignore b/.vscodeignore index 36da8fa..22beb62 100644 --- a/.vscodeignore +++ b/.vscodeignore @@ -3,3 +3,31 @@ **/*.map **/.eslintrc.json node_modules/.bin/** + +# Development-only files. They belong in the repository and not in a .vsix: the +# tests drive the client against a real filesystem and cannot run inside an +# installed extension, and install.sh is the OTHER way to install this — shipping +# it inside the thing it installs is a loop that can only confuse. scripts/ is +# the same argument: version.sh edits this repository's files and +# package-extension.sh builds the very artifact it would be riding in. +test/** +scripts/** +install.sh +package-lock.json +CLA.md +CONTRIBUTING.md + +# Repository plumbing. `vsce ls` is the only thing that shows these — they are +# invisible in the source tree and would otherwise ride along into every .vsix. +.mailmap +.github/** + +# NOT ignored, deliberately: +# docs/** — README.md embeds docs/images/writ-mark-200.png, so the marketplace +# page loses its mark without it. 44K, and worth it. +# icons/** — the activity bar container and the language's file icon are +# contributed by PATH; an extension whose icon 404s draws nothing +# at all, and nothing is exactly as visible as a wrong icon. +# src/** — the extension itself. `main` is extension.js and every line of +# behaviour is a require away from it. +# LICENSE, NOTICE, AUTHORS — AGPL-3.0-or-later; the notices ship with the work. diff --git a/DEVELOPING.md b/DEVELOPING.md new file mode 100644 index 0000000..e7ef1a7 --- /dev/null +++ b/DEVELOPING.md @@ -0,0 +1,54 @@ +# Working on the Writ extension + +This is for people changing the extension. To use it, the [README](README.md) is enough; to send a patch, see [CONTRIBUTING.md](CONTRIBUTING.md) first. + +There is no compile step: every LSP request is answered by the OCaml server, so +a build pipeline would exist to typecheck glue. What the glue has instead is +structure — `extension.js` is the wiring, and one module per concern under +`src/`: + +| | | +| --- | --- | +| `locate.js` | where the engine is: the candidate order, the checkout a server came from, and the `writ` belonging to it | +| `watcher.js` | restart when the server binary is replaced | +| `staleness.js` | is the built server older than the sources it was built from | +| `engine.js` | what engine this editor is talking to, and the verdict on it | +| `panel.js` | the Activity Bar view | +| `commands.js` | the verbs | + +Only `extension.js` and each module's `register` touch the `vscode` API. The +rest is plain JavaScript that runs under node — which is what the tests +exercise, with nothing stubbed and nothing installed: + +```console +$ scripts/test.sh +``` + +Five files, and each one is there because its subject fails **silently**: + +| | | +| --- | --- | +| `test/watcher.test.js` | a watcher that never fires looks exactly like a server that is up to date | +| `test/resolve.test.js` | the wrong candidate order means "no language server" on a machine that has one | +| `test/status.test.js` | the verdict is shown to users as a warning; getting it wrong means telling someone with a good install that it is broken | +| `test/manifest.test.js` | nothing typechecks `package.json` — a command contributed but not registered appears in the palette and does nothing | +| `test/engine.test.js` | the engine is a separate install — a capability `writ-lsp` stops advertising, or a flag the CLI renames, leaves the extension running and doing nothing. It drives the real server and runs each command line the verbs build; with no `writ-lsp` on PATH it skips, and `WRIT_E2E_REQUIRED=1` makes that a failure | + +## The version + +The extension and the engine are released together and live in separate +repositories, so nothing structural keeps them in step — and the panel now +*shows* a mismatch to the user, which makes a version that is merely forgotten +into a warning on somebody's working install. + +```console +$ scripts/version.sh # print them, and fail if they disagree +$ scripts/version.sh 0.2.0 # set them +$ scripts/version.sh --from-writ # set them to what a writ checkout says +``` + +It reads writ's own version from the `dune-project` of a checkout beside this +one, or of `$WRIT_REPO`. `install.sh` derives its extension id from the manifest +rather than holding a copy, so the only two places left are `package.json` and +the `.vsix` filename in the README. + diff --git a/README.md b/README.md index 5d3f2e7..72bddfc 100644 --- a/README.md +++ b/README.md @@ -1,164 +1,161 @@ -# Writ language support for VS Code - -writ - -*The editor client for [writ](https://github.com/writ-lang/writ). The language, -the checker and the language server live there; this repository is the VS Code -front end and nothing else.* - -Editor support for **Writ** — *Partial Olog*, an abstract language for modelling -real-world domains — over all three of its file types: - -| | | -| --- | --- | -| `.writ` | models and libraries — schema, instance, transitions | -| `.claims` | the questions asked of a model, kept as their own document | -| `.rules` | Datalog-style derivations over a model's situation space | - -Syntax highlighting, plus everything the language's own server provides: -diagnostics from the real parser and type-checker, a document outline, hover -and completion. - -**The extension does not bundle a server and does not download one.** The point -of an OCaml server is that the editor and the checker are the *same code*, so a -diagnostic in the editor is one `writ check` would give you. It talks to a -`writ-lsp` you already have. - -## Install - -Two routes. The extension tries them in this order. - -### With writ installed, and no checkout - -The ordinary case. The extension needs `writ-lsp` on your `PATH`: +# Writ extension for Visual Studio Code + +[![AGPL-3.0 License](https://img.shields.io/badge/license-AGPL--3.0-blue.svg)](https://www.gnu.org/licenses/agpl-3.0) + +Writ is a language for modelling a rule-governed world and getting every +consequence back, with the route. This extension is its editor: highlighting +for all three file types, and diagnostics, outline, hover and completion +served by the language's own OCaml server, so what the editor says is what +`writ check` says. + +![A writ model and a claim about it](https://raw.githubusercontent.com/writ-lang/writ-vscode/main/docs/images/river-example.png) + +## Features + +- Syntax highlighting for `.writ` models, `.claims` question files and + `.rules` derivations +- Diagnostics from the real parser and type-checker, as you type +- Document outline, hover and completion, all from the server +- Check this file, with the sibling `.claims` attached; from a `.claims` file + the roles swap and the model becomes the argument +- Show a situation, answer a relation, compare with another model, each in a + terminal, each with the `writ` that belongs to the same install as the + server, never whatever is first on `PATH` +- A panel in the Activity Bar that shows which writ you are actually talking + to: both versions, the server's path, and whether they are in step +- The server restarts itself when its binary changes on disk, so a fresh + `make build` is what answers, not the process from before it + +**The extension bundles no server and downloads none.** The point of an +OCaml server is that the editor and the checker are the same code. It talks +to a `writ-lsp` you already have. + +## Supported + +| Piece | Where it comes from | +| ------------- | ----------------------------------------------------------------------------------- | +| `writ-lsp` | [writ](https://github.com/writ-lang/writ): an opam pin, a release tarball, or a checkout built with `make build` | +| VS Code | 1.82 or later | +| Remote windows| The extension runs on the workspace side, next to the server | + +### Feature Contributions + +- **Language:** Writ (`.writ`, `.claims`, `.rules`), with grammar +- **View:** a writ mark in the Activity Bar with an Overview panel +- **Keybinding:** `Ctrl+K Ctrl+Enter` checks this file +- **Commands** in the Command Palette under **Writ**, and in the editor and + explorer context menus: Check This File; Show a Situation…; Answer a + Relation…; Compare With Another Model…; Open the Writ Panel; Restart the + Language Server; Show the Server Log; Build the Engine; Update writ…; + Settings +- **Activation:** on opening a Writ file, or the panel + +## Getting Started + +**You need writ too.** The ordinary route needs `writ-lsp` on your `PATH`: ```console $ opam pin add writ git+https://github.com/writ-lang/writ.git # or unpack a release tarball -$ command -v writ-lsp # confirm it is on PATH +$ command -v writ-lsp /home/you/.opam/default/bin/writ-lsp ``` -`writ` is not in opam-repository, so there is no `opam install writ` to run — the -pin is the no-checkout route, and opam does the cloning. The other ways to get -one (a release tarball, `make install-writ` from a checkout) are in -[writ's README](https://github.com/writ-lang/writ#install); any of them puts -`writ-lsp` on your `PATH`, which is all this extension needs. - -Then install the extension — from a `.vsix`, or by linking it (below) — and -open a `.writ` file. Nothing to configure. +`writ` is not in opam-repository, so the pin is the no-checkout route. The +other ways to get one are in [writ's README](https://github.com/writ-lang/writ#install); +any of them puts `writ-lsp` on your `PATH`, which is all this extension needs. -### From this repository +Then install the extension. From this repository: ```console $ ./install.sh ``` -That fetches the extension's dependencies, links the extension into every VS -Code extensions directory it finds, and **verifies the server answers a -handshake** — so a success message means it works, not merely that it -installed. With no `writ-lsp` yet it warns and installs anyway: the server is -resolved when the extension activates, so installing writ afterwards is a -perfectly good order to do things in. - -Dropped inside a checkout of [writ](https://github.com/writ-lang/writ) instead — -as `tooling/vscode/` — the same script builds the server from source first, and -that build wins over any installed one. That is what you want while changing -the language itself. - -Then reload the window (Ctrl+Shift+P → *Developer: Reload Window*). -VS Code only scans its extensions directory at startup, which is the one step a -script cannot do for you. - -Re-running is safe. To remove it: - -```console -$ ./install.sh --uninstall -``` - -The install is a **symlink** into the extensions directory, so editing this repo -updates the extension with no reinstall — and moving or deleting the clone -breaks it, which is the trade. +That fetches the dependencies, links the extension into every VS Code +extensions directory it finds, and verifies the server answers a handshake, +so a success message means it works. With no `writ-lsp` yet it warns and +installs anyway; installing writ afterwards is a fine order. Given a checkout +of writ inside or beside this one, it builds the server from source first, +and that build wins over an installed one. Then reload the window +(Developer: Reload Window); VS Code scans its extensions directory only at +startup. -### Requirements - -`npm`, for `vscode-languageclient`. Everything else is the server, which comes -from [writ](https://github.com/writ-lang/writ) — this repository contains no OCaml -and builds nothing. - -### Packaging it instead +Or package a `.vsix`: ```console -$ npm install -$ npx @vscode/vsce package +$ scripts/package-extension.sh $ code --install-extension writ-0.1.0.vsix ``` -Or open this repository in VS Code and press F5 for an Extension -Development Host. +Open a `.writ` file. Nothing to configure. -## The setting +## Usage -**`writ.serverPath`** — default -`_build/default/tooling/lsp/bin/writ_lsp.exe`. +**Check.** `Ctrl+K Ctrl+Enter`, or the ▷ in the editor title, runs +`writ check` on the file with its sibling `.claims` attached if there is one. +Squiggles while you type come from the same checker, so the two never +disagree unless the server is stale, and the panel tells you when it is. -- A **relative** path is resolved against each open workspace folder, so the - default finds a checkout's own build with nobody editing a setting. -- If no workspace folder has it, **`writ-lsp` is looked up on `PATH`** — which is - what an opam pin or a release tarball provides, and is how this extension - works with no checkout at all. -- An **absolute** path is used exactly as given and nothing else is tried: if - you name a server, you mean that server. +**The verbs**, from the Command Palette or the panel: -If none exists, the extension says so and names what it looked for. Silence -would be worse — a server that starts and answers nothing looks identical to a -broken one, and is much harder to chase. +| Command | Runs | +| ------------------------------- | -------------------------------------------------------------------- | +| **Show a Situation…** | `writ show --at N` | +| **Answer a Relation…** | `writ derive` over a `.rules` file; prefix the question with `why ` for the derivation tree | +| **Compare With Another Model…** | `writ compare` against a model you pick | -## It restarts itself when the server changes +**The panel.** Click the writ mark in the Activity Bar, or run **Writ: Open +the Writ Panel** if the icon ended up unpinned. It prints both versions, the +server's path, and a verdict. Every way this can be wrong produces the same +symptom, an editor that highlights and says nothing else, and the causes +want different fixes: -`make build` writes a *new* file over the server; a process already running -keeps the old one. Without this the editor goes on answering with a language one -build out of date, and the symptom is a squiggle on code the CLI accepts — at -its most confusing exactly when you are changing the language. +| It says | What happened | The button | +| ----------------------------------------- | ----------------------------------------------- | -------------------- | +| no language server | nothing was found at any candidate path | build, or update writ| +| older than `core/…` | the checkout was edited since it was built | build the engine | +| the engine is *x*, the extension is *y* | one of the two was installed on its own | build, or update writ| +| the server did not say which writ it is | a writ from before the server reported one | update writ | -The client watches the binary and restarts on its own. **View → Output → "Writ -Language Server"** shows which server it launched, and says so when it swaps: +The stale case is the one nothing else catches: a build from before this +morning's edit reports the same version as a current one. The panel compares +times, and offers the build. -``` -[client] server: /home/you/writ/_build/default/tooling/lsp/bin/writ_lsp.exe -[client] server binary changed on disk — restarting (…) -[client] server restarted; diagnostics are from the current build -``` +**The server log.** View, Output, "Writ Language Server" shows which server +was launched and says so when it swaps after a rebuild. -## If something looks wrong +## Configuration -- **A diagnostic you disagree with** — `writ check` is the authority; same code, - no process to go stale. If they differ, the server is stale, and the output - channel above shows whether it restarted. -- **No diagnostics at all** — check that channel for which server was launched, - or whether the extension reported finding none. -- **A `(load …)` resolving to the wrong file** — `WRIT_TRACE_LOADS=1 writ check - FILE` prints what each load actually resolved to. A `stdlib.writ` sitting - beside your model replaces the installed one, by design and silently. +| Setting | Default | Description | +| ----------------- | ---------------------------------------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------- | +| `writ.serverPath` | `_build/default/tooling/lsp/bin/writ_lsp.exe` | A relative path is resolved against each open workspace folder, so the default finds a checkout's own build. If none has it, `writ-lsp` is looked up on `PATH`. An absolute path is used exactly as given. | -## Development +If nothing exists at any of those, the extension says so and names what it +looked for. -`extension.js` is the whole client, and there is no compile step: every LSP -request is answered by the OCaml server, so a build pipeline would exist to -typecheck sixty lines of glue. +## Troubleshooting -Two behaviours have tests, because both fail **silently** when broken: +- **A diagnostic you disagree with.** `writ check` is the authority. If they + differ, the server is stale; the output channel shows whether it restarted. +- **No diagnostics at all.** Check that channel for which server was + launched, or whether the extension reported finding none. +- **A `(load …)` resolving to the wrong file.** `WRIT_TRACE_LOADS=1 writ check + FILE` prints what each load resolved to. A `stdlib.writ` beside your model + replaces the installed one, by design and silently. +- **Removing a linked install:** `./install.sh --uninstall`. The install is a + symlink into the extensions directory, so moving the clone breaks it. -```console -$ node test-watcher.js # the restart-on-rebuild watcher -$ node test-resolve.js # where the server is looked for -``` +## Developing the Extension -Run them here: the editor client is its own repository now, so writ has no -target that runs them. `vscode` and `vscode-languageclient` are stubbed at the -module loader, so neither needs an editor. +- Open this repository in VS Code and press F5 for an Extension Development + Host. There is no compile step; every request is answered by the server. +- `scripts/test.sh` runs the tests under plain node, nothing stubbed. +- `scripts/version.sh` keeps the extension's version in step with writ's. +- [DEVELOPING.md](DEVELOPING.md) has the module map, what each test guards + against, and the version scheme. Patches need the CLA in + [CONTRIBUTING.md](CONTRIBUTING.md). ## License -Copyright (C) 2026 Alex Kunich. **GNU Affero General Public License, version 3 -or later** — the same as [writ](https://github.com/writ-lang/writ) itself. See +Copyright (C) 2026 Alex Kunich. GNU Affero General Public License, version 3 +or later, the same as [writ](https://github.com/writ-lang/writ) itself. See [LICENSE](LICENSE). diff --git a/docs/images/river-example.png b/docs/images/river-example.png new file mode 100644 index 0000000..dd3a421 Binary files /dev/null and b/docs/images/river-example.png differ diff --git a/docs/images/river-example.svg b/docs/images/river-example.svg new file mode 100644 index 0000000..ee9dea8 --- /dev/null +++ b/docs/images/river-example.svg @@ -0,0 +1,16 @@ + + +;; river.writ, the farmer, the wolf, the goat and the cabbage +(schema river + (type bank (left right)) + (type thing (arrow at (to bank)))) + +(transition cross-goat-LR + (when (and (is farmer.at left) (is goat.at left))) + (do (set farmer.at right) (set goat.at right))) + +;; river.claims, the questions live beside the model +(property solvable "everything can reach the right bank intact" + (possible (and (is farmer.at right) (is wolf.at right) + (is goat.at right) (is cabbage.at right)))) + \ No newline at end of file diff --git a/extension.js b/extension.js index 75fe710..c6f405c 100644 --- a/extension.js +++ b/extension.js @@ -1,194 +1,142 @@ // Copyright (C) 2026 Alex Kunich // SPDX-License-Identifier: AGPL-3.0-or-later -// The VS Code client. It does one thing: find the server this repository built -// and hand it to vscode-languageclient over stdio. +// The VS Code client. // -// There is no compile step and no TypeScript here on purpose. Every LSP request -// the editor answers is answered by the OCaml server, so a build pipeline would -// exist to typecheck sixty lines of glue. +// It does one thing that matters: find the writ this workspace means and hand +// its language server to vscode-languageclient over stdio. Everything the +// editor answers — diagnostics, outline, hover, completion — is answered by the +// OCaml server, so that a squiggle here is one `writ check` would give. +// +// There is no compile step and no TypeScript, on purpose: a build pipeline +// would exist to typecheck glue. What the glue does have is structure, one +// module per concern under src/, and only this file and each module's +// [register] touch the vscode API — the rest is plain JavaScript that runs +// under node, which is what test/ exercises. -const fs = require("fs"); -const path = require("path"); const vscode = require("vscode"); const { LanguageClient, TransportKind } = require("vscode-languageclient/node"); -const SETTING = "writ.serverPath"; -const POLL_MS = 2000; - -let client; -let watcher; +const engine = require("./src/engine"); +const locate = require("./src/locate"); +const staleness = require("./src/staleness"); +const watcher = require("./src/watcher"); +const commands = require("./src/commands"); +const panel = require("./src/panel"); -// Restart the server when its binary is replaced. -// -// WHY THIS EXISTS. `make build` writes a NEW inode over the server, and the -// process already running keeps the old one — `/proc/PID/exe` reads -// "(deleted)". Nothing surfaces that. The editor keeps answering, confidently, -// with a language that is one build out of date, and the symptom is a squiggle -// on code the CLI accepts. That has cost real debugging time more than once, -// and it is worst exactly when the language itself is being changed, because -// then the stale answer is *plausible*. -// -// Polling rather than [createFileSystemWatcher]: the default server path is -// under `_build`, which is routinely listed in `files.watcherExclude`, and a -// watcher that silently never fires would be a worse version of this same bug. -// One stat every two seconds is not a cost worth optimising. -function watchServerBinary(serverPath, log, pollMs = POLL_MS) { - let known = stampOf(serverPath); - let pending = null; - - const id = setInterval(async () => { - const now = stampOf(serverPath); - if (now === null) return; // mid-build: the file is briefly gone - if (now === known) { - pending = null; // nothing new, or a change that reverted - return; - } - if (pending !== now) { - // Seen a change, but act only once it has stopped moving, so a - // multi-second link step restarts the server once and not four times. - pending = now; - return; - } - known = now; - pending = null; - log(`server binary changed on disk — restarting (${serverPath})`); - try { - await client.restart(); - log("server restarted; diagnostics are from the current build"); - } catch (e) { - vscode.window.showErrorMessage( - `Writ: the language server changed on disk but would not restart: ${e}. ` + - "Reload the window to pick it up." - ); - } - }, pollMs); +let watching; - return { dispose: () => clearInterval(id) }; -} - -// Identity of the file as built, not merely its name: dune replaces the -// executable, so the inode changes even when a rebuild lands within the same -// mtime granularity. -function stampOf(p) { - try { - const s = fs.statSync(p); - return `${s.ino}:${s.mtimeMs}:${s.size}`; - } catch { - return null; - } -} - -// The name an installed writ puts on PATH (tooling/lsp/bin/dune's -// public_name). NOT the same as the in-checkout file name, which is -// `writ_lsp.exe` under _build. -const INSTALLED = "writ-lsp"; - -function onPath(exe) { - const dirs = (process.env.PATH || "").split(path.delimiter).filter(Boolean); - const names = process.platform === "win32" ? [exe + ".exe", exe] : [exe]; - return dirs.flatMap((d) => names.map((n) => path.join(d, n))); -} - -// Where to look for the server, in order. Returns every path tried, so a -// failure can name them rather than say "not found". -// -// TWO AUDIENCES, and the order is which one gets served first. A CHECKOUT of -// this repository builds its own server, and that one must win — the whole -// point of an OCaml server is that the editor and the checker are the same -// code, so a developer changing the language wants the build in front of them -// and not whatever is installed. Everyone ELSE has installed writ (by pin, or -// unpacked a release) and has no checkout at all; for them the relative default -// resolves to nothing, and `writ-lsp` on PATH is the only server there is. +// Say what is missing, once, and offer the two things that fix it. // -// Serving only the first audience is what this did until now, which meant the -// extension could not be used with writ installed separately — the case -// tooling/lsp/bin/dune installs `writ-lsp` for in the first place. -// -// An ABSOLUTE setting is taken literally and nothing is guessed after it: an -// operator who names a server means that server. -function candidates(configured) { - if (path.isAbsolute(configured)) return [configured]; - const folders = vscode.workspace.workspaceFolders || []; - const inWorkspace = folders.map((f) => path.join(f.uri.fsPath, configured)); - return [...inWorkspace, ...onPath(INSTALLED)]; -} - -function activate(context) { - const configured = vscode.workspace - .getConfiguration() - .get(SETTING, "_build/default/tooling/lsp/bin/writ_lsp.exe"); - const tried = candidates(configured); - const found = tried.find((p) => fs.existsSync(p)); - - if (!found) { - // Silence here would look like a server that starts and answers nothing, - // which is the same symptom as a broken server and much harder to chase. - // - // The PATH candidates are summarised rather than listed: naming forty - // directories buries the one thing worth reading, which is that `writ-lsp` - // was not in any of them. - const inWorkspace = tried.filter((p) => !onPath(INSTALLED).includes(p)); - const where = inWorkspace.length - ? `not at ${inWorkspace.join(", ")}, and \`${INSTALLED}\` is not on PATH` - : `\`${INSTALLED}\` is not on PATH`; - vscode.window.showErrorMessage( +// Silence here would look like a server that starts and answers nothing, which +// is the same symptom as a broken server and much harder to chase. The PATH +// candidates are summarised rather than listed: naming forty directories buries +// the one thing worth reading, which is that `writ-lsp` was not in any of them. +function reportMissing(tried) { + const onPath = locate.onPath(locate.INSTALLED); + const inWorkspace = tried.filter((p) => !onPath.includes(p)); + const where = inWorkspace.length + ? `not at ${inWorkspace.join(", ")}, and \`${locate.INSTALLED}\` is not on PATH` + : `\`${locate.INSTALLED}\` is not on PATH`; + vscode.window + .showErrorMessage( `Writ: no language server — ${where}. ` + "In a checkout of the writ repository, run `make build`. Otherwise " + "install writ (`opam pin add writ git+https://github.com/writ-lang/writ.git`, " + "or a release tarball) so " + - `\`${INSTALLED}\` is on PATH — or set \`${SETTING}\` to an absolute ` + - "path to the server you want." - ); + `\`${locate.INSTALLED}\` is on PATH — or set \`${engine.SETTING}\` to an ` + + "absolute path to the server you want.", + "Open the Writ panel", + "Open settings" + ) + .then((choice) => { + if (choice === "Open the Writ panel") + vscode.commands.executeCommand("writ.openOverview"); + else if (choice === "Open settings") + vscode.commands.executeCommand("writ.openSettings"); + }); +} + +// Start the server, or record that there is none. Separated from [activate] so +// that a changed setting can redo exactly this and nothing else. +async function start(context) { + const state = engine.resolve(); + + // The panel and the commands are registered whether or not a server was + // found — the panel is where the absence is explained, so it must exist + // precisely when there is nothing to talk to. + if (!state.serverPath) { + reportMissing(state.tried); + panel.refresh(); return; } - const serverOptions = { - command: found, - args: [], - transport: TransportKind.stdio, - }; - - const clientOptions = { - documentSelector: [{ scheme: "file", language: "writ" }], - outputChannelName: "Writ Language Server", - }; - - client = new LanguageClient( + const client = new LanguageClient( "writ", "Writ Language Server", - serverOptions, - clientOptions + { command: state.serverPath, args: [], transport: TransportKind.stdio }, + { + documentSelector: [{ scheme: "file", language: "writ" }], + outputChannelName: "Writ Language Server", + } ); - + engine.attach(client); context.subscriptions.push(client); - const started = client.start(); + await client.start(); + + // Which writ answered. This is the whole reason the server reports serverInfo: + // the extension and the engine are separate installs and nothing else can tell + // them apart. See the panel, which is where the comparison is shown. + const version = engine.readVersion(client); const log = (m) => client.outputChannel.appendLine(`[client] ${m}`); - log(`server: ${found}`); - watcher = watchServerBinary(found, log); - context.subscriptions.push(watcher); + log(`server: ${state.serverPath}`); + log(`engine: ${version || "did not report a version"}`); + if (state.checkout) log(`checkout: ${state.checkout}`); + if (state.cli) log(`command line: ${state.cli}`); + + watching = watcher.watchServerBinary(state.serverPath, log, undefined, { + restart: () => engine.restart(), + onRestart: () => { + staleness.markBuilt(); + panel.refresh(); + }, + onFailure: (e) => + vscode.window.showErrorMessage( + `Writ: the language server changed on disk but would not restart: ${e}. ` + + "Reload the window to pick it up." + ), + }); + context.subscriptions.push(watching); + panel.refresh(); +} - return started; +function activate(context) { + panel.register(context); + commands.register(context); + + context.subscriptions.push( + // The server may have moved, so everything derived from it is suspect: which + // binary, which version, whether it is stale, and whether it is running at + // all. Reloading the window used to be the only way to pick up a corrected + // setting. + vscode.workspace.onDidChangeConfiguration(async (event) => { + if (!event.affectsConfiguration("writ")) return; + if (watching) watching.dispose(); + const client = engine.current().client; + if (client) await client.stop().catch(() => {}); + engine.attach(null); + await start(context); + }) + ); + + return start(context); } function deactivate() { - if (watcher) watcher.dispose(); + if (watching) watching.dispose(); + const client = engine.current().client; return client ? client.stop() : undefined; } module.exports = { activate, deactivate }; - -// Exposed for tooling/vscode/test-watcher.js, which drives the watcher against a -// real file on disk. The watcher is the one part of this glue with behaviour of -// its own, and a watcher that silently never fires is the bug it exists to fix. -module.exports.__test = { - watchServerBinary, - stampOf, - candidates, - onPath, - INSTALLED, - setClient: (c) => { - client = c; - }, -}; diff --git a/icons/writ-activitybar.svg b/icons/writ-activitybar.svg new file mode 100644 index 0000000..ab27424 --- /dev/null +++ b/icons/writ-activitybar.svg @@ -0,0 +1,23 @@ + +writ + + + + + + + + diff --git a/icons/writ-file-dark.svg b/icons/writ-file-dark.svg new file mode 100644 index 0000000..08c90db --- /dev/null +++ b/icons/writ-file-dark.svg @@ -0,0 +1,19 @@ + +writ + + + + + + + + diff --git a/icons/writ-file-light.svg b/icons/writ-file-light.svg new file mode 100644 index 0000000..be0c5ca --- /dev/null +++ b/icons/writ-file-light.svg @@ -0,0 +1,19 @@ + +writ + + + + + + + + diff --git a/install.sh b/install.sh index 902a078..8c36f19 100755 --- a/install.sh +++ b/install.sh @@ -3,24 +3,56 @@ # SPDX-License-Identifier: AGPL-3.0-or-later # Install the .writ language support into VS Code. # -# ./tooling/vscode/install.sh # build, install, verify -# ./tooling/vscode/install.sh --uninstall # remove it again +# ./install.sh # build, install, verify +# ./install.sh --uninstall # remove it again # # Safe to re-run. Installs as a symlink into every VS Code extensions directory # it finds, so editing this repo updates the extension with no reinstall. set -euo pipefail here=$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd) -ext_id="writ.writ-0.1.0" - -# INSIDE a writ checkout or not. This script ships with the extension, and the -# extension is usable both ways: from the writ repository, where the server is -# built from source two levels up, and on its own against a `writ-lsp` that -# an installed writ already put on PATH. Deciding by looking for the engine -# rather than by assuming, because `$here/../..` is a real directory either -# way — it is simply not the writ repo when the extension lives alone. -repo=$(cd "$here/../.." && pwd) -if [ -f "$repo/dune-project" ] && [ -d "$repo/core/stdlib" ]; then +# The extension id VS Code files this under: publisher.name-version, from the +# manifest. READ rather than written down — a hardcoded copy here was a fourth +# place the version lived, and the one nobody thinks of at bump time: install +# under a stale id and the new extension lands BESIDE the old one, both +# manifests valid, and VS Code loads whichever it scans first. See +# scripts/version.sh for the copies that remain. +field() { sed -n "s/^ \"$1\": \"\(.*\)\",\?$/\1/p" "$here/package.json" | head -1; } +ext_id="$(field publisher).$(field name)-$(field version)" + +# Extension ids this extension has been installed under BEFORE. The project was +# called `pol` (Partial Olog) and the extension `pol.pol`; see "rename: pol +# becomes writ". Kept so the rename can be migrated rather than left behind — +# purge_legacy below is the only thing that ever cleans these up. +legacy_globs=("pol.pol-*") + +# WHERE THE ENGINE IS. This script ships with the extension, and the extension is +# usable three ways, so the answer is looked up rather than assumed: +# +# 1. $WRIT_REPO — set it to say exactly which checkout to build. +# 2. $here/../.. — the extension living INSIDE a writ checkout, at +# tooling/vscode/, which is where it started. +# 3. $here/../writ — the extension as its OWN repository, checked out +# beside the engine. This is what the split into +# writ/ and writ-vscode/ actually produces, and +# looking only at `../..` missed it entirely: two +# levels up from a sibling checkout is the +# directory that CONTAINS both, never the engine. +# 4. no checkout at all — writ installed by opam pin or release tarball, +# where `writ-lsp` on PATH is the only server. +# +# Identified by the engine's own files, not by name, so a checkout in a directory +# called something else is still found. +is_repo() { [ -f "$1/dune-project" ] && [ -d "$1/core/stdlib" ]; } + +repo="" +for cand in "${WRIT_REPO:-}" "$here/../.." "$here/../writ"; do + [ -n "$cand" ] && [ -d "$cand" ] || continue + cand=$(cd "$cand" && pwd) + if is_repo "$cand"; then repo="$cand"; break; fi +done + +if [ -n "$repo" ]; then in_checkout=yes server="$repo/_build/default/tooling/lsp/bin/writ_lsp.exe" else @@ -52,8 +84,50 @@ mapfile -t ext_dirs < <(find_extension_dirs) [ -n "${ext_dirs[0]:-}" ] || die "no VS Code extensions directory found. Open this folder in VS Code once (which creates it), then re-run this script." +# Remove an install made under a name this extension no longer uses. +# +# WHY THIS EXISTS. An install from before the rename is a symlink named +# `pol.pol-0.1.0` pointing at a directory the rename took away. VS Code scans the +# extensions directory, cannot read a manifest through a dangling link, and +# reports "invalid extensions detected", naming `pol` — an extension the user +# CANNOT remove from the UI, because there is nothing behind it to uninstall. +# The marketplace pane then offers to "Install Locally" a ghost. Nothing in the +# renamed script removed it, so every pre-rename install stayed broken and +# visible. Run on install as well as uninstall: the person hitting this is +# installing the new extension, not uninstalling an old one they forgot about. +# +# `-e` is false for a dangling symlink, which is exactly the case to clean, so +# the test is `-e OR -L` and the removal is `rm -rf` on the link itself — never +# through it, which would delete a live checkout. +purge_legacy() { + local d g p + for d in "${ext_dirs[@]}"; do + for g in "${legacy_globs[@]}"; do + for p in "$d"/$g; do + [ -e "$p" ] || [ -L "$p" ] || continue + rm -rf "$p" + say "removed a pre-rename install: $p" + done + done + done + # VS Code also keeps a registry, and an entry there outlives the directory — + # it is what re-reports the extension as invalid. Only its own CLI can edit it + # safely, so ask, and stay quiet when the entry is already gone. + if command -v code >/dev/null 2>&1; then + local id + for g in "${legacy_globs[@]}"; do + id="${g%-*}" + if code --list-extensions 2>/dev/null | grep -qx "$id"; then + code --uninstall-extension "$id" >/dev/null 2>&1 && \ + say "deregistered $id from VS Code" + fi + done + fi +} + # ---------------------------------------------------------------- uninstall -- if [ "${1:-}" = "--uninstall" ]; then + purge_legacy for d in "${ext_dirs[@]}"; do if [ -e "$d/$ext_id" ] || [ -L "$d/$ext_id" ]; then rm -rf "$d/$ext_id" @@ -64,6 +138,8 @@ if [ "${1:-}" = "--uninstall" ]; then exit 0 fi +purge_legacy + # -------------------------------------------------------------------- build -- if [ "$in_checkout" = yes ]; then say "building the language server" @@ -104,20 +180,26 @@ done # ------------------------------------------------------------------- verify -- # Prove the server actually answers, rather than trusting that it built. A # handshake here is the difference between "installed" and "works". -say "verifying the server responds" -init='{"jsonrpc":"2.0","id":1,"method":"initialize","params":{"processId":null,"rootUri":null,"capabilities":{}}}' -exit_msg='{"jsonrpc":"2.0","method":"exit"}' -reply=$(printf 'Content-Length: %d\r\n\r\n%sContent-Length: %d\r\n\r\n%s' \ - "${#init}" "$init" "${#exit_msg}" "$exit_msg" \ - | "$server" 2>/dev/null | tr -d '\r' || true) - -case "$reply" in - *documentSymbolProvider*completionProvider*|*completionProvider*documentSymbolProvider*) - say "server answered with its capabilities" ;; - *) - warn "the server did not answer a handshake as expected. The extension is +# +# Skipped, not attempted, when there is no server: the no-checkout path above +# already said why, and piping into an empty command name would report a shell +# error about "" instead of the thing that is actually true. +if [ -n "$server" ] && [ -x "$server" ]; then + say "verifying the server responds" + init='{"jsonrpc":"2.0","id":1,"method":"initialize","params":{"processId":null,"rootUri":null,"capabilities":{}}}' + exit_msg='{"jsonrpc":"2.0","method":"exit"}' + reply=$(printf 'Content-Length: %d\r\n\r\n%sContent-Length: %d\r\n\r\n%s' \ + "${#init}" "$init" "${#exit_msg}" "$exit_msg" \ + | "$server" 2>/dev/null | tr -d '\r' || true) + + case "$reply" in + *documentSymbolProvider*completionProvider*|*completionProvider*documentSymbolProvider*) + say "server answered with its capabilities" ;; + *) + warn "the server did not answer a handshake as expected. The extension is installed, but check: $server" ;; -esac + esac +fi cat </dev/null 2>&1 || { echo "npx is not installed" >&2; exit 1; } + +scripts/version.sh >/dev/null || { + echo "the version is inconsistent — see scripts/version.sh" >&2 + exit 1 +} +version=$(sed -n 's/^ "version": "\(.*\)",$/\1/p' package.json) + +# The dependencies are SHIPPED: vscode-languageclient is the one thing this +# extension does not get from the engine, and a .vsix without node_modules +# activates to a module-not-found. +if [ ! -d node_modules/vscode-languageclient ]; then + echo "==> installing dependencies" + if [ -f package-lock.json ]; then + npm ci --no-audit --no-fund + else + npm install --no-audit --no-fund + fi +fi + +npx --yes @vscode/vsce package --out "writ-$version.vsix" + +echo +echo "built writ-$version.vsix" +echo "install it with: code --install-extension writ-$version.vsix" +echo +echo "it needs a writ-lsp to talk to; see scripts/version.sh for whether this" +echo "version matches the engine beside it." diff --git a/scripts/test.sh b/scripts/test.sh new file mode 100755 index 0000000..bef713c --- /dev/null +++ b/scripts/test.sh @@ -0,0 +1,20 @@ +#!/bin/sh +# Copyright (C) 2026 Alex Kunich +# SPDX-License-Identifier: AGPL-3.0-or-later +# +# Every test, in plain node. No runner and nothing to install: this repository's +# one dependency is vscode-languageclient, and a test framework would be the +# second — for four files that each print a line. +set -e +cd "$(dirname "$0")/.." + +failed=0 +for t in test/*.test.js; do + node "$t" || failed=1 +done + +# The version is not a test file, but it is checked the same way and by the same +# people at the same moment. +scripts/version.sh >/dev/null || failed=1 + +[ "$failed" = 0 ] || { echo; echo "some checks FAILED" >&2; exit 1; } diff --git a/scripts/version.sh b/scripts/version.sh new file mode 100755 index 0000000..a2c15dd --- /dev/null +++ b/scripts/version.sh @@ -0,0 +1,90 @@ +#!/bin/sh +# Copyright (C) 2026 Alex Kunich +# SPDX-License-Identifier: AGPL-3.0-or-later +# +# The version, in the two places here that have to agree — and against the +# engine, which is the version that decides. +# +# scripts/version.sh print them, and fail if they disagree +# scripts/version.sh 0.2.0 set them +# scripts/version.sh --from-writ set them to what a writ checkout says +# +# WHY THIS EXISTS. The extension and the engine ship together and are separate +# repositories, so nothing structural keeps them in step: writ's version lives +# in its dune-project and is generated into the binary and the opam package, +# while this repository writes it into package.json by hand. +# +# install.sh used to hold a third copy, as the extension id — the one nobody +# thinks of at bump time, and the one with teeth: install under a stale id and +# the new extension lands BESIDE the old one, both manifests valid, and VS Code +# loads whichever it scans first. It now reads the manifest instead, which is +# why it is not listed below. The README's .vsix filename cannot be derived the +# same way, so it stays here. +# +# The panel compares the extension's version against the engine's at runtime and +# reports a mismatch to the user, which is what makes this worth enforcing here: +# a version that is wrong is not a cosmetic problem any more, it is a warning +# shown to someone whose install is fine. +set -e +cd "$(dirname "$0")/.." + +pkg=$(sed -n 's/^ "version": "\(.*\)",$/\1/p' package.json) +doc=$(sed -n 's/.*code --install-extension writ-\(.*\)\.vsix.*/\1/p' README.md) + +# The engine's version, if a checkout is at hand. Read from dune-project rather +# than by running the binary: this must work in a checkout that has not been +# built, and dune-project is the source `writ --version` is generated from. +writ_version() { + for cand in "${WRIT_REPO:-}" ../writ ..; do + [ -n "$cand" ] && [ -f "$cand/dune-project" ] || continue + sed -n 's/^(version \(.*\))$/\1/p' "$cand/dune-project" | head -1 + return + done +} + +set_all() { + sed -i "s/^ \"version\": \".*\",$/ \"version\": \"$1\",/" package.json + sed -i "s/code --install-extension writ-.*\.vsix/code --install-extension writ-$1.vsix/" README.md +} + +if [ "${1:-}" = "--from-writ" ]; then + engine=$(writ_version) + [ -n "$engine" ] || { + echo "no writ checkout found — set WRIT_REPO, or pass the version" >&2 + exit 1 + } + set_all "$engine" + echo "$pkg -> $engine (from the engine)" + exit 0 +fi + +if [ -n "${1:-}" ]; then + set_all "$1" + echo "$pkg -> $1" + exit 0 +fi + +printf 'package.json %s\n' "$pkg" +printf 'README.md %s\n' "$doc" + +engine=$(writ_version) +if [ -n "$engine" ]; then + printf 'writ %s (the engine, from its dune-project)\n' "$engine" +else + printf 'writ — (no checkout beside this one; set WRIT_REPO to compare)\n' +fi + +if [ "$pkg" != "$doc" ]; then + echo "they disagree; run: scripts/version.sh $pkg" >&2 + exit 1 +fi + +# A version behind the engine is a real state — the extension is released when +# it changes, and it does not change every time writ does — so this is reported +# and not failed. What is failed above is the copies here contradicting each +# other, which is never anything but a mistake. +if [ -n "$engine" ] && [ "$pkg" != "$engine" ]; then + echo "note: the extension is $pkg and the engine is $engine." >&2 + echo " the panel will show that as a mismatch to anyone with both." >&2 + echo " run: scripts/version.sh --from-writ" >&2 +fi diff --git a/src/commands.js b/src/commands.js new file mode 100644 index 0000000..0994bde --- /dev/null +++ b/src/commands.js @@ -0,0 +1,353 @@ +// Copyright (C) 2026 Alex Kunich +// SPDX-License-Identifier: AGPL-3.0-or-later + +// The commands. +// +// Every one of them runs the SAME writ the language server is: `engine.current().cli` +// is derived from the resolved server, never looked up on its own. That is the +// whole point — an editor whose "check this file" disagrees with its own +// squiggles would be worse than having no command at all. +// +// The verbs run in a terminal, not a task and not an output channel: `writ +// check` prints a report meant to be read, `writ derive --why` prints a tree, +// and both are things you scroll back through and re-run with an edited +// argument. A task would file them under the Problems view, which is where the +// server's diagnostics already live and where a report is not a diagnostic. +// +// [build] is the exception, and for the opposite reason: nobody reads a build +// log that succeeded, and the one thing that has to be known about it is +// whether it did. Only a task reports an exit code. + +const fs = require("fs"); +const path = require("path"); +const engine = require("./engine"); +const staleness = require("./staleness"); +const panel = require("./panel"); + +let terminal = null; + +function shell() { + const vscode = require("vscode"); + if (!terminal || terminal.exitStatus !== undefined) { + terminal = vscode.window.createTerminal("writ"); + } + terminal.show(true); + return terminal; +} + +// Quote for a shell, because these are typed into a terminal. +function quote(s) { + return /[^\w@%+=:,./-]/.test(s) ? "'" + s.replace(/'/g, "'\\''") + "'" : s; +} + +// The CLI, or a complaint that says what to do about not having one. Every verb +// goes through this, so the message is written once. +function cli() { + const vscode = require("vscode"); + const found = engine.current().cli; + if (found) return found; + vscode.window + .showWarningMessage( + "Writ: no `writ` command line to run. The language server answers " + + "diagnostics, but the verbs need the CLI, which ships beside it.", + "Open the Writ panel" + ) + .then((c) => { + if (c) vscode.commands.executeCommand("writ.openOverview"); + }); + return null; +} + +function run(args) { + const found = cli(); + if (!found) return; + shell().sendText([quote(found), ...args.map(quote)].join(" ")); +} + +// The file a command acts on: the one the explorer offered, else the active +// editor's. Saved first when it is dirty, because the CLI reads the disk and +// checking the previous save is a confusing kind of wrong answer. +async function target(uri) { + const vscode = require("vscode"); + const editor = vscode.window.activeTextEditor; + const chosen = uri && uri.fsPath ? uri : editor ? editor.document.uri : null; + if (!chosen) { + vscode.window.showInformationMessage("Writ: no file to act on."); + return null; + } + if ( + editor && + editor.document.uri.toString() === chosen.toString() && + editor.document.isDirty + ) + await editor.document.save(); + return chosen.fsPath; +} + +// The model a .claims or .rules file belongs to. +// +// A sibling of the same name first — the convention writ's own help states +// ("A model's questions live beside it in MODEL.claims") — and a pick over the +// workspace's models when there is none, rather than an error. Splitting +// questions from models is deliberate in this language; one question suite is +// meant to be asked of several models, and a command that could only ever ask +// the sibling would be arguing with the design. +async function modelFor(file) { + const vscode = require("vscode"); + const sibling = file.replace(/\.[^.]+$/, ".writ"); + if (sibling !== file && fs.existsSync(sibling)) return sibling; + const found = await vscode.workspace.findFiles("**/*.writ", "**/_build/**", 200); + if (!found.length) { + vscode.window.showInformationMessage( + "Writ: no model to ask. A .claims or .rules file is a question about a " + + "model, and there is no .writ file in this workspace to ask it of." + ); + return null; + } + const pick = await vscode.window.showQuickPick( + found.map((u) => ({ + label: path.basename(u.fsPath), + description: vscode.workspace.asRelativePath(u), + path: u.fsPath, + })), + { title: "Which model?", placeHolder: path.basename(file) + " asks about…" } + ); + return pick ? pick.path : null; +} + +// --- the verbs ------------------------------------------------------------- + +// `writ check` on whatever is in front of you, with the questions attached. +// +// The two file types swap roles and the command must not: from a model, the +// sibling .claims is the optional extra; from a .claims, the model is the +// argument and the buffer is the extra. Asking the user which way round it goes +// would be asking them to restate something the extension can see. +async function check(uri) { + const file = await target(uri); + if (!file) return; + if (file.endsWith(".claims")) { + const model = await modelFor(file); + if (!model) return; + run(["check", model, "--claims", file]); + return; + } + if (file.endsWith(".rules")) { + // `check` has nothing to say about a .rules file; `derive` is the verb. + await derive(uri); + return; + } + const claims = file.replace(/\.writ$/, ".claims"); + run(claims !== file && fs.existsSync(claims) + ? ["check", file, "--claims", claims] + : ["check", file]); +} + +async function show(uri) { + const vscode = require("vscode"); + const file = await target(uri); + if (!file) return; + const model = file.endsWith(".writ") ? file : await modelFor(file); + if (!model) return; + const at = await vscode.window.showInputBox({ + title: "Show a situation", + prompt: + "The state index to print. Empty shows the initial situation. " + + "Several, space-separated, print several.", + placeHolder: "0", + }); + if (at === undefined) return; // escaped, as opposed to entered empty + const indices = at.trim().split(/\s+/).filter(Boolean); + run(["show", model, ...indices.flatMap((i) => ["--at", i])]); +} + +// `writ derive`, which needs three things: the model, the rules, and the +// question. Two of them are on screen whenever this is worth running. +async function derive(uri) { + const vscode = require("vscode"); + const file = await target(uri); + if (!file) return; + let rules = file; + if (!file.endsWith(".rules")) { + const found = await vscode.workspace.findFiles("**/*.rules", "**/_build/**", 200); + if (!found.length) { + vscode.window.showInformationMessage( + "Writ: no .rules file in this workspace to derive from." + ); + return; + } + const pick = await vscode.window.showQuickPick( + found.map((u) => ({ + label: path.basename(u.fsPath), + description: vscode.workspace.asRelativePath(u), + path: u.fsPath, + })), + { title: "Which rules?" } + ); + if (!pick) return; + rules = pick.path; + } + // The model, which is `file` only when `file` IS one. Reached here from a + // .claims buffer as well as a .rules one — the palette entry is on the + // language, and all three extensions are the same language — and passing a + // .claims file where the model belongs would be a parse error blamed on the + // wrong file. + const model = file.endsWith(".writ") ? file : await modelFor(file); + if (!model) return; + const question = await vscode.window.showInputBox({ + title: "Answer a relation", + prompt: + "A bare RELATION prints every row; \"(RELATION ARG…)\" keeps the matching " + + "ones, ALL-CAPS being a free variable. Prefix with `why ` for the " + + "derivation tree of one fact.", + placeHolder: "subordinate or (subordinate nabu X) or why (subordinate nabu cabinet)", + }); + if (question === undefined || !question.trim()) return; + const q = question.trim(); + const why = /^why\s+/i.test(q); + run([ + "derive", + model, + rules, + ...(why ? ["--why", q.replace(/^why\s+/i, "")] : [q]), + ]); +} + +async function compare(uri) { + const vscode = require("vscode"); + const file = await target(uri); + if (!file || !file.endsWith(".writ")) { + vscode.window.showInformationMessage( + "Writ: compare takes two models — open a .writ file first." + ); + return; + } + const found = ( + await vscode.workspace.findFiles("**/*.writ", "**/_build/**", 200) + ).filter((u) => u.fsPath !== file); + if (!found.length) { + vscode.window.showInformationMessage( + "Writ: there is no second model in this workspace to compare with." + ); + return; + } + const pick = await vscode.window.showQuickPick( + found.map((u) => ({ + label: path.basename(u.fsPath), + description: vscode.workspace.asRelativePath(u), + path: u.fsPath, + })), + { + title: "Compare with", + placeHolder: + "The NEW model. " + path.basename(file) + " is the old one, and its " + + "sibling .claims supplies the properties.", + } + ); + if (!pick) return; + run(["compare", file, pick.path]); +} + +// --- the install itself ---------------------------------------------------- + +// Build the engine, in the checkout the server came from. +// +// `make build` and not `dune build`: the Makefile is what writ's own README +// tells you to run, and it is the target that knows about the opam switch. +// +// A TASK and not a plain terminal, for one reason: the staleness verdict has to +// be cleared by a build that SUCCEEDED, and a terminal cannot say whether one +// did. `sendText` types into a shell, and the shell's own exit status is what +// closing the terminal reports — zero whether or not make failed. A task +// reports the process's code. +// +// Clearing it needs saying at all because dune is content-addressed: a build +// that changes nothing leaves the binary's mtime exactly where it was, so the +// watcher next door never fires and "older than core/…/reader.ml" would stand +// for ever after a build that did the right thing and had nothing to do. +function build() { + const vscode = require("vscode"); + const root = engine.current().checkout; + if (!root) { + vscode.window.showInformationMessage( + "Writ: nothing to build here — the server in use is an installed one, " + + "not a checkout’s. Use “Update writ” instead." + ); + return; + } + // Which folder the task belongs to, matched on a path boundary: a plain + // prefix test would put a build of `writ` under a workspace folder called + // `writ-vscode`, which is exactly the pair of names this project has. + const folder = (vscode.workspace.workspaceFolders || []).find( + (f) => root === f.uri.fsPath || root.startsWith(f.uri.fsPath + path.sep) + ); + const task = new vscode.Task( + { type: "shell", task: "writ: build the engine" }, + folder || vscode.TaskScope.Workspace, + "build the engine", + "writ", + new vscode.ShellExecution("make build", { cwd: root }) + ); + const ended = vscode.tasks.onDidEndTaskProcess((e) => { + if (e.execution.task !== task) return; + ended.dispose(); + if (e.exitCode !== 0) return; + staleness.markBuilt(); + panel.refresh(); + // The watcher restarts the server when the binary is replaced. When it was + // not — the content-addressed case above — nothing is running that is + // stale, so there is nothing else to do. + }); + vscode.tasks.executeTask(task); +} + +const PIN = "opam pin add writ git+https://github.com/writ-lang/writ.git"; + +// Update an installed writ. +// +// Re-running the pin is the update: opam re-fetches the branch and rebuilds, +// which is exactly what `opam upgrade writ` would do for a pinned package and +// works whether or not one is pinned already. Typed into a terminal rather than +// spawned, because it takes minutes, prints as it goes, and may ask a question. +function update() { + const vscode = require("vscode"); + if (engine.current().checkout) { + build(); + return; + } + const t = vscode.window.createTerminal("writ update"); + t.show(true); + t.sendText(PIN, false); // NOT executed: an install command is the user's to press enter on +} + +function register(context) { + const vscode = require("vscode"); + const on = (name, fn) => + context.subscriptions.push(vscode.commands.registerCommand(name, fn)); + + on("writ.check", check); + on("writ.show", show); + on("writ.derive", derive); + on("writ.compare", compare); + on("writ.build", build); + on("writ.update", update); + + on("writ.restartServer", async () => { + await engine.restart(); + panel.refresh(); + vscode.window.setStatusBarMessage("Writ: language server restarted", 3000); + }); + on("writ.showOutput", () => { + const client = engine.current().client; + if (client && client.outputChannel) client.outputChannel.show(true); + else + vscode.window.showInformationMessage( + "Writ: no server log — the language server never started." + ); + }); + on("writ.openSettings", () => + vscode.commands.executeCommand("workbench.action.openSettings", engine.SETTING) + ); +} + +module.exports = { register, quote, PIN }; diff --git a/src/engine.js b/src/engine.js new file mode 100644 index 0000000..bca6c12 --- /dev/null +++ b/src/engine.js @@ -0,0 +1,155 @@ +// Copyright (C) 2026 Alex Kunich +// SPDX-License-Identifier: AGPL-3.0-or-later + +// What engine this editor is talking to, and whether it is the right one. +// +// The extension and the engine are SEPARATE INSTALLS — a .vsix from one place, +// a `writ-lsp` from an opam pin or a checkout's `_build` from another — and +// nothing has ever made them agree. When they disagree the editor does not +// break; it answers, confidently, with a different writ than the one you think +// you have, and the symptom is a diagnostic `writ check` will not reproduce. +// +// This module is the one place that knows the answer, so the panel, the +// commands and the activation warning all report the same thing. + +const locate = require("./locate"); +const staleness = require("./staleness"); + +const SETTING = "writ.serverPath"; + +const state = { + serverPath: null, // the server that was resolved, or null + tried: [], // every candidate, so a failure can name them + checkout: null, // the checkout it was built in, or null if installed + cli: null, // the `writ` command line belonging to that same install + version: null, // what its `initialize` reported, or null + client: null, +}; + +function configured() { + const vscode = require("vscode"); + return vscode.workspace.getConfiguration().get(SETTING, locate.DEFAULT_SERVER); +} + +function folders() { + const vscode = require("vscode"); + return (vscode.workspace.workspaceFolders || []).map((f) => f.uri.fsPath); +} + +// Look for the server and remember what was found. Returns the state so a +// caller does not have to fetch it separately. +function resolve() { + const fs = require("fs"); + state.tried = locate.candidates(configured(), folders()); + state.serverPath = state.tried.find((p) => fs.existsSync(p)) || null; + state.checkout = state.serverPath ? locate.checkoutOf(state.serverPath) : null; + state.cli = state.serverPath ? locate.cliFor(state.serverPath) : null; + state.version = null; + staleness.forget(); + return state; +} + +function current() { + return state; +} + +// The version the server named itself with, from `initialize`. +// +// A server that reports none is not an error: it is a writ from before the LSP +// grew serverInfo. Saying so is worth a line in the panel, because "unknown" and +// "mismatched" want different things done about them and look identical if both +// are drawn as a warning. +function readVersion(client) { + const info = + client && client.initializeResult && client.initializeResult.serverInfo; + state.version = (info && info.version) || null; + return state.version; +} + +function attach(client) { + state.client = client; +} + +function stale() { + if (!state.serverPath) return null; + return staleness.stale(state.checkout, state.serverPath); +} + +// The verdict, as one fact about the install. +// +// Pure — extension version, engine version, staleness and whether there is a +// checkout, in; a level and a sentence, out — so every case can be checked +// under plain node. Null means "nothing to say", which the panel draws as the +// reassuring line rather than as no line at all: an empty status box is +// indistinguishable from a panel that failed to render. +// +// ORDER MATTERS. Staleness is asked BEFORE the versions are compared, because a +// server that is merely out of date reports the same version as a current one — +// the two agree, and the agreement is exactly the misleading part. +function verdict({ extension, engine, stale, checkout, serverPath }) { + if (!serverPath) { + return { + level: "bad", + message: + "No language server. Syntax highlighting still works — it is a grammar " + + "file — but there are no diagnostics, no outline, no hover and no " + + "completion, because all four are answered by the engine.", + action: checkout ? "build" : "install", + }; + } + if (stale) { + return { + level: "warn", + message: + "The server is older than " + + stale.path + + ". Until it is rebuilt, every answer here comes from a build that " + + "predates your change — and it reports the same version as a current " + + "one, so nothing else would tell you.", + action: "build", + }; + } + if (engine === null || engine === undefined) { + return { + level: "warn", + message: + "The server did not say which writ it is. That means a writ from " + + "before the language server reported one, so this extension cannot " + + "tell whether the two are in step. Updating writ restores the check.", + action: checkout ? "build" : "install", + }; + } + if (String(engine).trim() !== String(extension).trim()) { + return { + level: "warn", + message: + "The extension is " + + extension + + " and the engine is " + + String(engine).trim() + + ". They are released together; a mismatch means one of them was " + + "installed on its own, and a diagnostic here may not be one " + + "`writ check` would give.", + action: checkout ? "build" : "install", + }; + } + return null; +} + +// Restart the running server. Used by the command and by the watcher. +function restart() { + if (!state.client) return Promise.resolve(); + return state.client.restart().then(() => readVersion(state.client)); +} + +module.exports = { + SETTING, + resolve, + current, + readVersion, + attach, + stale, + verdict, + restart, + configured, +}; diff --git a/src/locate.js b/src/locate.js new file mode 100644 index 0000000..9a27280 --- /dev/null +++ b/src/locate.js @@ -0,0 +1,142 @@ +// Copyright (C) 2026 Alex Kunich +// SPDX-License-Identifier: AGPL-3.0-or-later + +// Where the engine is. +// +// Everything else in this extension needs an answer to that and must not have +// its own: the server the client talks to, the `writ` the commands run, and the +// checkout the build command builds all have to be the SAME install, or the +// panel reports a version from one and the diagnostics come from another. + +const fs = require("fs"); +const path = require("path"); + +// The name an installed writ puts on PATH (tooling/lsp/bin/dune's +// public_name). NOT the same as the in-checkout file name, which is +// `writ_lsp.exe` under _build. +const INSTALLED = "writ-lsp"; + +// The command line, likewise: `writ` installed, `writ.exe` under _build. +const CLI = "writ"; + +const DEFAULT_SERVER = "_build/default/tooling/lsp/bin/writ_lsp.exe"; + +// The CLI's path inside a checkout, relative to the root, and the server's. +// Kept together because the pair is what lets a resolved server name a +// checkout and a checkout name its CLI. +const IN_CHECKOUT = { + server: DEFAULT_SERVER, + cli: "_build/default/tooling/cli/writ.exe", +}; + +function onPath(exe) { + const dirs = (process.env.PATH || "").split(path.delimiter).filter(Boolean); + const names = process.platform === "win32" ? [exe + ".exe", exe] : [exe]; + return dirs.flatMap((d) => names.map((n) => path.join(d, n))); +} + +// A writ checkout, identified by the engine's own file rather than by being +// named `writ` — a checkout in a directory called something else is still one. +function isCheckout(dir) { + return fs.existsSync(path.join(dir, "dune-project")); +} + +// The checkouts one level below a workspace folder. +// +// WHY ONE LEVEL. Splitting writ and this extension into separate repositories +// means the natural thing to open is the directory that CONTAINS both, and then +// the relative default resolves against a folder that has no _build in it. The +// server is right there, one directory down, and the extension said "no language +// server" — the same symptom as not having built it, which is the wrong thing to +// go and check. One level covers that layout and stops; this must not become a +// walk of the workspace, which on a large tree would cost more than it saves. +function checkoutsBelow(dir) { + let entries; + try { + entries = fs.readdirSync(dir, { withFileTypes: true }); + } catch { + return []; // a folder that is gone or unreadable is not worth failing over + } + return entries + .filter((e) => e.isDirectory() || e.isSymbolicLink()) + .map((e) => path.join(dir, e.name)) + .filter(isCheckout); +} + +// Where to look for the server, in order. Returns every path tried, so a +// failure can name them rather than say "not found". +// +// TWO AUDIENCES, and the order is which one gets served first. A CHECKOUT of +// this repository builds its own server, and that one must win — the whole +// point of an OCaml server is that the editor and the checker are the same +// code, so a developer changing the language wants the build in front of them +// and not whatever is installed. Everyone ELSE has installed writ (by pin, or +// unpacked a release) and has no checkout at all; for them the relative default +// resolves to nothing, and `writ-lsp` on PATH is the only server there is. +// +// An ABSOLUTE setting is taken literally and nothing is guessed after it: an +// operator who names a server means that server. +// +// `folders` is passed in rather than read from `vscode` so the order can be +// checked under plain node, which is what test/resolve.test.js does. +function candidates(configured, folders) { + if (path.isAbsolute(configured)) return [configured]; + // The folder itself before anything under it: opening the checkout directly + // is the common case and must not be slowed down or second-guessed. + const inWorkspace = (folders || []).flatMap((f) => [ + path.join(f, configured), + ...checkoutsBelow(f).map((d) => path.join(d, configured)), + ]); + return [...inWorkspace, ...onPath(INSTALLED)]; +} + +// The checkout a resolved server came out of, or null for an installed one. +// +// Pure string work, deliberately: asking the filesystem "is there a +// dune-project above this?" would also say yes for `~/.opam/…/bin/writ-lsp` +// sitting inside some unrelated tree, and then the build command would offer to +// rebuild a checkout that has nothing to do with the server in use. A server is +// a checkout's only when it is at the exact path a checkout builds it to. +function checkoutOf(serverPath) { + const suffix = path.join(...IN_CHECKOUT.server.split("/")); + if (!serverPath.endsWith(suffix)) return null; + const root = serverPath.slice(0, serverPath.length - suffix.length); + const trimmed = root.replace(/[\\/]+$/, ""); + return trimmed && isCheckout(trimmed) ? trimmed : null; +} + +// The `writ` command line that belongs to a given server. +// +// It must be the SAME install, which is why this is derived from the server +// rather than looked up independently: a checkout's server with the installed +// `writ` on PATH is exactly the mismatch the panel exists to catch, and running +// commands through the wrong one would hide it. +function cliFor(serverPath) { + const root = checkoutOf(serverPath); + if (root) { + const built = path.join(root, ...IN_CHECKOUT.cli.split("/")); + if (fs.existsSync(built)) return built; + return null; // a checkout that built the server but not the CLI + } + // An installed server has the CLI beside it: opam and the release tarball + // both put `writ` and `writ-lsp` in the same bin directory. + const beside = path.join( + path.dirname(serverPath), + process.platform === "win32" ? CLI + ".exe" : CLI + ); + if (fs.existsSync(beside)) return beside; + return onPath(CLI).find((p) => fs.existsSync(p)) || null; +} + +module.exports = { + INSTALLED, + CLI, + DEFAULT_SERVER, + IN_CHECKOUT, + onPath, + isCheckout, + checkoutsBelow, + candidates, + checkoutOf, + cliFor, +}; diff --git a/src/panel.js b/src/panel.js new file mode 100644 index 0000000..b491698 --- /dev/null +++ b/src/panel.js @@ -0,0 +1,245 @@ +// Copyright (C) 2026 Alex Kunich +// SPDX-License-Identifier: AGPL-3.0-or-later + +// The Activity Bar panel. +// +// DELIBERATELY NOT THE README. VS Code already shows the readme and the version +// if you click the extension in the Extensions sidebar, so nothing here is +// information the editor lacks — this is about WHERE SOMEONE LOOKS when the +// thing they are looking at is wrong. +// +// Two things earn their place in a 250px strip. +// +// The INSTALL STATUS, because this extension bundles no engine and downloads +// none: it talks to a `writ-lsp` you already have, resolved at activation from a +// checkout's `_build` or from PATH. Every way that can go wrong produces the +// same symptom — an editor that highlights and says nothing else — and the three +// causes want three different things done about them. No server, a server older +// than the sources it was built from, and a server that is a different writ than +// this extension: the first needs an install, the second a build, the third +// either. Until now the extension said one of these once, in a toast, at +// activation, and then never again. +// +// And the VERBS, because writ is a command-line tool that answers questions and +// the extension exposed none of them. `check` on the file in front of you is +// two clicks from here rather than a remembered invocation with two paths in it. +// +// The file-type table is three lines and stays because the split — models here, +// questions there, derivations somewhere else — is the first thing about this +// language a person has to hold in their head, and the panel is already open. + +const engine = require("./engine"); + +const GUIDE = "https://github.com/writ-lang/writ-vscode#readme"; +const LANGUAGE = "https://github.com/writ-lang/writ#readme"; + +const FILE_TYPES = [ + [".writ", "models and libraries — schema, instance, transitions"], + [".claims", "the questions asked of a model, kept as their own document"], + [".rules", "Datalog-style derivations over a model's situation space"], +]; + +function escapeHtml(s) { + return String(s).replace( + /[&<>"']/g, + (c) => + ({ + "&": "&", + "<": "<", + ">": ">", + '"': """, + "'": "'", + })[c] + ); +} + +// The action button under the status line, if the verdict asks for one. +// Named here rather than in [engine.verdict] so that the verdict stays a +// statement about the install and not a piece of user interface. +function actionButton(action, checkout) { + if (action === "build") + return ''; + if (action === "install") + return ( + '" + ); + return ""; +} + +// Pure, so the whole panel can be rendered and inspected under plain node — +// which test/panel.test.js does, because a webview is otherwise only checkable +// by looking at it. +function renderHtml({ extension, engineVersion, serverPath, checkout, stale }) { + const v = engine.verdict({ + extension, + engine: engineVersion, + stale, + checkout, + serverPath, + }); + const status = v + ? escapeHtml(v.message) + : "The extension and the engine are in step."; + const cls = v ? v.level : "ok"; + const shownEngine = + engineVersion === null || engineVersion === undefined + ? serverPath + ? "not reported" + : "not found" + : escapeHtml(String(engineVersion).trim()); + + const types = FILE_TYPES.map( + ([ext, what]) => + '' + + escapeHtml(ext) + + "" + + escapeHtml(what) + + "" + ).join("\n"); + + return ` + + + + +

Ask something

+ + + + + +

Three kinds of file

+ ${types}
+ +

The engine

+
+
Extension
${escapeHtml(extension)}
+
Engine
${shownEngine}
+
+
${escapeHtml(serverPath || "no language server")}
+

${status}

+ ${v ? actionButton(v.action, checkout) : ""} + + + + +

Help

+ + + + +`; +} + +// The view, once it exists, so that anything which changes what the panel says +// can ask it to say it again. Rendering once and never again would be a bug of +// its own: you build the engine, the warning stays, and the panel is the only +// thing left in the editor still claiming you are out of date. +let live = null; + +function refresh() { + if (live) live(); +} + +function register(context) { + const vscode = require("vscode"); + + const provider = { + resolveWebviewView(view) { + view.webview.options = { enableScripts: true }; + const mine = + (context.extension && + context.extension.packageJSON && + context.extension.packageJSON.version) || + "0.0.0"; + + const paint = () => { + const s = engine.current(); + view.webview.html = renderHtml({ + extension: mine, + engineVersion: s.version, + serverPath: s.serverPath, + checkout: s.checkout, + stale: engine.stale(), + }); + }; + live = paint; + paint(); + + view.onDidChangeVisibility(() => { + if (view.visible) paint(); + }); + view.onDidDispose(() => { + if (live === paint) live = null; + }); + + view.webview.onDidReceiveMessage((m) => { + if (m.command) vscode.commands.executeCommand(m.command); + else if (m.open) vscode.env.openExternal(vscode.Uri.parse(m.open)); + }); + }, + }; + + context.subscriptions.push( + vscode.window.registerWebviewViewProvider("writ.home", provider), + + // A Command Palette route to the panel, because the Activity Bar entry can + // be invisible through no fault of the manifest: VS Code stores per-user + // workbench state in workbench.activity.pinnedViewlets2, and on a crowded + // bar a newly contributed container can land there pinned but not visible — + // registered, ordered, and never drawn. "Click the icon" is then a dead end + // with nothing to search for. VS Code generates .focus for a + // contributed view; this wraps it under a name a person can find by typing + // "writ". + vscode.commands.registerCommand("writ.openOverview", () => + vscode.commands.executeCommand("writ.home.focus") + ) + ); +} + +module.exports = { register, refresh, renderHtml, escapeHtml, FILE_TYPES }; diff --git a/src/staleness.js b/src/staleness.js new file mode 100644 index 0000000..cfb4a08 --- /dev/null +++ b/src/staleness.js @@ -0,0 +1,123 @@ +// Copyright (C) 2026 Alex Kunich +// SPDX-License-Identifier: AGPL-3.0-or-later + +// Is the built server older than the language it was built from? +// +// The version comparison in the panel cannot answer this. dune-project's +// version moves only when someone bumps it deliberately, so a checkout built +// before this morning's edit reports exactly the same version as one built +// after it — the two agree, the panel says so, and the editor goes on answering +// with a server that predates the change being made. +// +// The watcher next door handles the other half: a server that is rebuilt WHILE +// the editor runs. This is the half it cannot see, because nothing happened — +// the build was never run at all. +// +// Times catch what versions cannot. + +const fs = require("fs"); +const path = require("path"); + +// Only the engine and the tools built from it. Not tests/ (a changed test does +// not make the server wrong) and not core/stdlib (.writ files, read at runtime +// from disk, never compiled in). +const SOURCE_DIRS = ["core", "tooling"]; +const SOURCE_EXT = [".ml", ".mli"]; + +// Pure, so it can be checked without a filesystem. +// +// [builtAt] is when a build last finished, and it matters because dune is +// content-addressed: touch a file without changing it and dune rebuilds +// nothing, so the binary keeps an mtime older than the source for ever. A +// completed build means the binary reflects the sources whether or not any +// bytes moved, and without this the warning could never be cleared by doing the +// thing the warning asks for. +function staleness(binaryMtime, sources, builtAt) { + if (binaryMtime === null || binaryMtime === undefined) return null; + const floor = Math.max(binaryMtime, builtAt || 0); + let newest = null; + for (const source of sources) { + if (source.mtime > floor && (!newest || source.mtime > newest.mtime)) + newest = source; + } + return newest + ? { path: newest.path, mtime: newest.mtime, binary: binaryMtime } + : null; +} + +// The engine's sources under a checkout. Recursive, because writ's are nested +// (tooling/lsp/lib/feature/…) where a flat listing would see none of them — +// and bounded to SOURCE_DIRS, which are 61 files, so this is a walk of the +// engine and never of the workspace. +function sourcesIn(root) { + const out = []; + const walk = (dir, shown) => { + let entries; + try { + entries = fs.readdirSync(dir, { withFileTypes: true }); + } catch { + return; + } + for (const e of entries) { + const full = path.join(dir, e.name); + const label = shown + "/" + e.name; + if (e.isDirectory()) { + if (e.name === "_build" || e.name === ".git") continue; + walk(full, label); + } else if (SOURCE_EXT.includes(path.extname(e.name))) { + try { + out.push({ path: label, mtime: fs.statSync(full).mtimeMs }); + } catch { + // it went away between the listing and the stat + } + } + } + }; + for (const dir of SOURCE_DIRS) walk(path.join(root, dir), dir); + return out; +} + +// Said by whoever ran the build, when it succeeded. +let builtAt = 0; +let lastLook = 0; +let lastAnswer = null; + +function markBuilt(when) { + builtAt = when === undefined ? Date.now() : when; + lastLook = 0; + lastAnswer = null; +} + +function forget() { + lastLook = 0; + lastAnswer = null; +} + +// Cached for a second: the panel repaints on every visibility change, and a +// 61-file walk on each one would be paid for nothing. +// +// Returns null for an INSTALLED server as well as for an up-to-date one. That +// is not a gap: there are no sources to be older than, and "your opam pin is +// behind the repository" is a different question with a different answer, which +// is the update command and not a rebuild. +function stale(checkout, serverPath, now) { + const t = now === undefined ? Date.now() : now; + if (now === undefined && t - lastLook < 1000) return lastAnswer; + const answer = (() => { + if (!checkout) return null; + let binaryMtime; + try { + binaryMtime = fs.statSync(serverPath).mtimeMs; + } catch { + return null; // no server at all is a different complaint + } + return staleness(binaryMtime, sourcesIn(checkout), builtAt); + })(); + if (now === undefined) { + lastLook = t; + lastAnswer = answer; + } + return answer; +} + +module.exports = { staleness, sourcesIn, stale, markBuilt, forget, SOURCE_DIRS }; diff --git a/src/watcher.js b/src/watcher.js new file mode 100644 index 0000000..dd6245d --- /dev/null +++ b/src/watcher.js @@ -0,0 +1,74 @@ +// Copyright (C) 2026 Alex Kunich +// SPDX-License-Identifier: AGPL-3.0-or-later + +// Restart the server when its binary is replaced. +// +// WHY THIS EXISTS. `make build` writes a NEW inode over the server, and the +// process already running keeps the old one — `/proc/PID/exe` reads +// "(deleted)". Nothing surfaces that. The editor keeps answering, confidently, +// with a language that is one build out of date, and the symptom is a squiggle +// on code the CLI accepts. That has cost real debugging time more than once, +// and it is worst exactly when the language itself is being changed, because +// then the stale answer is *plausible*. +// +// Polling rather than [createFileSystemWatcher]: the default server path is +// under `_build`, which is routinely listed in `files.watcherExclude`, and a +// watcher that silently never fires would be a worse version of this same bug. +// One stat every two seconds is not a cost worth optimising. + +const fs = require("fs"); + +const POLL_MS = 2000; + +// Identity of the file as built, not merely its name: dune replaces the +// executable, so the inode changes even when a rebuild lands within the same +// mtime granularity. +function stampOf(p) { + try { + const s = fs.statSync(p); + return `${s.ino}:${s.mtimeMs}:${s.size}`; + } catch { + return null; + } +} + +// `restart` and `onRestart` are injected rather than reached for, so this can +// be driven against a real file with no editor — which test/watcher.test.js +// does, because a watcher that silently never fires is the bug it exists to +// fix and nothing else would catch it. +function watchServerBinary(serverPath, log, pollMs = POLL_MS, hooks = {}) { + const restart = hooks.restart || (() => Promise.resolve()); + const onRestart = hooks.onRestart || (() => {}); + const onFailure = hooks.onFailure || (() => {}); + let known = stampOf(serverPath); + let pending = null; + + const id = setInterval(async () => { + const now = stampOf(serverPath); + if (now === null) return; // mid-build: the file is briefly gone + if (now === known) { + pending = null; // nothing new, or a change that reverted + return; + } + if (pending !== now) { + // Seen a change, but act only once it has stopped moving, so a + // multi-second link step restarts the server once and not four times. + pending = now; + return; + } + known = now; + pending = null; + log(`server binary changed on disk — restarting (${serverPath})`); + try { + await restart(); + log("server restarted; diagnostics are from the current build"); + onRestart(); + } catch (e) { + onFailure(e); + } + }, pollMs); + + return { dispose: () => clearInterval(id) }; +} + +module.exports = { watchServerBinary, stampOf, POLL_MS }; diff --git a/syntaxes/writ.tmLanguage.json b/syntaxes/writ.tmLanguage.json index 542ef80..638d08f 100644 --- a/syntaxes/writ.tmLanguage.json +++ b/syntaxes/writ.tmLanguage.json @@ -73,12 +73,12 @@ "match": "(?<=\\()(arrow|to|fixed|vacatable|when|do|vacant)(?![-\\w])" }, "guard": { - "comment": "Guard connectives and leaf predicates (core/syntax/grammar.ml, guard): and/or/not/is/defined/some. This alternation is what .afk-flow/check-grammar.py asserts against the engine; keep the six as whole ( | ) alternatives. Head position only.", + "comment": "Guard connectives and leaf predicates (core/syntax/grammar.ml, guard): and/or/not/is/defined/some. These six are `guard_words` in core/syntax/rules_parser.ml; a word added there must be added here, or the editor silently paints it as a user relation. Kept as whole ( | ) alternatives so the set can be diffed against that list by eye. Head position only.", "name": "support.function.guard.writ", "match": "(?<=\\()(and|or|not|is|defined|some)(?![-\\w])" }, "effect": { - "comment": "Effect heads (core/syntax/grammar.ml, effect): set/vacate/gap. Also asserted by check-grammar.py as whole ( | ) alternatives. Head position only.", + "comment": "Effect heads (core/syntax/grammar.ml, effect): set/vacate/gap. Kept as whole ( | ) alternatives for the same reason as the guard set above. Head position only.", "name": "keyword.other.effect.writ", "match": "(?<=\\()(set|vacate|gap)(?![-\\w])" }, @@ -103,7 +103,7 @@ "match": "(?<=\\()=(?=\\s)" }, "rules-builtin": { - "comment": "The extension's seven BUILT-IN relations (core/syntax/rules_parser.ml, `builtins`): situation/init/edge/gap-edge/phase/phase-step/holds. Their arities and sorts are fixed, so a literal headed by one of these is never a user relation \u2014 which is exactly why they read as vocabulary and not as a name. Head position only. Kept as whole ( | ) alternatives for .afk-flow/check-grammar.py.", + "comment": "The extension's seven BUILT-IN relations (core/syntax/rules_parser.ml, `builtins`): situation/init/edge/gap-edge/phase/phase-step/holds. Their arities and sorts are fixed, so a literal headed by one of these is never a user relation \u2014 which is exactly why they read as vocabulary and not as a name. Head position only. Kept as whole ( | ) alternatives so they can be diffed against `builtins` by eye.", "name": "support.function.rules-builtin.writ", "match": "(?<=\\()(situation|init|edge|gap-edge|phase-step|phase|holds)(?![-\\w])" }, diff --git a/test-resolve.js b/test-resolve.js deleted file mode 100644 index fd4ab2b..0000000 --- a/test-resolve.js +++ /dev/null @@ -1,97 +0,0 @@ -// Copyright (C) 2026 Alex Kunich -// SPDX-License-Identifier: AGPL-3.0-or-later - -// Where the client looks for the language server, and in what order. -// -// This is the whole of "the extension works with writ installed separately". -// Until it was written, the only candidate was a path under `_build`, which -// exists ONLY inside a checkout — so on a machine that had installed writ -// separately the extension found nothing, even though tooling/lsp/bin/dune installs -// `writ-lsp` precisely so that case works. -// -// The order matters as much as the set: a checkout's own build must win, because -// an OCaml server exists so the editor and the checker are the same code, and -// someone changing the language wants the build in front of them. -// -// Run: node tooling/vscode/test-resolve.js - -const Module = require("module"); -const path = require("path"); - -let workspace = []; -const origLoad = Module._load; -Module._load = function (req) { - if (req === "vscode") - return { - workspace: { - get workspaceFolders() { - return workspace; - }, - getConfiguration: () => ({ get: (_k, d) => d }), - }, - window: { showErrorMessage: () => {} }, - }; - if (req === "vscode-languageclient/node") - return { LanguageClient: class {}, TransportKind: { stdio: 0 } }; - return origLoad.apply(this, arguments); -}; - -const { candidates, onPath, INSTALLED } = require( - path.join(__dirname, "extension.js") -).__test; - -let failed = 0; -function check(name, cond) { - if (!cond) { - console.log(`FAIL: ${name}`); - failed++; - } -} - -const DEFAULT = "_build/default/tooling/lsp/bin/writ_lsp.exe"; -const folder = (p) => ({ uri: { fsPath: p } }); - -// 1. In a checkout: the build comes first, the installed server after it. -workspace = [folder("/w/writ")]; -let c = candidates(DEFAULT); -check("a checkout's own build is tried first", c[0] === path.join("/w/writ", DEFAULT)); -check("and the installed writ-lsp is still a fallback", c.some((p) => p.endsWith(path.sep + INSTALLED))); -check( - "the build is tried BEFORE anything on PATH", - c.indexOf(path.join("/w/writ", DEFAULT)) < - c.findIndex((p) => p.endsWith(path.sep + INSTALLED)) -); - -// 2. No workspace at all — a lone .writ file, or writ installed without a -// checkout. This is the case that used to yield an empty list. -workspace = []; -c = candidates(DEFAULT); -check("with no workspace there is still somewhere to look", c.length > 0); -check( - "and it is writ-lsp on PATH", - c.every((p) => p.endsWith(path.sep + INSTALLED)) -); - -// 3. An absolute setting is taken literally: an operator naming a server means -// that server, and nothing is guessed after it. -workspace = [folder("/w/writ")]; -c = candidates("/opt/writ/bin/writ-lsp"); -check("an absolute setting is the only candidate", c.length === 1); -check("and it is exactly what was set", c[0] === "/opt/writ/bin/writ-lsp"); - -// 4. The PATH search uses the INSTALLED name, not the in-checkout file name. -// an installed writ produces `writ-lsp`; `_build` produces `writ_lsp.exe`. -check("the installed name is writ-lsp", INSTALLED === "writ-lsp"); -check( - "every PATH candidate ends in it", - onPath(INSTALLED).every((p) => path.basename(p).startsWith(INSTALLED)) -); -check("PATH is actually searched", onPath(INSTALLED).length > 0); - -const n = 10 - failed; -console.log( - failed === 0 - ? `extension resolve tests: ${n} checks passed` - : `extension resolve tests: ${failed} FAILED` -); -process.exit(failed === 0 ? 0 : 1); diff --git a/test-watcher.js b/test-watcher.js deleted file mode 100644 index 3acffdc..0000000 --- a/test-watcher.js +++ /dev/null @@ -1,94 +0,0 @@ -// Copyright (C) 2026 Alex Kunich -// SPDX-License-Identifier: AGPL-3.0-or-later - -// Drives extension.js's server-binary watcher against a real file on disk. -// -// The watcher is the only part of the client with behaviour of its own, and its -// failure mode is SILENCE — it either fires or it does not, and a watcher that -// never fires looks exactly like a server that is simply up to date. That is -// the bug it exists to fix, so it does not get to go untested. The first -// version of it never fired at all; this file is what caught that. -// -// `vscode` and `vscode-languageclient` do not exist outside the editor, so both -// are stubbed at the module loader. Nothing here needs the real ones: the -// watcher only stats a path and calls `client.restart()`. -// -// Run: node tooling/vscode/test-watcher.js - -const Module = require("module"); -const fs = require("fs"); -const path = require("path"); -const os = require("os"); - -const errors = []; -const origLoad = Module._load; -Module._load = function (req) { - if (req === "vscode") - return { - workspace: { - workspaceFolders: [], - getConfiguration: () => ({ get: (_k, d) => d }), - }, - window: { showErrorMessage: (m) => errors.push(m) }, - }; - if (req === "vscode-languageclient/node") - return { LanguageClient: class {}, TransportKind: { stdio: 0 } }; - return origLoad.apply(this, arguments); -}; - -const ext = require(path.join(__dirname, "extension.js")); - -const POLL = 40; // fast enough to gate; the shipped default is 2000 -const sleep = (ms) => new Promise((r) => setTimeout(r, ms)); - -let failed = 0; -function check(name, cond) { - if (!cond) { - console.log(`FAIL: ${name}`); - failed++; - } -} - -(async () => { - const dir = fs.mkdtempSync(path.join(os.tmpdir(), "writ-watch-")); - const bin = path.join(dir, "writ_lsp.exe"); - fs.writeFileSync(bin, "v1"); - - let restarts = 0; - const logs = []; - ext.__test.setClient({ - restart: async () => { - restarts++; - }, - }); - const w = ext.__test.watchServerBinary(bin, (m) => logs.push(m), POLL); - - await sleep(POLL * 6); - check("an unchanged binary does not restart the server", restarts === 0); - - // Replaced, not edited in place — which is what dune does, and why the stamp - // carries the inode and not just the mtime. - fs.rmSync(bin); - fs.writeFileSync(bin, "v2-different-length"); - await sleep(POLL * 8); - check("a replaced binary restarts the server", restarts === 1); - check("and says so in the output channel", logs.length === 2); - - await sleep(POLL * 6); - check("a settled binary restarts it once, not repeatedly", restarts === 1); - - // A vanished file is a build in progress, not a reason to do anything. - fs.rmSync(bin); - await sleep(POLL * 6); - check("a missing binary is not a restart", restarts === 1); - check("nothing was reported to the user", errors.length === 0); - - w.dispose(); - const n = 6 - failed; - console.log( - failed === 0 - ? `extension watcher tests: ${n} checks passed` - : `extension watcher tests: ${failed} FAILED` - ); - process.exit(failed === 0 ? 0 : 1); -})(); diff --git a/test/engine.test.js b/test/engine.test.js new file mode 100644 index 0000000..d8a699e --- /dev/null +++ b/test/engine.test.js @@ -0,0 +1,229 @@ +// Copyright (C) 2026 Alex Kunich +// SPDX-License-Identifier: AGPL-3.0-or-later + +// The extension against a REAL engine: what it asks of `writ-lsp`, and the +// command lines it hands to `writ`. +// +// The other test files check this repository's JavaScript, and nothing in them +// would notice the engine changing underneath it. That coupling is the one most +// likely to break silently: a capability the server stops advertising, or a +// flag the CLI renames, leaves the extension running and doing nothing. The +// verbs are the worst case, because they are typed into a terminal and nobody +// reads the usage error that comes back. +// +// So this spawns the server the extension would find, speaks LSP to it over +// vscode-jsonrpc (already installed, as vscode-languageclient's transport), +// and runs each command-line SHAPE src/commands.js builds. A new verb or flag +// there belongs here too. +// +// No engine, no test: with no `writ-lsp`, or no node_modules to speak LSP +// with, it prints a skip and passes, so this stays as installable as the rest. Set WRIT_E2E_REQUIRED=1 to make a missing +// engine a failure, which is what writ's downstream image does. WRIT_LSP names +// a server explicitly. +// +// Run: node test/engine.test.js + +const fs = require("fs"); +const os = require("os"); +const path = require("path"); +const { spawn, spawnSync } = require("child_process"); +const { suite } = require("./harness"); +const locate = require("../src/locate"); + +const { check, done } = suite("engine tests"); + +// Found the way the extension finds an installed one, and its CLI derived from +// it the way the extension derives it — beside the server, not off PATH. +function skip(why) { + if (process.env.WRIT_E2E_REQUIRED === "1") { + console.log(`FAIL: ${why}, and WRIT_E2E_REQUIRED=1`); + process.exit(1); + } + console.log(`engine tests: SKIP — ${why}`); + process.exit(0); +} + +const server = + process.env.WRIT_LSP || + locate.onPath(locate.INSTALLED).find((p) => fs.existsSync(p)); +if (!server) skip("no writ-lsp on PATH (set WRIT_LSP=)"); + +// Required here rather than at the top: the other test files need nothing +// installed, and a checkout without `npm ci` should skip this, not crash. +let rpc; +try { + rpc = require("vscode-jsonrpc/node"); +} catch { + skip("vscode-jsonrpc is not installed (run npm ci)"); +} +const cli = locate.cliFor(server); + +// A model small enough to read, using the stdlib so the load path is exercised +// from a directory that is not the install prefix. +const MODEL = [ + '(load "stdlib.writ")', + "(schema s (type v (lo hi)) (type box (arrow f (to v))))", + "(instance i s (box b (f lo)))", + "(use s)", + "(initial i)", + "(transition raise (when (is b.f lo)) (do (set b.f hi)))", + "", +].join("\n"); +const CLAIMS = '(property raised "b can go high" (possible (is b.f hi)))\n'; +const RULES = '(load "ct.rules")\n'; +// An unbalanced form: whatever else changes, the reader must reject it. +const BROKEN = "(schema s (type v (lo hi))\n"; + +const dir = fs.mkdtempSync(path.join(os.tmpdir(), "writ-e2e-")); +const file = (name, text) => { + const p = path.join(dir, name); + fs.writeFileSync(p, text); + return p; +}; +const model = file("m.writ", MODEL); +const claims = file("m.claims", CLAIMS); +const rules = file("m.rules", RULES); +const other = file("other.writ", MODEL); +const broken = file("broken.writ", BROKEN); +const uri = (p) => "file://" + p; + +// ── the command lines ──────────────────────────────────────────────────────── +// Exit 0 and 1 are verdicts (1 means "has findings"); 2 is how the CLI says it +// could not run the command at all, which for these inputs means the shape the +// extension builds is no longer one the CLI accepts. +function cliChecks() { + check("a `writ` CLI is found beside the server", !!cli); + if (!cli) return; + const shapes = [ + ["check", model], + ["check", model, "--claims", claims], + ["show", model, "--at", "0"], + ["show", model, "--at", "0", "--at", "1"], + ["derive", model, rules, "reach"], + ["derive", model, rules, "(reach X Y)"], + ["derive", model, rules, "--why", "(reach 0 1)"], + ["compare", model, other], + ]; + for (const args of shapes) { + const r = spawnSync(cli, args, { cwd: dir, encoding: "utf8" }); + const ok = r.status === 0 || r.status === 1; + if (!ok) console.log(` writ ${args.join(" ")}\n ${r.stderr.trim()}`); + const shown = args.map((a) => (a.startsWith(dir) ? path.basename(a) : a)); + check(`writ ${shown.join(" ")} is accepted`, ok); + } +} + +// ── the language server ───────────────────────────────────────────────────── +async function lspChecks() { + const proc = spawn(server, [], { stdio: ["pipe", "pipe", "inherit"] }); + const conn = rpc.createMessageConnection( + new rpc.StreamMessageReader(proc.stdout), + new rpc.StreamMessageWriter(proc.stdin) + ); + const diagnostics = new Map(); + const waiting = new Map(); + conn.onNotification("textDocument/publishDiagnostics", (p) => { + diagnostics.set(p.uri, p.diagnostics); + const w = waiting.get(p.uri); + if (w) w(p.diagnostics); + }); + conn.listen(); + const diagnosticsFor = (u) => + diagnostics.has(u) + ? Promise.resolve(diagnostics.get(u)) + : new Promise((resolve) => { + waiting.set(u, resolve); + setTimeout(() => resolve(null), 10000); + }); + const open = (p) => + conn.sendNotification("textDocument/didOpen", { + textDocument: { + uri: uri(p), + languageId: "writ", + version: 1, + text: fs.readFileSync(p, "utf8"), + }, + }); + + const init = await conn.sendRequest("initialize", { + processId: process.pid, + rootUri: uri(dir), + capabilities: {}, + }); + conn.sendNotification("initialized", {}); + const caps = init.capabilities || {}; + const info = init.serverInfo || {}; + check("initialize names the server", !!info.name); + // engine.js shows this version in the panel and compares it with the + // extension's; a server that stops sending it reads as "unknown engine". + check("initialize reports a version", !!info.version); + check("full-document sync, which is what the client sends", caps.textDocumentSync === 1); + check("hover is advertised", caps.hoverProvider === true); + check("the outline is advertised", caps.documentSymbolProvider === true); + check("completion is advertised", !!caps.completionProvider); + + open(model); + const clean = await diagnosticsFor(uri(model)); + check("a good model gets diagnostics published", Array.isArray(clean)); + check( + "and none of them is an error", + Array.isArray(clean) && !clean.some((d) => d.severity === 1) + ); + + open(broken); + const bad = await diagnosticsFor(uri(broken)); + check( + "a broken model gets an error, with a range to underline", + Array.isArray(bad) && + bad.some((d) => d.severity === 1 && d.range && d.range.start) + ); + + const symbols = await conn.sendRequest("textDocument/documentSymbol", { + textDocument: { uri: uri(model) }, + }); + check("the outline is not empty", Array.isArray(symbols) && symbols.length > 0); + check( + "and it names the transition", + JSON.stringify(symbols || []).includes("raise") + ); + + // On the `initial` keyword: the server documents the language's forms, and + // completion offers names at the same place. + const at = { line: 4, character: 2 }; + const hover = await conn.sendRequest("textDocument/hover", { + textDocument: { uri: uri(model) }, + position: at, + }); + check( + "hover documents a form", + JSON.stringify((hover && hover.contents) || "").includes("initial") + ); + const completion = await conn.sendRequest("textDocument/completion", { + textDocument: { uri: uri(model) }, + position: at, + }); + const items = Array.isArray(completion) ? completion : (completion || {}).items; + check("completion offers something", Array.isArray(items) && items.length > 0); + + await conn.sendRequest("shutdown"); + conn.sendNotification("exit"); + const exited = await new Promise((resolve) => { + proc.on("exit", () => resolve(true)); + setTimeout(() => resolve(false), 5000); + }); + check("shutdown then exit stops the server", exited); + if (!exited) proc.kill(); + conn.dispose(); +} + +(async () => { + console.log(`engine tests: ${server}`); + cliChecks(); + try { + await lspChecks(); + } catch (e) { + check(`the LSP session completes (${e.message})`, false); + } + fs.rmSync(dir, { recursive: true, force: true }); + done(); +})(); diff --git a/test/harness.js b/test/harness.js new file mode 100644 index 0000000..334e9f6 --- /dev/null +++ b/test/harness.js @@ -0,0 +1,33 @@ +// Copyright (C) 2026 Alex Kunich +// SPDX-License-Identifier: AGPL-3.0-or-later + +// What the test files share: counting, and a name for a failure. +// +// Deliberately not a framework. Each file is `node test/NAME.test.js` and +// nothing has to be installed to run one — which matters because this +// repository's only dependency is vscode-languageclient, and a test runner +// would be the second. + +function suite(label) { + let failed = 0; + let passed = 0; + return { + check(name, cond) { + if (cond) passed++; + else { + console.log(`FAIL: ${name}`); + failed++; + } + }, + done() { + console.log( + failed === 0 + ? `${label}: ${passed} checks passed` + : `${label}: ${failed} FAILED of ${failed + passed}` + ); + process.exit(failed === 0 ? 0 : 1); + }, + }; +} + +module.exports = { suite }; diff --git a/test/manifest.test.js b/test/manifest.test.js new file mode 100644 index 0000000..24877ed --- /dev/null +++ b/test/manifest.test.js @@ -0,0 +1,129 @@ +// Copyright (C) 2026 Alex Kunich +// SPDX-License-Identifier: AGPL-3.0-or-later + +// The manifest against the code. +// +// package.json is the half of an extension that nothing typechecks. A command +// contributed but never registered shows up in the palette and does nothing +// when picked; a command registered but not contributed is unreachable except +// from a button; a menu or a webview button naming a command that is neither is +// a click that silently fails. All three are invisible until someone tries the +// one path that hits them, and none of them is a crash — which is why they get +// a test rather than a review. +// +// The panel in particular is HTML in a string: the buttons carry command ids +// that no tool anywhere resolves. +// +// Run: node test/manifest.test.js + +const fs = require("fs"); +const path = require("path"); +const { suite } = require("./harness"); + +const { check, done } = suite("manifest tests"); + +const root = path.join(__dirname, ".."); +const pkg = JSON.parse(fs.readFileSync(path.join(root, "package.json"), "utf8")); +const c = pkg.contributes; +const read = (p) => fs.readFileSync(path.join(root, p), "utf8"); + +// Every `writ.…` id the source registers, wherever it registers it. +const source = ["src/commands.js", "src/panel.js"].map(read).join("\n"); +const registered = new Set( + [...source.matchAll(/(?:registerCommand\(|\bon\()\s*"(writ\.[\w.]+)"/g)].map((m) => m[1]) +); + +const contributed = new Set(c.commands.map((x) => x.command)); + +// --- contributed against registered ---------------------------------------- + +for (const id of contributed) + check(`${id} is contributed and registered`, registered.has(id)); + +// The reverse is not an error in general — a command can exist for a button +// alone — but it is worth knowing about, because an id that is registered and +// contributed nowhere is one nobody can reach from the palette either. +for (const id of registered) + check(`${id} is registered and contributed`, contributed.has(id)); + +// --- everything that NAMES a command --------------------------------------- + +const referenced = new Set(); +for (const group of Object.values(c.menus || {})) + for (const item of group) referenced.add(item.command); +for (const b of c.keybindings || []) referenced.add(b.command); +// The panel's buttons, which are command ids inside an HTML string. +for (const m of read("src/panel.js").matchAll(/(?:data-cmd="|command: ')(writ\.[\w.]+)/g)) + referenced.add(m[1]); +// And the ones the activation error offers. +for (const m of read("extension.js").matchAll(/executeCommand\("(writ\.[\w.]+)"/g)) + referenced.add(m[1]); + +for (const id of referenced) + check(`${id}, named in a menu or a button, exists`, registered.has(id)); + +check("the panel does name commands, so the check above is not vacuous", referenced.size > 5); + +// --- the activity bar ------------------------------------------------------ + +const container = c.viewsContainers.activitybar[0]; +check("there is an activity bar container", !!container); +check("its views are keyed by its id", Array.isArray(c.views[container.id])); + +const view = c.views[container.id][0]; +check("the view is a webview, which is what the panel renders", view.type === "webview"); +check( + "and the extension activates when it is opened — otherwise the panel that " + + "explains a missing server would itself need a .writ file open to appear", + (pkg.activationEvents || []).includes("onView:" + view.id) +); +check( + "the panel registers a provider for exactly that id", + read("src/panel.js").includes('registerWebviewViewProvider("' + view.id + '"') +); +check( + "and the palette route focuses that same view — the activity bar icon can " + + "be unpinned, and then it is the only way in", + read("src/panel.js").includes('executeCommand("' + view.id + '.focus")') +); + +// --- files the manifest promises ------------------------------------------- + +const icons = [ + container.icon, + ...Object.values((c.languages[0] || {}).icon || {}), + pkg.icon, +].filter(Boolean); +for (const i of icons) + check(`${i} exists`, fs.existsSync(path.join(root, i.replace(/^\.\//, "")))); +check("the language icons are declared for both themes", icons.length >= 4); + +check( + "the grammar file exists", + fs.existsSync(path.join(root, c.grammars[0].path.replace(/^\.\//, ""))) +); +check("main points at a real file", fs.existsSync(path.join(root, pkg.main.replace(/^\.\//, "")))); + +// --- the setting the code actually reads ----------------------------------- + +const setting = Object.keys(c.configuration.properties)[0]; +check( + "the contributed setting is the one src/engine.js reads", + read("src/engine.js").includes('SETTING = "' + setting + '"') +); +check( + "and its default is the path src/locate.js defaults to", + c.configuration.properties[setting].default === + read("src/locate.js").match(/DEFAULT_SERVER = "([^"]+)"/)[1] +); + +// --- version ----------------------------------------------------------------- +// +// Cheap here, and the README is the copy that gets forgotten. scripts/version.sh +// is the thing that fixes it; this is the thing that notices. +check( + "the README's .vsix filename carries the manifest's version", + read("README.md").includes("writ-" + pkg.version + ".vsix") +); + +done(); diff --git a/test/resolve.test.js b/test/resolve.test.js new file mode 100644 index 0000000..daeca38 --- /dev/null +++ b/test/resolve.test.js @@ -0,0 +1,151 @@ +// Copyright (C) 2026 Alex Kunich +// SPDX-License-Identifier: AGPL-3.0-or-later + +// Where the client looks for the engine, and in what order. +// +// This is the whole of "the extension works with writ installed separately". +// Until it was written, the only candidate was a path under `_build`, which +// exists ONLY inside a checkout — so on a machine that had installed writ +// separately the extension found nothing, even though tooling/lsp/bin/dune +// installs `writ-lsp` precisely so that case works. +// +// The order matters as much as the set: a checkout's own build must win, +// because an OCaml server exists so the editor and the checker are the same +// code, and someone changing the language wants the build in front of them. +// +// Nothing is stubbed here any more. [candidates] takes its workspace folders as +// an argument rather than reaching into `vscode`, which is what makes the +// module plain node — and the reason the resolution order is the one part of +// this extension that has never needed an editor to check. +// +// Run: node test/resolve.test.js + +const fs = require("fs"); +const os = require("os"); +const path = require("path"); +const { suite } = require("./harness"); +const locate = require("../src/locate"); + +const { check, done } = suite("resolve tests"); +const { candidates, onPath, checkoutOf, cliFor, INSTALLED, DEFAULT_SERVER: DEFAULT } = locate; + +// 1. In a checkout: the build comes first, the installed server after it. +let c = candidates(DEFAULT, ["/w/writ"]); +check("a checkout's own build is tried first", c[0] === path.join("/w/writ", DEFAULT)); +check( + "and the installed writ-lsp is still a fallback", + c.some((p) => p.endsWith(path.sep + INSTALLED)) +); +check( + "the build is tried BEFORE anything on PATH", + c.indexOf(path.join("/w/writ", DEFAULT)) < + c.findIndex((p) => p.endsWith(path.sep + INSTALLED)) +); + +// 2. No workspace at all — a lone .writ file, or writ installed without a +// checkout. This is the case that used to yield an empty list. +c = candidates(DEFAULT, []); +check("with no workspace there is still somewhere to look", c.length > 0); +check("and it is writ-lsp on PATH", c.every((p) => p.endsWith(path.sep + INSTALLED))); + +// 3. An absolute setting is taken literally: an operator naming a server means +// that server, and nothing is guessed after it. +c = candidates("/opt/writ/bin/writ-lsp", ["/w/writ"]); +check("an absolute setting is the only candidate", c.length === 1); +check("and it is exactly what was set", c[0] === "/opt/writ/bin/writ-lsp"); + +// 4. The PATH search uses the INSTALLED name, not the in-checkout file name: +// an installed writ produces `writ-lsp`; `_build` produces `writ_lsp.exe`. +check("the installed name is writ-lsp", INSTALLED === "writ-lsp"); +check( + "every PATH candidate ends in it", + onPath(INSTALLED).every((p) => path.basename(p).startsWith(INSTALLED)) +); +check("PATH is actually searched", onPath(INSTALLED).length > 0); + +// 5. The workspace root is the PARENT of the checkout, not the checkout. +// +// This is what the split into separate writ/ and writ-vscode/ repositories +// produces: you open the directory that holds both, so the relative default +// resolves against a folder with no _build in it, and the extension reported +// "no language server" while a perfectly good one sat one level down. +const root = fs.mkdtempSync(path.join(os.tmpdir(), "writ-resolve-")); +fs.mkdirSync(path.join(root, "writ")); +fs.writeFileSync(path.join(root, "writ", "dune-project"), "(lang dune 3.0)\n"); +fs.mkdirSync(path.join(root, "writ-vscode")); // a sibling that is NOT a checkout +fs.mkdirSync(path.join(root, "notes")); + +c = candidates(DEFAULT, [root]); +check( + "a checkout one level below the workspace root is found", + c.includes(path.join(root, "writ", DEFAULT)) +); +check("the workspace root itself is still tried first", c[0] === path.join(root, DEFAULT)); +check( + "a subdirectory that is not a checkout is not guessed at", + !c.some((p) => p.startsWith(path.join(root, "notes") + path.sep)) +); +check( + "the nested checkout still beats anything on PATH", + c.indexOf(path.join(root, "writ", DEFAULT)) < + c.findIndex((p) => p.endsWith(path.sep + INSTALLED)) +); + +// An unreadable or absent folder must not throw — a workspace folder can name a +// disconnected drive, and resolution failing there would take the whole +// extension down at activation. +let threw = false; +try { + candidates(DEFAULT, [path.join(root, "gone")]); +} catch { + threw = true; +} +check("a workspace folder that does not exist is survivable", !threw); + +// 6. Which checkout a resolved server belongs to. +// +// The panel's build button and the "older than your sources" warning both +// depend on this being the checkout that produced THIS server, and not any +// checkout that happens to be above it on disk. An installed server inside +// somebody's source tree is the case that makes the difference: it must +// report no checkout, or the panel would offer to rebuild a repository that +// has nothing to do with the server in use. +const built = path.join(root, "writ", DEFAULT); +check("a server under a checkout names that checkout", checkoutOf(built) === path.join(root, "writ")); +check( + "a server merely sitting inside a checkout names none", + checkoutOf(path.join(root, "writ", "some", "bin", "writ-lsp")) === null +); +check( + "and neither does one at the right path under a directory that is no checkout", + checkoutOf(path.join(root, "notes", DEFAULT)) === null +); + +// 7. The command line that belongs to the SAME install as the server. +// +// Looking `writ` up on PATH independently is exactly the mismatch the panel +// exists to catch: a checkout's server answering the squiggles while the +// installed `writ` answers "Check this file" would make the two disagree by +// construction. +const cliPath = path.join(root, "writ", ...locate.IN_CHECKOUT.cli.split("/")); +fs.mkdirSync(path.dirname(cliPath), { recursive: true }); +fs.writeFileSync(cliPath, ""); +check("a checkout's server is paired with that checkout's CLI", cliFor(built) === cliPath); + +fs.rmSync(cliPath); +check("a checkout that built no CLI reports none, rather than falling back to PATH", cliFor(built) === null); + +// An installed server's CLI is its neighbour: opam and the release tarball both +// put `writ` and `writ-lsp` in the same bin directory. +const bin = path.join(root, "bin"); +fs.mkdirSync(bin); +fs.writeFileSync(path.join(bin, "writ-lsp"), ""); +fs.writeFileSync(path.join(bin, process.platform === "win32" ? "writ.exe" : "writ"), ""); +check( + "an installed server is paired with the writ beside it", + cliFor(path.join(bin, "writ-lsp")) === + path.join(bin, process.platform === "win32" ? "writ.exe" : "writ") +); + +fs.rmSync(root, { recursive: true, force: true }); +done(); diff --git a/test/status.test.js b/test/status.test.js new file mode 100644 index 0000000..fa05816 --- /dev/null +++ b/test/status.test.js @@ -0,0 +1,164 @@ +// Copyright (C) 2026 Alex Kunich +// SPDX-License-Identifier: AGPL-3.0-or-later + +// What the panel says about the install, and why it says it. +// +// The verdict is the extension's one piece of judgement. Everything else here +// either finds a path or forwards a message the server wrote; this decides, +// from four facts, which of four different things has gone wrong — and it is +// shown to a user as a warning, so getting it wrong means telling someone with +// a perfectly good install that it is broken. +// +// The ORDER of the cases is the part worth pinning. A stale build reports the +// same version as a current one, so if the versions were compared first, the +// most misleading state this extension can be in would report as healthy. +// +// Run: node test/status.test.js + +const fs = require("fs"); +const os = require("os"); +const path = require("path"); +const { suite } = require("./harness"); +const { verdict } = require("../src/engine"); +const { staleness, sourcesIn } = require("../src/staleness"); +const { renderHtml, escapeHtml } = require("../src/panel"); + +const { check, done } = suite("status tests"); + +const base = { + extension: "0.1.0", + engine: "0.1.0", + stale: null, + checkout: "/w/writ", + serverPath: "/w/writ/_build/default/tooling/lsp/bin/writ_lsp.exe", +}; +const v = (over) => verdict({ ...base, ...over }); + +// --- the four states ------------------------------------------------------- + +check("matched versions, fresh build: nothing to say", v({}) === null); + +check("no server at all is the bad one", v({ serverPath: null }).level === "bad"); +check( + "and it says what still works, because highlighting keeps working and that " + + "is exactly what makes the failure hard to spot", + /highlighting/.test(v({ serverPath: null }).message) +); + +const mismatch = v({ engine: "0.2.0" }); +check("a version mismatch is a warning, not an error", mismatch.level === "warn"); +check("and it names both versions", /0\.1\.0/.test(mismatch.message) && /0\.2\.0/.test(mismatch.message)); + +const old = v({ stale: { path: "core/syntax/reader.ml" } }); +check("a stale build is a warning", old.level === "warn"); +check("and it names the file that outran it", /reader\.ml/.test(old.message)); + +const silent = v({ engine: null }); +check("a server that reports no version is its own case", silent.level === "warn"); +check( + "and is not reported as a mismatch, which would be a lie about a version " + + "nobody has", + !/mismatch/.test(silent.message) +); + +// --- the order ------------------------------------------------------------- +// +// This is the whole reason staleness exists as a separate signal. +check( + "a stale build is reported even though the versions agree", + v({ engine: "0.1.0", stale: { path: "core/data/kind.ml" } }) !== null +); +check( + "and staleness wins over a version mismatch, because rebuilding is the step " + + "that has to happen first either way", + /older than/.test(v({ engine: "0.9.9", stale: { path: "core/data/kind.ml" } }).message) +); + +// --- what the verdict asks for --------------------------------------------- + +check("in a checkout, the fix offered is a build", v({ serverPath: null }).action === "build"); +check( + "with no checkout, it is an install", + v({ serverPath: null, checkout: null }).action === "install" +); + +// --- the clock ------------------------------------------------------------- + +check("nothing is stale when there is no binary", staleness(null, [{ path: "a", mtime: 9 }], 0) === null); +check("nothing is stale when every source is older", staleness(100, [{ path: "a", mtime: 9 }], 0) === null); +check( + "a newer source makes it stale, and names the newest one", + staleness(100, [{ path: "a", mtime: 101 }, { path: "b", mtime: 900 }], 0).path === "b" +); +// dune is content-addressed: a build that changes nothing leaves the binary's +// mtime where it was, so without a record of the build HAVING RUN the warning +// could never be cleared by doing the thing it asks for. +check( + "a completed build clears it even though the binary did not move", + staleness(100, [{ path: "a", mtime: 900 }], 1000) === null +); + +// A real walk, over a real tree, because the failure that matters is finding +// nothing: writ's sources are nested three deep and a flat listing sees none. +const root = fs.mkdtempSync(path.join(os.tmpdir(), "writ-stale-")); +fs.mkdirSync(path.join(root, "tooling", "lsp", "lib", "feature"), { recursive: true }); +fs.writeFileSync(path.join(root, "tooling", "lsp", "lib", "feature", "hover.ml"), ""); +fs.mkdirSync(path.join(root, "core", "data"), { recursive: true }); +fs.writeFileSync(path.join(root, "core", "data", "kind.ml"), ""); +fs.writeFileSync(path.join(root, "core", "data", "kind.mli"), ""); +fs.mkdirSync(path.join(root, "tooling", "lsp", "_build"), { recursive: true }); +fs.writeFileSync(path.join(root, "tooling", "lsp", "_build", "stale.ml"), ""); +fs.mkdirSync(path.join(root, "tests"), { recursive: true }); +fs.writeFileSync(path.join(root, "tests", "test_lsp.ml"), ""); +fs.mkdirSync(path.join(root, "core", "stdlib"), { recursive: true }); +fs.writeFileSync(path.join(root, "core", "stdlib", "stdlib.writ"), ""); + +const found = sourcesIn(root).map((s) => s.path).sort(); +check("a source nested three deep is found", found.includes("tooling/lsp/lib/feature/hover.ml")); +check("interfaces count as sources", found.includes("core/data/kind.mli")); +check("_build is not walked", !found.some((p) => p.includes("_build"))); +check( + "tests are not sources: a changed test does not make the server wrong", + !found.some((p) => p.startsWith("tests/")) +); +check( + "and neither is the .writ standard library, which is read at runtime and " + + "never compiled in", + !found.some((p) => p.endsWith(".writ")) +); +fs.rmSync(root, { recursive: true, force: true }); + +// --- the page -------------------------------------------------------------- + +check("a version is escaped before it reaches the page", escapeHtml('&"') === "<b>&""); + +const page = renderHtml({ + extension: "0.1.0", + engineVersion: "0.1.0", + serverPath: "/w/writ/_build/default/tooling/lsp/bin/writ_lsp.exe", + checkout: "/w/writ", + stale: null, +}); +check("the panel offers the verbs", /writ\.check/.test(page) && /writ\.derive/.test(page)); +check("and a way back to the server log", /writ\.showOutput/.test(page)); +check("a healthy install draws the reassuring status, not an empty box", /status ok/.test(page)); + +const broken = renderHtml({ + extension: "0.1.0", + engineVersion: null, + serverPath: null, + checkout: null, + stale: null, +}); +check("no server draws the bad status", /status bad/.test(broken)); +check("and the button offered is the update, not a build of a checkout that is not there", /writ\.update/.test(broken)); +check("the engine version reads as not found rather than blank", /not found/.test(broken)); + +const nover = renderHtml({ ...base, engineVersion: null, engine: undefined }); +check( + "a server that reported no version reads as not reported, which is a " + + "different thing from not found", + /not reported/.test(nover) +); + +done(); diff --git a/test/watcher.test.js b/test/watcher.test.js new file mode 100644 index 0000000..830169a --- /dev/null +++ b/test/watcher.test.js @@ -0,0 +1,90 @@ +// Copyright (C) 2026 Alex Kunich +// SPDX-License-Identifier: AGPL-3.0-or-later + +// Drives the server-binary watcher against a real file on disk. +// +// The watcher's failure mode is SILENCE — it either fires or it does not, and +// one that never fires looks exactly like a server that is simply up to date. +// That is the bug it exists to fix, so it does not get to go untested. The +// first version of it never fired at all; this file is what caught that. +// +// Nothing is stubbed. The watcher takes its restart as an argument rather than +// reaching for a client, so it only ever stats a path and calls a function — +// which is the whole reason it can be checked with no editor in the room. +// +// Run: node test/watcher.test.js + +const fs = require("fs"); +const os = require("os"); +const path = require("path"); +const { suite } = require("./harness"); +const { watchServerBinary } = require("../src/watcher"); + +const POLL = 40; // fast enough to gate; the shipped default is 2000 +const sleep = (ms) => new Promise((r) => setTimeout(r, ms)); +const { check, done } = suite("watcher tests"); + +(async () => { + const dir = fs.mkdtempSync(path.join(os.tmpdir(), "writ-watch-")); + const bin = path.join(dir, "writ_lsp.exe"); + fs.writeFileSync(bin, "v1"); + + let restarts = 0; + let rebuilt = 0; + const logs = []; + const failures = []; + const w = watchServerBinary(bin, (m) => logs.push(m), POLL, { + restart: async () => { + restarts++; + }, + onRestart: () => rebuilt++, + onFailure: (e) => failures.push(e), + }); + + await sleep(POLL * 6); + check("an unchanged binary does not restart the server", restarts === 0); + + // Replaced, not edited in place — which is what dune does, and why the stamp + // carries the inode and not just the mtime. + fs.rmSync(bin); + fs.writeFileSync(bin, "v2-different-length"); + await sleep(POLL * 8); + check("a replaced binary restarts the server", restarts === 1); + check("and says so in the output channel", logs.length === 2); + // The panel has to be told, or it goes on showing the staleness warning that + // the very build just cleared — the one place in the editor still claiming + // you are out of date. + check("and the rest of the extension is told the build landed", rebuilt === 1); + + await sleep(POLL * 6); + check("a settled binary restarts it once, not repeatedly", restarts === 1); + + // A vanished file is a build in progress, not a reason to do anything. + fs.rmSync(bin); + await sleep(POLL * 6); + check("a missing binary is not a restart", restarts === 1); + check("nothing was reported to the user", failures.length === 0); + + w.dispose(); + + // A restart that throws must reach the user, not the void: the server on disk + // has already changed, so staying quiet leaves the editor answering from a + // binary that is gone. + const bin2 = path.join(dir, "two.exe"); + fs.writeFileSync(bin2, "a"); + const seen = []; + const w2 = watchServerBinary(bin2, () => {}, POLL, { + restart: async () => { + throw new Error("no"); + }, + onFailure: (e) => seen.push(e), + }); + fs.rmSync(bin2); + fs.writeFileSync(bin2, "bbbbbb"); + await sleep(POLL * 8); + check("a restart that fails is reported", seen.length === 1); + w2.dispose(); + + fs.rmSync(dir, { recursive: true, force: true }); + done(); +})();