Add more control over Rzk update checks, bump version, update changelog

Author: fizruk

CHANGELOG.md

@@ -4,6 +4,51 @@ All notable changes to the "rzk-1-experimental-highlighting" extension will be d
 
 Check [Keep a Changelog](http://keepachangelog.com/) for recommendations on how to structure this file.
 
+## v0.4.6 - 2026-05-31
+
+Syntax highlighting:
+
+- Extend the TextMate grammar to match the latest Rzk surface syntax. New
+  constructs covered: block comments (`{- ... -}`), hole identifiers (`?`),
+  modal type bracketing (`<| ... |>`), standalone `let` keyword, ASCII `_id`
+  modality, `Unit` type and `unit` term, all tope/cube inversions
+  (`invᵒᵖ`, `uninvᵒᵖ`, `flipᵒᵖ`, `unflipᵒᵖ` + ASCII variants), and the
+  internal `$extract$` keyword (rendered as `invalid` to signal it is not
+  for user code).
+- Fix lambda highlighting: `\` after a space (e.g. `:= \ x -> x`) now
+  receives the lambda scope, and `->` correctly closes the lambda region.
+  Two bugs were involved: a `\b` word-boundary in the lambda begin pattern
+  that could not match between space and `\`, and a `#param-identifiers`
+  regex that could match a zero-length span and silently collapse the
+  enclosing begin/end region.
+- Add modal-syntax highlighting contributed by
+  [Islam Talipov](https://github.com/LIshy2) ([#73](https://github.com/rzk-lang/vscode-rzk/pull/73)):
+  modal-type brackets, `mod`/`let mod`, and the three Unicode modalities
+  (`♭`, `♯`, `ᵒᵖ`) plus ASCII forms.
+
+UX:
+
+- Suppress VS Code's automatic color decorators for Rzk files, so `#def`,
+  `#abc`, etc. no longer get a colour-swatch preview from being mistaken
+  for hex colour codes.
+- Add the `Rzk: Check for updates` command for triggering an on-demand
+  update check ([#57](https://github.com/rzk-lang/vscode-rzk/issues/57)).
+- Add the `rzk.updateCheckIntervalMinutes` setting (default 60) to
+  configure how often the extension checks GitHub for new `rzk` releases;
+  set to `0` to disable the periodic check
+  ([#56](https://github.com/rzk-lang/vscode-rzk/issues/56)).
+
+Project hygiene:
+
+- Bump CI from Node 18 to Node 20 (the latest `@vscode/vsce` requires
+  Node 20+); bump `actions/setup-node`, `actions/upload-artifact`, and
+  `actions/download-artifact` from v3 to v4.
+- Add a grammar test suite (`vscode-tmgrammar-test` for inline-annotated
+  unit tests and `vscode-tmgrammar-snap` for snapshot tests over real-world
+  Rzk extracted from sHoTT). `npm test` runs both layers; CI invokes it.
+- Update the README to document `rzk.format.enable` and to mention support
+  for `*.rzk.tex` files.
+
 ## v0.4.5 - 2023-12-08
 
 - Added some sensible default settings for Rzk files formatting and a message upon formatting for the first time ([#66](https://github.com/rzk-lang/vscode-rzk/pull/66))

README.md

@@ -10,11 +10,12 @@ Syntax and semantic highlighting for [`rzk`](https://rzk-lang.github.io/rzk/), a
 
 Features:
 
-1. Basic syntax highlighting with a simple TextMate grammar.
+1. Basic syntax highlighting with a simple TextMate grammar (for `*.rzk`, `*.rzk.md`, and `*.rzk.tex` files).
 2. Semantic highlighting via LSP (you must have `rzk` version v0.6 or above).
 3. Prompts for installing/updating `rzk` binaries from GitHub Releases automatically (usable from local Terminal).
 4. Markdown Preview button for `*.rzk.md` files.
 5. Automatic typechecking for all files listed in `rzk.yaml`
+6. Automatic code formatting on save (can be disabled via the `rzk.format.enable` setting).
 
 See [Changelog](CHANGELOG.md) for recent updated and changes.
 
@@ -43,7 +44,9 @@ Extension settings can be configured by going to the settings page (using the me
 
 The currently available settings are:
 
-| Name                   | Type      | Default value | Description                                                                                                                                   |
-| ---------------------- | --------- | ------------- | --------------------------------------------------------------------------------------------------------------------------------------------- |
-| `rzk.path`             | `string`  | `""`          | The path to the `rzk` executable to use for the language server. `""` (default) means that `rzk` executable available in `PATH` will be used. |
-| `rzk.fetchPrereleases` | `boolean` | `false`       | If true, will include releases marked as \"pre-release\" on GitHub when fetching the latest binaries.                                         |
+| Name                             | Type      | Default value | Description                                                                                                                                                                                                                  |
+| -------------------------------- | --------- | ------------- | ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- |
+| `rzk.path`                       | `string`  | `""`          | The path to the `rzk` executable to use for the language server. `""` (default) means that `rzk` executable available in `PATH` will be used.                                                                                |
+| `rzk.fetchPrereleases`           | `boolean` | `false`       | If true, will include releases marked as \"pre-release\" on GitHub when fetching the latest binaries.                                                                                                                        |
+| `rzk.format.enable`              | `boolean` | `true`        | Enable the Rzk formatter (provided via LSP). Disable to opt out of formatting on save.                                                                                                                                       |
+| `rzk.updateCheckIntervalMinutes` | `number`  | `60`          | How often (in minutes) to check GitHub for new releases of `rzk`. Only applies to extension-managed installations; set to `0` to disable periodic checks. You can always trigger a check via the `Rzk: Check for updates` command. |

package.json

@@ -3,7 +3,7 @@
   "displayName": "Rzk",
   "description": "Interactive theorem proving support in VS Code for Rzk, a proof assistant for synthetic ∞-categories",
   "icon": "images/icon.png",
-  "version": "0.4.5",
+  "version": "0.4.6",
   "repository": "https://github.com/rzk-lang/vscode-rzk",
   "publisher": "NikolaiKudasovfizruk",
   "main": "./out/extension.js",
@@ -158,6 +158,12 @@
           "type": "boolean",
           "default": false,
           "description": "If true, will include releases marked as \"pre-release\" on GitHub when fetching the latest binaries"
+        },
+        "rzk.updateCheckIntervalMinutes": {
+          "type": "number",
+          "default": 60,
+          "minimum": 0,
+          "description": "How often (in minutes) to check GitHub for new releases of rzk. Only applies to extension-managed installations; set to 0 to disable periodic checks (you can still trigger a check manually via the \"Rzk: Check for updates\" command)."
         }
       }
     },
@@ -196,6 +202,10 @@
       {
         "command": "rzk.restartLspServer",
         "title": "Rzk: Restart LSP server"
+      },
+      {
+        "command": "rzk.checkForUpdates",
+        "title": "Rzk: Check for updates"
       }
     ],
     "yamlValidation": [

src/extension.ts

@@ -2,7 +2,11 @@ import * as vscode from 'vscode';
 import { spawnSync } from 'node:child_process';
 import { delimiter } from 'node:path';
 import { output } from './logging';
-import { clearLocalInstallations, installRzkIfNotExists } from './installRzk';
+import {
+  checkForUpdates,
+  clearLocalInstallations,
+  installRzkIfNotExists,
+} from './installRzk';
 import {
   LanguageClient,
   LanguageClientOptions,
@@ -67,6 +71,24 @@ export function activate(context: vscode.ExtensionContext) {
     }
   );
 
+  vscode.commands.registerCommand('rzk.checkForUpdates', async () => {
+    const path = locateRzk(context);
+    if (!path) {
+      vscode.window.showWarningMessage(
+        'Cannot find rzk to check for updates. Configure `rzk.path` or install rzk first.'
+      );
+      return;
+    }
+    // Pass binFolder only when rzk is the extension-managed installation,
+    // so an interactive update prompt is offered (instead of just a notice).
+    const binExtension = process.platform === 'win32' ? '.exe' : '';
+    const managedPath = vscode.Uri.joinPath(
+      binFolder,
+      'rzk' + binExtension
+    ).fsPath;
+    await checkForUpdates(path, path === managedPath ? binFolder : undefined);
+  });
+
   let client: LanguageClient;
   if (rzkPath) {
     let serverOptions: ServerOptions = {

src/installRzk.ts

@@ -71,9 +71,16 @@ export async function installRzkIfNotExists({
     const path = join(binFolder.fsPath, localBin[0]);
     output.appendLine('Found local installation of rzk: ' + path);
     await checkForUpdates(path, binFolder);
-    // Repeat the check for updates every hour
-    // TODO: make the check period configurable by the user
-    setInterval(() => checkForUpdates(path, binFolder), 1000 * 60 * 60);
+    const intervalMinutes =
+      vscode.workspace
+        .getConfiguration()
+        .get<number>('rzk.updateCheckIntervalMinutes') ?? 60;
+    if (intervalMinutes > 0) {
+      setInterval(
+        () => checkForUpdates(path, binFolder),
+        1000 * 60 * intervalMinutes
+      );
+    }
     return;
   }
 
@@ -233,7 +240,7 @@ function buildRzkWithPackageManager(
   });
 }
 
-async function checkForUpdates(binPath: string, binFolder?: vscode.Uri) {
+export async function checkForUpdates(binPath: string, binFolder?: vscode.Uri) {
   output.appendLine('Checking if updates are available');
   const version = spawnSync(binPath, ['version']).stdout.toString();
   const latestRelease = await fetchLatestCompatibleRelease();