Prepare VS Code extension for Marketplace release

.github/workflows/vscode-extension.yml

@@ -0,0 +1,61 @@
+name: VS Code extension
+
+on:
+  push:
+    branches: [main]
+    paths:
+      - "editors/vscode/**"
+      - ".github/workflows/vscode-extension.yml"
+  pull_request:
+    branches: [main]
+    paths:
+      - "editors/vscode/**"
+      - ".github/workflows/vscode-extension.yml"
+  workflow_dispatch:
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+permissions: {}
+
+jobs:
+  package:
+    name: Package VSIX
+    runs-on: ubuntu-latest
+    permissions:
+      contents: read
+    defaults:
+      run:
+        working-directory: editors/vscode
+    steps:
+      - uses: actions/checkout@v7
+        with:
+          persist-credentials: false
+
+      - name: Set up Node.js
+        uses: actions/setup-node@v6
+        with:
+          node-version: "22"
+          cache: npm
+          cache-dependency-path: editors/vscode/package-lock.json
+
+      - name: Install dependencies
+        run: npm ci
+
+      - name: Check extension source
+        run: npm run check
+
+      - name: Inspect packaged files
+        run: npm run package:list
+
+      - name: Build VSIX
+        run: npm run package
+
+      - name: Upload VSIX
+        uses: actions/upload-artifact@v7
+        with:
+          name: vera-language-vsix-${{ github.sha }}
+          path: editors/vscode/*.vsix
+          if-no-files-found: error
+          retention-days: 30

editors/vscode/.vscodeignore

@@ -1,6 +1,8 @@
 .git/**
 .gitignore
 .vscode/**
+*.vsix
+package-lock.json
 *.md
 !README.md
 !CHANGELOG.md

editors/vscode/CHANGELOG.md

@@ -4,6 +4,7 @@
 
 Language server integration.
 
+- First VS Code Marketplace release as `veralang.vera-language`
 - The extension now starts Vera's language server (`vera lsp`) for
   `.vera` files: proof-aware diagnostics with verification-tier hints,
   expression-type hover, De Bruijn slot go-to-definition, and

editors/vscode/README.md

@@ -18,9 +18,9 @@ edit and provides:
 - **Typed-hole completion** — at a `?` hole, completion lists the
   in-scope bindings that fit, with their types.
 
-Requires the `vera` binary with the `[lsp]` extra (see
-[Requirements](#requirements)); without it the extension quietly stays
-in syntax-highlighting-only mode. See [LSP_SERVER.md](../../LSP_SERVER.md)
+Requires the `vera` binary with the `[lsp]` extra from PyPI (see
+[Requirements](#requirements)); without it the extension stays in
+syntax-highlighting-only mode. See [LSP_SERVER.md](../../LSP_SERVER.md)
 for everything the server can do, including the custom methods for
 coding agents.
 
@@ -44,21 +44,21 @@ coding agents.
 
 ## Requirements
 
-For language-server features the extension needs a `vera` binary that
-can serve LSP — from a clone of the repo:
+For language-server features the extension needs Python 3.11+ and a
+`vera` binary with the optional LSP dependencies:
 
 ```bash
-pip install -e ".[lsp]"     # or ".[dev]", which includes it
+python -m pip install "veralang[lsp]"
 ```
 
-The extension finds the binary in this order: the `vera.lsp.path`
-setting (if you changed it), a **workspace-local venv**
-(`.venv/bin/vera` — which means a standard from-source clone needs no
-configuration at all), then `vera` from `PATH`. VS Code launched from
-the GUI does not inherit your shell's `PATH`, so the workspace-venv
-detection is what makes the zero-config case work. If the server
-fails to start you get one warning with an *Open Settings* button;
-syntax highlighting works with no binary at all.
+The base `veralang` installation does not include the optional language
+server dependencies, so keep the `[lsp]` extra in the command. The
+extension finds the binary in this order: the `vera.lsp.path` setting
+(if changed from its default), a workspace-local virtual environment
+(`.venv/bin/vera` or `.venv\\Scripts\\vera.exe`), then `vera` from
+`PATH`. If a GUI-launched VS Code cannot see the Python installation,
+set `vera.lsp.path` to the absolute path of the `vera` executable.
+Syntax highlighting works without the binary.
 
 ## Settings
 
@@ -72,7 +72,23 @@ The **Vera: Restart Language Server** command restarts the server
 
 ## Installation
 
-### From source (recommended for now)
+### VS Code Marketplace
+
+Install **Vera Language** from the Extensions view, or run:
+
+```bash
+code --install-extension veralang.vera-language
+```
+
+[Open Vera Language in the VS Code Marketplace](https://marketplace.visualstudio.com/items?itemName=veralang.vera-language).
+
+### From VSIX
+
+```bash
+code --install-extension vera-language-0.2.0.vsix
+```
+
+### From source
 
 **Fresh clone:**
 
@@ -94,18 +110,6 @@ The `npm install` fetches the LSP client library
 (`vscode-languageclient`); skipping it is fine — you just get syntax
 highlighting without the language server.
 
-### From VSIX
-
-If a packaged `.vsix` is available:
-
-```bash
-code --install-extension vera-language-0.2.0.vsix
-```
-
-### VS Code Marketplace
-
-Not yet published. This is planned once the language reaches a stable release.
-
 ## Scope reference
 
 The grammar uses standard TextMate scope conventions, so it works with any colour theme. Key assignments:
@@ -132,6 +136,7 @@ The grammar uses standard TextMate scope conventions, so it works with any colou
 
 - [Vera language](https://veralang.dev/)
 - [Vera on GitHub](https://github.com/aallan/vera)
+- [Vera Language on the VS Code Marketplace](https://marketplace.visualstudio.com/items?itemName=veralang.vera-language)
 - [TextMate bundle](https://github.com/aallan/vera/tree/main/editors/textmate) (same grammar, TextMate 2 packaging)
 
 ## Licence

editors/vscode/extension.js

@@ -29,11 +29,10 @@ function loadLanguageClient() {
         return require("vscode-languageclient/node");
     } catch (err) {
         log(
-            "vscode-languageclient is not installed; running in " +
-            "syntax-highlighting-only mode. For language-server " +
-            "features (proof-aware diagnostics, hover, slot " +
-            "go-to-definition, hole completion), run `npm install` " +
-            "in the extension directory. " + err.message,
+            "vscode-languageclient is missing; running in " +
+            "syntax-highlighting-only mode. Reinstall the extension, " +
+            "or run `npm install` when using a source checkout. " +
+            err.message,
         );
         return null;
     }
@@ -118,16 +117,18 @@ async function startClient(lc) {
         log(
             "Failed to start `vera lsp`. Check that the vera binary " +
             "is on PATH (or set the vera.lsp.path setting) and that " +
-            'the [lsp] extra is installed: pip install -e ".[lsp]". ' +
+            "the PyPI package includes the LSP extra: " +
+            'python -m pip install "veralang[lsp]". ' +
             "Details: " + err.message,
         );
         client = undefined;
         // One actionable toast — the silent output-channel line made
         // "nothing is showing up" needlessly hard to diagnose.
         const choice = await vscode.window.showWarningMessage(
             "Vera language server failed to start (syntax highlighting " +
-            "still works). Point the vera.lsp.path setting at your " +
-            "vera binary, e.g. .venv/bin/vera in a clone.",
+            "still works). Install it with `python -m pip install " +
+            '\"veralang[lsp]\"`, or point vera.lsp.path at the Vera ' +
+            "executable.",
             "Open Settings",
         );
         if (choice === "Open Settings") {