From 868bed4e17b054f8b9b321742627d9fbb31ad2c4 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Thu, 18 Jun 2026 06:24:34 -0700 Subject: [PATCH] Run SANY before invoking TLAPS proof commands TLAPS accepts "raw TLA" (rTLA) that SANY rejects: formulas that are not insensitive to stuttering, permitting unrestrictive assertions about behaviors that should be unassertable in TLA+. Without a SANY check, a user can obtain a passing TLAPS result for a module that is not valid TLA+. Parse the saved module with SANY first (reusing tlaplus.parse) and abort the proof check, surfacing diagnostics, when SANY reports errors. Closes Github issue #526 https://github.com/tlaplus/vscode-tlaplus/issues/526 [Feature][TLAPS] Co-authored-by: Claude Opus 4.8 Signed-off-by: Markus Alexander Kuppe --- src/commands/parseModule.ts | 6 +++ src/main.ts | 1 + src/tlaps.ts | 87 ++++++++++++++++++++++++++++++++----- 3 files changed, 84 insertions(+), 10 deletions(-) diff --git a/src/commands/parseModule.ts b/src/commands/parseModule.ts index 3268d6dd..41d428fc 100644 --- a/src/commands/parseModule.ts +++ b/src/commands/parseModule.ts @@ -94,6 +94,12 @@ export async function transpilePlusCal(fileUri: vscode.Uri, token?: vscode.Cance */ export async function parseSpec(fileUri: vscode.Uri, token?: vscode.CancellationToken): Promise { throwIfCancelled(token); + // SANY runs on a filesystem path, so only file:// URIs are supported. + // Reject untitled or virtual (e.g. jarfile://) URIs with a clear error + // instead of letting the underlying process fail obscurely on fsPath. + if (fileUri.scheme !== 'file') { + throw new Error(`Cannot parse '${fileUri.toString()}': only files saved on disk are supported.`); + } const procInfo = await runSany(fileUri.fsPath); sanyOutChannel.bindTo(procInfo); const cancellationDisposable = registerCancellation(procInfo, token); diff --git a/src/main.ts b/src/main.ts index 0386839b..58c94fa8 100644 --- a/src/main.ts +++ b/src/main.ts @@ -262,6 +262,7 @@ export async function activate(context: vscode.ExtensionContext): Promise ); tlapsClient = new TlapsClient( context, + diagnostic, details => currentProofStepWebviewViewProvider.showProofStepDetails(details), configChanged => currentProofStepWebviewViewProvider.considerConfigChanged(configChanged) ); diff --git a/src/tlaps.ts b/src/tlaps.ts index adc72550..6091dc5b 100644 --- a/src/tlaps.ts +++ b/src/tlaps.ts @@ -28,6 +28,9 @@ import { InitResponseCapabilitiesExperimental, } from './model/paths'; import { moduleSearchPaths, TLAPS } from './paths'; +import { parseSpec } from './commands/parseModule'; +import { SanyData } from './parsers/sany'; +import { applyDCollection } from './diagnostic'; export enum proofStateNames { proved = 'proved', @@ -67,6 +70,7 @@ export class TlapsClient { constructor( private context: vscode.ExtensionContext, + private diagnostic: vscode.DiagnosticCollection, private currentProofStepDetailsListener: ((details: TlapsProofStepDetails) => void), private configChangedListener: ((configChanged: TlapsConfigChanged) => void) ) { @@ -118,16 +122,9 @@ export class TlapsClient { if (!this.client) { return; } - vscode.commands.executeCommand('tlaplus.tlaps.check-step.lsp', - { - uri: te.document.uri.toString(), - version: te.document.version - } as VersionedTextDocumentIdentifier, - { - start: te.selection.start, - end: te.selection.end - } as Range, - ); + this.checkStep(te).catch((err) => { + vscode.window.showErrorMessage(`TLAPS proof check failed: ${err}`); + }); } )); context.subscriptions.push(vscode.workspace.onDidChangeConfiguration(event => { @@ -174,6 +171,76 @@ export class TlapsClient { this.tryStop(); } + // Runs SANY on the module before forwarding the proof check to TLAPS. + // + // TLAPS and SANY do not accept exactly the same language: TLAPS accepts some + // specifications that SANY (the standard TLA+ front end) correctly rejects. + // TLAPS accepts "raw TLA" (rTLA), which permits unrestrictive assertions + // about behaviors that should be unassertable in TLA+, i.e. formulas that + // are not insensitive to stuttering. Eliminating rTLA is the primary reason + // for running SANY before TLAPS. + // To preserve the invariant the TLA+ Toolbox used to enforce, we parse the + // module with SANY first (reusing the implementation behind `tlaplus.parse`) + // and only invoke TLAPS if the module is a valid TLA+ module. + private async checkStep(te: vscode.TextEditor) { + const document = te.document; + // SANY and the TLAPS LSP expect file:// documents. + if (document.uri.scheme !== 'file') { + vscode.window.showWarningMessage( + 'TLAPS proof checking is only available for TLA+ files saved on disk.' + ); + return; + } + // Capture the selection before any `await`, as it may change meanwhile. + const selection: Range = { + start: te.selection.start, + end: te.selection.end, + }; + // Persist the buffer so SANY and TLAPS operate on the same content. + if (document.isDirty && !await document.save()) { + return; + } + let sanyData: SanyData; + try { + sanyData = await parseSpec(document.uri); + } catch (err) { + // SANY itself failed to run (not a parse error). Let the user decide + // whether to proceed without the SANY check; default to aborting. + const continueLabel = 'Run TLAPS anyway'; + const choice = await vscode.window.showErrorMessage( + `Error parsing module with SANY: ${err}`, + continueLabel + ); + if (choice === continueLabel) { + this.runCheckStep(document, selection); + } + return; + } + applyDCollection(sanyData.dCollection, this.diagnostic); + const hasErrors = sanyData.dCollection.getMessages().some( + (msg) => msg.diagnostic.severity === vscode.DiagnosticSeverity.Error + ); + if (hasErrors) { + // SANY's diagnostics already annotate the module (editor markers and + // the Problems view), so don't invoke TLAPS on an invalid module. + return; + } + this.runCheckStep(document, selection); + } + + private runCheckStep(document: vscode.TextDocument, selection: Range) { + if (!this.client) { + return; + } + vscode.commands.executeCommand('tlaplus.tlaps.check-step.lsp', + { + uri: document.uri.toString(), + version: document.version + } as VersionedTextDocumentIdentifier, + selection, + ); + } + private readConfig(): boolean { const config = vscode.workspace.getConfiguration(); const configEnabled = config.get('tlaplus.tlaps.enabled');