From f8ad1baaa7f43a9abd45b76d0981f396c5710126 Mon Sep 17 00:00:00 2001 From: jzxia Date: Mon, 20 Jul 2026 21:50:39 +0800 Subject: [PATCH 1/7] feat: add "T" button for LEO-III-STC type-checker --- tptplus/client/src/extension.ts | 4 + tptplus/client/src/prettyPrint/remote.ts | 4 +- tptplus/client/src/systemB4TptpOutput.ts | 42 ++++- tptplus/client/src/typeCheck/command.ts | 122 ++++++++++++++ tptplus/client/src/typeCheck/errors.ts | 59 +++++++ .../client/test/systemB4TptpOutput.test.js | 153 ++++++++++++++++++ tptplus/client/test/typeCheckErrors.test.js | 37 +++++ tptplus/package.json | 18 ++- 8 files changed, 435 insertions(+), 4 deletions(-) create mode 100644 tptplus/client/src/typeCheck/command.ts create mode 100644 tptplus/client/src/typeCheck/errors.ts create mode 100644 tptplus/client/test/systemB4TptpOutput.test.js create mode 100644 tptplus/client/test/typeCheckErrors.test.js diff --git a/tptplus/client/src/extension.ts b/tptplus/client/src/extension.ts index bf1a570..d03f805 100644 --- a/tptplus/client/src/extension.ts +++ b/tptplus/client/src/extension.ts @@ -14,6 +14,7 @@ import { import { errorMessage } from './errorMessage'; import { createSystemB4TptpForm } from './systemTptpForms'; import { registerPrettyPrintCommand } from './prettyPrint/command'; +import { registerTypeCheckCommand } from './typeCheck/command'; let client: LanguageClient; @@ -319,6 +320,9 @@ export function activate(context: ExtensionContext) { //@ FORMAT A PROBLEM BY RUNNING JJPARSER LOCALLY, USING REMOTE SYSTEMB4TPTP AS FALLBACK context.subscriptions.push(registerPrettyPrintCommand(context)); + //@ CHECK TYPES WITH LEO-III-STC THROUGH SYSTEMONTPTP + context.subscriptions.push(registerTypeCheckCommand()); + //@ RUN A THEOREM THROUGH SYSTEMONTPTP const proveProblem = vscode.commands.registerCommand('tptp.proveProblem', async (uri: vscode.Uri) => { diff --git a/tptplus/client/src/prettyPrint/remote.ts b/tptplus/client/src/prettyPrint/remote.ts index 34c10c1..e2386be 100644 --- a/tptplus/client/src/prettyPrint/remote.ts +++ b/tptplus/client/src/prettyPrint/remote.ts @@ -1,6 +1,6 @@ import { errorMessage } from '../errorMessage'; import { - extractSystemB4TptpOutput, + extractSystemB4TptpHtmlOutput, lastNonemptyLine } from '../systemB4TptpOutput'; import { createSystemB4TptpForm } from '../systemTptpForms'; @@ -25,7 +25,7 @@ export async function formatTptpRemotely( }; } - const output = extractSystemB4TptpOutput(await response.text()); + const output = extractSystemB4TptpHtmlOutput(await response.text()); if (output === undefined) { return { kind: 'failure', message: 'unrecognized response' }; } diff --git a/tptplus/client/src/systemB4TptpOutput.ts b/tptplus/client/src/systemB4TptpOutput.ts index 894a727..3839804 100644 --- a/tptplus/client/src/systemB4TptpOutput.ts +++ b/tptplus/client/src/systemB4TptpOutput.ts @@ -3,7 +3,7 @@ import { JSDOM } from 'jsdom'; /** * Extract the text between `
` and `
` from the HTML response of System B4 TPTP. */ -export function extractSystemB4TptpOutput(html: string): string | undefined { +export function extractSystemB4TptpHtmlOutput(html: string): string | undefined { const dom = new JSDOM(html); const preText = dom.window.document.querySelector('pre')?.textContent ?? undefined; if (preText === undefined) { @@ -40,3 +40,43 @@ export function lastNonemptyLine(text: string): string | undefined { return undefined; } + +/** Finds an SZS status line outside an SZS output block. */ +function getSzsStatusLine(output: string): string | undefined { + for (const line of output.split(/\r?\n/)) { + if (/^% SZS output start \S+/.test(line)) { + return undefined; + } + if (/^% SZS status \S+/.test(line)) { + return line; + } + } + + return undefined; +} + +/** Extracts the status name from an SZS status line outside an SZS output block. */ +export function getSzsStatus(output: string): string | undefined { + return getSzsStatusLine(output)?.match(/^% SZS status (\S+)/)?.[1]; +} + +/** Extracts the message after the first colon in an SZS status line. */ +export function getSzsStatusMessage(output: string): string | undefined { + const statusLine = getSzsStatusLine(output); + const colonIndex = statusLine?.indexOf(':') ?? -1; + if (!statusLine || colonIndex < 0) { + return undefined; + } + + return statusLine.slice(colonIndex + 1).trim() || undefined; +} + +/** Extracts the content between the outermost SZS output markers. */ +export function getSzsOutput(output: string): string | undefined { + const szsOutput = output.match( + /^% SZS output start \S+[^\r\n]*\r?\n([\s\S]*)\r?\n% SZS output end \S+[^\r\n]*$/m + )?.[1]; + + // A greedy capture can consume the `\r` from the final CRLF delimiter. + return szsOutput?.replace(/\r$/, ''); +} diff --git a/tptplus/client/src/typeCheck/command.ts b/tptplus/client/src/typeCheck/command.ts new file mode 100644 index 0000000..9165489 --- /dev/null +++ b/tptplus/client/src/typeCheck/command.ts @@ -0,0 +1,122 @@ +import * as path from 'path'; +import * as vscode from 'vscode'; + +import { errorMessage } from '../errorMessage'; +import { + getSzsOutput, + getSzsStatus, + getSzsStatusMessage +} from '../systemB4TptpOutput'; +import { + createLeoIIITypeErrorDiagnostics, + getLeoIIITypeErrors +} from './errors'; + +const SYSTEM_ON_TPTP_URL = 'https://tptp.org/cgi-bin/SystemOnTPTPFormReply'; +const LEO_III_STC = 'Leo-III-STC---'; // SystemB4TPTP will automatically run the latest version of LEO-III-STC it has available +const TYPE_CHECK_RUNNING_CONTEXT_KEY = 'tptp.typeCheckRunning'; + +function createLeoIIITypeCheckForm(document: vscode.TextDocument): FormData { + const form = new FormData(); + + // These are the fields used by RemoteSoT.py for one selected system. + form.append('NoHTML', '1'); + form.append('QuietFlag', '-q1'); + form.append('SubmitButton', 'RunSelectedSystems'); + form.append('X2TPTP', ''); + form.append('ProblemSource', 'UPLOAD'); + form.append(`System___${LEO_III_STC}`, LEO_III_STC); + form.append(`TimeLimit___${LEO_III_STC}`, '60'); + form.append( + 'UPLOADProblem', + new Blob([document.getText()], { type: 'text/plain' }), + path.basename(document.fileName) || 'problem.p' + ); + + return form; +} + +/** Registers the command that asks LEO-III-STC on SystemB4TPTP to type-check a TPTP document. */ +export function registerTypeCheckCommand(): vscode.Disposable { + let typeCheckRunning = false; + + const diagnostics = vscode.languages.createDiagnosticCollection('tptpTypeCheck'); + const command = vscode.commands.registerCommand('tptp.typeCheck', async (uri?: vscode.Uri) => { + if (typeCheckRunning) { + vscode.window.showInformationMessage('LEO-III-STC is already checking types.'); + return; + } + + if (!uri) { + const activeEditor = vscode.window.activeTextEditor; + if (!activeEditor) { + vscode.window.showErrorMessage('No TPTP file is currently open.'); + return; + } + uri = activeEditor.document.uri; + } + + typeCheckRunning = true; + try { + await vscode.commands.executeCommand('setContext', TYPE_CHECK_RUNNING_CONTEXT_KEY, true); + + const document = await vscode.workspace.openTextDocument(uri); + const checkedDocumentVersion = document.version; + diagnostics.delete(document.uri); + const response = await fetch(SYSTEM_ON_TPTP_URL, { + method: 'POST', + body: createLeoIIITypeCheckForm(document) + }); + + if (!response.ok) { + throw new Error(`HTTP ${response.status}: ${response.statusText || 'request failed'}`); + } + + const output = await response.text(); + const status = getSzsStatus(output); + const statusMessage = getSzsStatusMessage(output); + const szsOutput = getSzsOutput(output); + const outputSuffix = [statusMessage, szsOutput] + .filter((message): message is string => Boolean(message)) // discard '' or undefined + .map(message => `\n${message}`) + .join(''); + if (status === 'Success') { + vscode.window.showInformationMessage(`LEO-III-STC type check succeeded.`); + } else if (status === 'TypeError') { + if (document.version === checkedDocumentVersion) { + const typeErrors = getLeoIIITypeErrors(szsOutput ?? output); + diagnostics.set( + document.uri, + createLeoIIITypeErrorDiagnostics(document, typeErrors) + ); + vscode.window.showErrorMessage( + `LEO-III-STC found type error(s).${szsOutput ? `\n${szsOutput}` : ''}` + ); + } else { + vscode.window.showErrorMessage( + `TPTP file changed while type-checking. Please run the type-checker again.` + ); + } + } else if (status) { + vscode.window.showErrorMessage(`LEO-III-STC reported ${status}.${outputSuffix}`); + } else { + vscode.window.showErrorMessage(`LEO-III-STC returned an unrecognized response: ${output}`); + } + } catch (error: unknown) { + vscode.window.showErrorMessage( + `Failed to check types with LEO-III-STC: ${errorMessage(error)}` + ); + } finally { + typeCheckRunning = false; + await vscode.commands.executeCommand('setContext', TYPE_CHECK_RUNNING_CONTEXT_KEY, false); + } + }); + + return vscode.Disposable.from( + diagnostics, + command, + vscode.workspace.onDidChangeTextDocument(event => { + diagnostics.delete(event.document.uri); + }) + ); +} diff --git a/tptplus/client/src/typeCheck/errors.ts b/tptplus/client/src/typeCheck/errors.ts new file mode 100644 index 0000000..be445bf --- /dev/null +++ b/tptplus/client/src/typeCheck/errors.ts @@ -0,0 +1,59 @@ +import type * as vscode from 'vscode'; + +const TYPE_CHECK_DIAGNOSTIC_SOURCE = 'LEO-III-STC type checker'; +// DiagnosticSeverity.Warning is 1 in the VS Code API. Keeping this module's +// VS Code dependency type-only also makes the error parser independently testable. +const WARNING_DIAGNOSTIC_SEVERITY: vscode.DiagnosticSeverity = 1; + +export interface LeoIIITypeError { + formulaName: string; + /** One-based source line reported by LEO-III-STC. */ + line: number; + /** One-based source character reported by LEO-III-STC. */ + character: number; + message: string; +} + +/** Extracts every source-located type error reported by LEO-III-STC. */ +export function getLeoIIITypeErrors(output: string): LeoIIITypeError[] { + const typeErrors: LeoIIITypeError[] = []; + const typeErrorPattern = /Illtyped formula ([^\r\n]+?) in line ([1-9]\d*):([1-9]\d*)\./g; + + for (const match of output.matchAll(typeErrorPattern)) { + typeErrors.push({ + formulaName: match[1], + line: Number(match[2]), + character: Number(match[3]), + message: match[0] + }); + } + + return typeErrors; +} + +/** Creates warning diagnostics from each valid LEO-III-STC source location. */ +export function createLeoIIITypeErrorDiagnostics( + document: vscode.TextDocument, + typeErrors: LeoIIITypeError[] +): vscode.Diagnostic[] { + const diagnostics: vscode.Diagnostic[] = []; + + for (const typeError of typeErrors) { + const lineIndex = typeError.line - 1; + if (lineIndex < 0 || lineIndex >= document.lineCount) { + continue; + } + + const line = document.lineAt(lineIndex); + const characterIndex = Math.min(typeError.character - 1, line.text.length); + const startPosition = line.range.start.with(undefined, characterIndex); + diagnostics.push({ + range: line.range.with(startPosition, line.range.end), + message: typeError.message, + severity: WARNING_DIAGNOSTIC_SEVERITY, + source: TYPE_CHECK_DIAGNOSTIC_SOURCE + }); + } + + return diagnostics; +} diff --git a/tptplus/client/test/systemB4TptpOutput.test.js b/tptplus/client/test/systemB4TptpOutput.test.js new file mode 100644 index 0000000..891c47a --- /dev/null +++ b/tptplus/client/test/systemB4TptpOutput.test.js @@ -0,0 +1,153 @@ +const test = require('node:test'); +const assert = require('node:assert/strict'); + +const { + getSzsOutput, + getSzsStatus, + getSzsStatusMessage +} = require('../out/systemB4TptpOutput'); + +test('getSzsStatus extracts a success status', () => { + const output = [ + '% [INFO] Parsing done.', + '% SZS status Success for problem : Type check succeeded' + ].join('\n'); + + assert.equal(getSzsStatus(output), 'Success'); +}); + +test('getSzsStatus extracts a type-error status', () => { + const output = + '% SZS status TypeError for problem : Problem is not well-typed'; + + assert.equal(getSzsStatus(output), 'TypeError'); +}); + +test('getSzsStatusMessage extracts all text after the first colon', () => { + const outputs = [ + [ + '% SZS status TypeError for /tmp/SwwGaHgmBe/SOT_Lh8QMt : Problem is not well-typed', + 'Problem is not well-typed' + ], + [ + "% SZS status SyntaxError for /tmp/N0V9SIj94_/SOT_BHhD5F : Parse error in file '/tmp/N0V9SIj94_/SOT_BHhD5F' in line 11:40. Unrecognized token '<~'", + "Parse error in file '/tmp/N0V9SIj94_/SOT_BHhD5F' in line 11:40. Unrecognized token '<~'" + ], + [ + "% SZS status SyntaxError for /tmp/lHM9ZFyxij/SOT_dlgIer : Parse error in file '/tmp/lHM9ZFyxij/SOT_dlgIer' in line 10:1. Expected DOT but read LOWERWORD 'tff'", + "Parse error in file '/tmp/lHM9ZFyxij/SOT_dlgIer' in line 10:1. Expected DOT but read LOWERWORD 'tff'" + ] + ]; + + for (const [output, expected] of outputs) { + assert.equal(getSzsStatusMessage(output), expected); + } +}); + +test('getSzsStatusMessage returns undefined when the status has no message', () => { + assert.equal(getSzsStatusMessage('% SZS status Success for problem'), undefined); +}); + +test('getSzsStatus returns undefined when there is no status line', () => { + assert.equal(getSzsStatus('% [INFO] Parsing done.'), undefined); +}); + +test('getSzsStatus ignores a status line within an SZS output block', () => { + const output = [ + '% START OF SYSTEM OUTPUT', + '% [INFO] \t Parsing problem /tmp/SwwGaHgmBe/SOT_Lh8QMt ...', + '% [INFO] \t Parsing done (133ms).', + '', + '% SZS output start LogicalData for /tmp/SwwGaHgmBe/SOT_Lh8QMt', + 'Illtyped formula distinct_cats in line 18:1.', + 'Illtyped formula jon_owns_garfields_lovers in line 29:5.', + '', + '% SZS status TypeError for /tmp/SwwGaHgmBe/SOT_Lh8QMt : Problem is not well-typed', + '', + '% SZS output end LogicalData for /tmp/SwwGaHgmBe/SOT_Lh8QMt', + '', + '% END OF SYSTEM OUTPUT' + ].join('\n'); + + assert.equal(getSzsStatus(output), undefined); +}); + +test('getSzsStatus extracts a status after an SZS output block', () => { + const output = [ + '% SZS output start LogicalData for problem', + '% SZS status TypeError for nested-output', + '% SZS output end LogicalData for problem', + '% SZS status Success for problem' + ].join('\r\n'); + + assert.equal(getSzsStatus(output), 'Success'); +}); + +test('getSzsOutput extracts multiline output and preserves blank lines', () => { + const output = [ + '% START OF SYSTEM OUTPUT', + '% SZS output start LogicalData for problem', + 'Test: multi-line output', + '', + 'Illtyped formula example in line 29:1.', + '% SZS output end LogicalData for problem', + '% END OF SYSTEM OUTPUT' + ].join('\n'); + + assert.equal( + getSzsOutput(output), + 'Test: multi-line output\n\nIlltyped formula example in line 29:1.' + ); +}); + +test('getSzsOutput extracts content between the outermost duplicated markers', () => { + const output = [ + '% SZS output start LogicalData for outer', + '% SZS output start LogicalData for inner', + 'Test: multi-line output', + '', + 'Illtyped formula example in line 29:1.', + '% SZS output end LogicalData for inner', + '% SZS output end LogicalData for outer' + ].join('\n'); + + const expected = [ + '% SZS output start LogicalData for inner', + 'Test: multi-line output', + '', + 'Illtyped formula example in line 29:1.', + '% SZS output end LogicalData for inner' + ].join('\n'); + + assert.equal(getSzsOutput(output), expected); +}); + +test('getSzsOutput supports CRLF line endings', () => { + const output = [ + '% SZS output start LogicalData for problem', + 'First line', + '', + 'Second line', + '% SZS output end LogicalData for problem' + ].join('\r\n'); + + assert.equal(getSzsOutput(output), 'First line\r\n\r\nSecond line'); +}); + +test('getSzsOutput returns undefined when the start marker is missing', () => { + const output = [ + 'Illtyped formula example in line 29:1.', + '% SZS output end LogicalData for problem' + ].join('\n'); + + assert.equal(getSzsOutput(output), undefined); +}); + +test('getSzsOutput returns undefined when the end marker is missing', () => { + const output = [ + '% SZS output start LogicalData for problem', + 'Illtyped formula example in line 29:1.' + ].join('\n'); + + assert.equal(getSzsOutput(output), undefined); +}); diff --git a/tptplus/client/test/typeCheckErrors.test.js b/tptplus/client/test/typeCheckErrors.test.js new file mode 100644 index 0000000..bed9cf1 --- /dev/null +++ b/tptplus/client/test/typeCheckErrors.test.js @@ -0,0 +1,37 @@ +const test = require('node:test'); +const assert = require('node:assert/strict'); + +const { getLeoIIITypeErrors } = require('../out/typeCheck/errors'); + +test('getLeoIIITypeErrors extracts every reported formula and location', () => { + const output = [ + 'Illtyped formula first_formula in line 29:1.', + 'Some unrelated output.', + 'Illtyped formula \'formula with spaces\' in line 42:17.' + ].join('\n'); + + assert.deepEqual(getLeoIIITypeErrors(output), [ + { + formulaName: 'first_formula', + line: 29, + character: 1, + message: 'Illtyped formula first_formula in line 29:1.' + }, + { + formulaName: "'formula with spaces'", + line: 42, + character: 17, + message: "Illtyped formula 'formula with spaces' in line 42:17." + } + ]); +}); + +test('getLeoIIITypeErrors ignores malformed and non-positive locations', () => { + const output = [ + 'Illtyped formula missing_period in line 3:4', + 'Illtyped formula zero_line in line 0:4.', + 'Illtyped formula zero_character in line 3:0.' + ].join('\n'); + + assert.deepEqual(getLeoIIITypeErrors(output), []); +}); diff --git a/tptplus/package.json b/tptplus/package.json index 4ca0159..188a0b7 100644 --- a/tptplus/package.json +++ b/tptplus/package.json @@ -59,6 +59,15 @@ "dark": "./images/icons/PrettyPrint.png" } }, + { + "command": "tptp.typeCheck", + "title": "TPTP: Type-Check with LEO-III", + "enablement": "!tptp.typeCheckRunning", + "icon": { + "light": "./images/icons/Type.png", + "dark": "./images/icons/Type.png" + } + }, { "command": "tptp.proveProblem", "title": "TPTP: Prove Problem" @@ -89,7 +98,12 @@ { "command": "tptp.prettyPrint", "when": "editorLangId == tptp", - "group": "navigation" + "group": "navigation@1" + }, + { + "command": "tptp.typeCheck", + "when": "editorLangId == tptp", + "group": "navigation@2" } ], "editor/context": [ @@ -163,6 +177,8 @@ "compile": "tsc -b", "watch": "tsc -b -w", "postinstall": "cd client && npm install && cd ../server && npm install && cd ..", + "pretest:unit": "npm run compile", + "test:unit": "node --test client/test/*.test.js", "test": "sh ./scripts/e2e.sh" }, "devDependencies": { From 498f6912d8f2c31c0a083560f766b95d5e6ccebc Mon Sep 17 00:00:00 2001 From: jzxia Date: Mon, 20 Jul 2026 22:05:32 +0800 Subject: [PATCH 2/7] feat(type-checker): discard unhelpful error messages returned by LEO-III-STC: temporary file names and generic "Problem is not well-typed" --- tptplus/client/src/typeCheck/command.ts | 8 ++++++-- tptplus/client/src/typeCheck/errors.ts | 22 +++++++++++++++++++++ tptplus/client/test/typeCheckErrors.test.js | 22 ++++++++++++++++++++- 3 files changed, 49 insertions(+), 3 deletions(-) diff --git a/tptplus/client/src/typeCheck/command.ts b/tptplus/client/src/typeCheck/command.ts index 9165489..6e529cc 100644 --- a/tptplus/client/src/typeCheck/command.ts +++ b/tptplus/client/src/typeCheck/command.ts @@ -9,6 +9,7 @@ import { } from '../systemB4TptpOutput'; import { createLeoIIITypeErrorDiagnostics, + formatTypeCheckStatusMessage, getLeoIIITypeErrors } from './errors'; @@ -74,7 +75,10 @@ export function registerTypeCheckCommand(): vscode.Disposable { const output = await response.text(); const status = getSzsStatus(output); - const statusMessage = getSzsStatusMessage(output); + const statusMessage = formatTypeCheckStatusMessage( + status, + getSzsStatusMessage(output) + ); const szsOutput = getSzsOutput(output); const outputSuffix = [statusMessage, szsOutput] .filter((message): message is string => Boolean(message)) // discard '' or undefined @@ -90,7 +94,7 @@ export function registerTypeCheckCommand(): vscode.Disposable { createLeoIIITypeErrorDiagnostics(document, typeErrors) ); vscode.window.showErrorMessage( - `LEO-III-STC found type error(s).${szsOutput ? `\n${szsOutput}` : ''}` + `LEO-III-STC found type error(s).${outputSuffix}` ); } else { vscode.window.showErrorMessage( diff --git a/tptplus/client/src/typeCheck/errors.ts b/tptplus/client/src/typeCheck/errors.ts index be445bf..95bfaf5 100644 --- a/tptplus/client/src/typeCheck/errors.ts +++ b/tptplus/client/src/typeCheck/errors.ts @@ -14,6 +14,28 @@ export interface LeoIIITypeError { message: string; } +/** Formats an SZS status message for display in a type-check toaster. */ +export function formatTypeCheckStatusMessage( + status: string | undefined, + message: string | undefined +): string | undefined { + if (status === 'TypeError') { + // Discard the generic "Problem is not well-typed" message. The detailed + // ill-typed formula messages from the SZS output are displayed instead. + return ''; + } + + if (status === 'SyntaxError') { + // Discard temporary file name + return message?.replace( + /^Parse error in file '[^\r\n]*' in line (?=\d+:\d+)/, + 'Parse error in line ' + ); + } + + return message; +} + /** Extracts every source-located type error reported by LEO-III-STC. */ export function getLeoIIITypeErrors(output: string): LeoIIITypeError[] { const typeErrors: LeoIIITypeError[] = []; diff --git a/tptplus/client/test/typeCheckErrors.test.js b/tptplus/client/test/typeCheckErrors.test.js index bed9cf1..85279fd 100644 --- a/tptplus/client/test/typeCheckErrors.test.js +++ b/tptplus/client/test/typeCheckErrors.test.js @@ -1,7 +1,27 @@ const test = require('node:test'); const assert = require('node:assert/strict'); -const { getLeoIIITypeErrors } = require('../out/typeCheck/errors'); +const { + formatTypeCheckStatusMessage, + getLeoIIITypeErrors +} = require('../out/typeCheck/errors'); + +test('formatTypeCheckStatusMessage removes the temporary file from syntax errors', () => { + const message = + "Parse error in file '/tmp/9wGGhEopjp/SOT_zt320r' in line 14:5. Expected COMMA but read LOWERWORD 'f'"; + + assert.equal( + formatTypeCheckStatusMessage('SyntaxError', message), + "Parse error in line 14:5. Expected COMMA but read LOWERWORD 'f'" + ); +}); + +test('formatTypeCheckStatusMessage discards the generic type-error message', () => { + assert.equal( + formatTypeCheckStatusMessage('TypeError', 'Problem is not well-typed'), + '' + ); +}); test('getLeoIIITypeErrors extracts every reported formula and location', () => { const output = [ From 8975b2f238b8652906901f68d5f8e344c0b9fb0d Mon Sep 17 00:00:00 2001 From: jzxia Date: Mon, 20 Jul 2026 22:28:14 +0800 Subject: [PATCH 3/7] fix(systemB4TptpOutput): extract SZS status before an SZS output block --- tptplus/client/src/systemB4TptpOutput.ts | 4 ++-- tptplus/client/test/systemB4TptpOutput.test.js | 11 ----------- 2 files changed, 2 insertions(+), 13 deletions(-) diff --git a/tptplus/client/src/systemB4TptpOutput.ts b/tptplus/client/src/systemB4TptpOutput.ts index 3839804..02d1b28 100644 --- a/tptplus/client/src/systemB4TptpOutput.ts +++ b/tptplus/client/src/systemB4TptpOutput.ts @@ -41,7 +41,7 @@ export function lastNonemptyLine(text: string): string | undefined { return undefined; } -/** Finds an SZS status line outside an SZS output block. */ +/** Finds an SZS status line before an SZS output block. */ function getSzsStatusLine(output: string): string | undefined { for (const line of output.split(/\r?\n/)) { if (/^% SZS output start \S+/.test(line)) { @@ -55,7 +55,7 @@ function getSzsStatusLine(output: string): string | undefined { return undefined; } -/** Extracts the status name from an SZS status line outside an SZS output block. */ +/** Extracts the status name from an SZS status line before an SZS output block. */ export function getSzsStatus(output: string): string | undefined { return getSzsStatusLine(output)?.match(/^% SZS status (\S+)/)?.[1]; } diff --git a/tptplus/client/test/systemB4TptpOutput.test.js b/tptplus/client/test/systemB4TptpOutput.test.js index 891c47a..a1554da 100644 --- a/tptplus/client/test/systemB4TptpOutput.test.js +++ b/tptplus/client/test/systemB4TptpOutput.test.js @@ -72,17 +72,6 @@ test('getSzsStatus ignores a status line within an SZS output block', () => { assert.equal(getSzsStatus(output), undefined); }); -test('getSzsStatus extracts a status after an SZS output block', () => { - const output = [ - '% SZS output start LogicalData for problem', - '% SZS status TypeError for nested-output', - '% SZS output end LogicalData for problem', - '% SZS status Success for problem' - ].join('\r\n'); - - assert.equal(getSzsStatus(output), 'Success'); -}); - test('getSzsOutput extracts multiline output and preserves blank lines', () => { const output = [ '% START OF SYSTEM OUTPUT', From 02dc51397f27f1a43f0eb8bf81d59934725bbd25 Mon Sep 17 00:00:00 2001 From: jzxia Date: Mon, 20 Jul 2026 22:31:34 +0800 Subject: [PATCH 4/7] fix(type-checker): check document freshness before handling any response status --- tptplus/client/src/typeCheck/command.ts | 29 +++++++++++++------------ 1 file changed, 15 insertions(+), 14 deletions(-) diff --git a/tptplus/client/src/typeCheck/command.ts b/tptplus/client/src/typeCheck/command.ts index 6e529cc..ea62f34 100644 --- a/tptplus/client/src/typeCheck/command.ts +++ b/tptplus/client/src/typeCheck/command.ts @@ -74,6 +74,13 @@ export function registerTypeCheckCommand(): vscode.Disposable { } const output = await response.text(); + if (document.version !== checkedDocumentVersion) { + vscode.window.showErrorMessage( + 'TPTP file changed while type-checking. Please run the type-checker again.' + ); + return; + } + const status = getSzsStatus(output); const statusMessage = formatTypeCheckStatusMessage( status, @@ -87,20 +94,14 @@ export function registerTypeCheckCommand(): vscode.Disposable { if (status === 'Success') { vscode.window.showInformationMessage(`LEO-III-STC type check succeeded.`); } else if (status === 'TypeError') { - if (document.version === checkedDocumentVersion) { - const typeErrors = getLeoIIITypeErrors(szsOutput ?? output); - diagnostics.set( - document.uri, - createLeoIIITypeErrorDiagnostics(document, typeErrors) - ); - vscode.window.showErrorMessage( - `LEO-III-STC found type error(s).${outputSuffix}` - ); - } else { - vscode.window.showErrorMessage( - `TPTP file changed while type-checking. Please run the type-checker again.` - ); - } + const typeErrors = getLeoIIITypeErrors(szsOutput ?? output); + diagnostics.set( + document.uri, + createLeoIIITypeErrorDiagnostics(document, typeErrors) + ); + vscode.window.showErrorMessage( + `LEO-III-STC found type error(s).${outputSuffix}` + ); } else if (status) { vscode.window.showErrorMessage(`LEO-III-STC reported ${status}.${outputSuffix}`); } else { From 4587bfd840ec38cda4a21cdbc06000ce19aefc6d Mon Sep 17 00:00:00 2001 From: jzxia Date: Mon, 20 Jul 2026 23:14:54 +0800 Subject: [PATCH 5/7] feat(type-checker): add cancellable request progress --- tptplus/client/src/typeCheck/command.ts | 82 ++++++++++++++++++++++--- 1 file changed, 72 insertions(+), 10 deletions(-) diff --git a/tptplus/client/src/typeCheck/command.ts b/tptplus/client/src/typeCheck/command.ts index ea62f34..971008f 100644 --- a/tptplus/client/src/typeCheck/command.ts +++ b/tptplus/client/src/typeCheck/command.ts @@ -16,6 +16,8 @@ import { const SYSTEM_ON_TPTP_URL = 'https://tptp.org/cgi-bin/SystemOnTPTPFormReply'; const LEO_III_STC = 'Leo-III-STC---'; // SystemB4TPTP will automatically run the latest version of LEO-III-STC it has available const TYPE_CHECK_RUNNING_CONTEXT_KEY = 'tptp.typeCheckRunning'; +const TYPE_CHECK_TIMEOUT_SEC = 60; // TODO: make this configurable +const TYPE_CHECK_REQUEST_TIMEOUT_MS = 75000; // TODO: make this configurable function createLeoIIITypeCheckForm(document: vscode.TextDocument): FormData { const form = new FormData(); @@ -27,7 +29,7 @@ function createLeoIIITypeCheckForm(document: vscode.TextDocument): FormData { form.append('X2TPTP', ''); form.append('ProblemSource', 'UPLOAD'); form.append(`System___${LEO_III_STC}`, LEO_III_STC); - form.append(`TimeLimit___${LEO_III_STC}`, '60'); + form.append(`TimeLimit___${LEO_III_STC}`, String(TYPE_CHECK_TIMEOUT_SEC)); form.append( 'UPLOADProblem', new Blob([document.getText()], { type: 'text/plain' }), @@ -37,6 +39,71 @@ function createLeoIIITypeCheckForm(document: vscode.TextDocument): FormData { return form; } +/** + * Runs the complete remote request with visible progress, cancellation, and a timeout. + * + * @returns The response body for a successful request, or `undefined` when the user + * cancels the operation. User cancellation is therefore an expected outcome rather + * than an error. + * @throws An error when the request times out, returns a non-successful HTTP status, + * encounters a network failure, or fails while reading the response body. + */ +async function requestLeoIIITypeCheck( + document: vscode.TextDocument +): Promise { + return vscode.window.withProgress( + { + location: vscode.ProgressLocation.Notification, + title: 'Type-checking with LEO-III-STC', + cancellable: true + }, + async (progress, token) => { + const controller = new AbortController(); + let timedOut = false; + + progress.report({ message: 'Waiting for tptp.org...' }); + const cancellation = token.onCancellationRequested(() => { + controller.abort(); + }); + const timeout = setTimeout(() => { + timedOut = true; + controller.abort(); + }, TYPE_CHECK_REQUEST_TIMEOUT_MS); + + try { + const response = await fetch(SYSTEM_ON_TPTP_URL, { + method: 'POST', + body: createLeoIIITypeCheckForm(document), + signal: controller.signal + }); + + if (token.isCancellationRequested) { + return undefined; + } + if (!response.ok) { + throw new Error(`HTTP ${response.status}: ${response.statusText || 'request failed'}`); + } + + const output = await response.text(); + return token.isCancellationRequested ? undefined : output; + } catch (error: unknown) { + if (token.isCancellationRequested) { + return undefined; + } + if (timedOut) { + throw new Error( + `LEO-III-STC type check timed out after ${TYPE_CHECK_REQUEST_TIMEOUT_MS / 1000} seconds.` + ); + } + throw error; + } finally { + clearTimeout(timeout); + cancellation.dispose(); + } + } + ); +} + /** Registers the command that asks LEO-III-STC on SystemB4TPTP to type-check a TPTP document. */ export function registerTypeCheckCommand(): vscode.Disposable { let typeCheckRunning = false; @@ -64,16 +131,11 @@ export function registerTypeCheckCommand(): vscode.Disposable { const document = await vscode.workspace.openTextDocument(uri); const checkedDocumentVersion = document.version; diagnostics.delete(document.uri); - const response = await fetch(SYSTEM_ON_TPTP_URL, { - method: 'POST', - body: createLeoIIITypeCheckForm(document) - }); - - if (!response.ok) { - throw new Error(`HTTP ${response.status}: ${response.statusText || 'request failed'}`); + const output = await requestLeoIIITypeCheck(document); + if (output === undefined) { + vscode.window.showInformationMessage('LEO-III-STC type check cancelled.'); + return; } - - const output = await response.text(); if (document.version !== checkedDocumentVersion) { vscode.window.showErrorMessage( 'TPTP file changed while type-checking. Please run the type-checker again.' From 52554e7f38893a3c7497df06f7c4adce454e1621 Mon Sep 17 00:00:00 2001 From: jzxia Date: Tue, 21 Jul 2026 00:02:55 +0800 Subject: [PATCH 6/7] publish v0.1.12 --- README.md | 6 +++++- tptplus/CHANGELOG.md | 3 ++- tptplus/README.md | 6 +++++- tptplus/package-lock.json | 4 ++-- tptplus/package.json | 2 +- 5 files changed, 15 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index bfd5baa..d8df216 100644 --- a/README.md +++ b/README.md @@ -167,7 +167,11 @@ Added error handling for "Format TPTP File": display error message and jump to p ### 0.1.11 -Added title-menu button for "TPTP: Check Syntax and Format TPTP File"; improved error handling for pretty-printer. +Added title-menu button for "TPTP: Pretty-Print TPTP File"; improved error handling for pretty-printer. + +### 0.1.12 + +Added title-menu button for "TPTP: Type-Check with LEO-III"; improved error handling for pretty-printer; retired legacy formatter. --- diff --git a/tptplus/CHANGELOG.md b/tptplus/CHANGELOG.md index 59c6fc9..b049fa6 100644 --- a/tptplus/CHANGELOG.md +++ b/tptplus/CHANGELOG.md @@ -23,4 +23,5 @@ - v0.1.8 Fixed issue where some greater-than-signs are not handled correctly by command "Format TPTP File". - v0.1.9 Added local pretty-printer so that "Format TPTP File" works without Internet connection. The original remote pretty-printer is kept as a fallback. - v0.1.10 Added error handling for "Format TPTP File": display error message and jump to position of syntax error. -- v0.1.11 Added title-menu button for "TPTP: Check Syntax and Format TPTP File"; improved error handling for pretty-printer. +- v0.1.11 Added title-menu button for "TPTP: Pretty-Print TPTP File"; improved error handling for pretty-printer. +- v0.1.12 Added title-menu button for "TPTP: Type-Check with LEO-III"; improved error handling for pretty-printer; retired legacy formatter. diff --git a/tptplus/README.md b/tptplus/README.md index 20feff2..256e0c8 100644 --- a/tptplus/README.md +++ b/tptplus/README.md @@ -166,7 +166,11 @@ Added error handling for "Format TPTP File": display error message and jump to p ### 0.1.11 -Added title-menu button for "TPTP: Check Syntax and Format TPTP File"; improved error handling for pretty-printer. +Added title-menu button for "TPTP: Pretty-Print TPTP File"; improved error handling for pretty-printer. + +### 0.1.12 + +Added title-menu button for "TPTP: Type-Check with LEO-III"; improved error handling for pretty-printer; retired legacy formatter. --- diff --git a/tptplus/package-lock.json b/tptplus/package-lock.json index e895acd..eb5dcda 100644 --- a/tptplus/package-lock.json +++ b/tptplus/package-lock.json @@ -1,12 +1,12 @@ { "name": "tptp", - "version": "0.1.11", + "version": "0.1.12", "lockfileVersion": 3, "requires": true, "packages": { "": { "name": "tptp", - "version": "0.1.11", + "version": "0.1.12", "hasInstallScript": true, "devDependencies": { "@types/node": "^16.18.34", diff --git a/tptplus/package.json b/tptplus/package.json index a7351fd..85441dc 100644 --- a/tptplus/package.json +++ b/tptplus/package.json @@ -3,7 +3,7 @@ "displayName": "TPTP", "publisher": "TPTPWorld", "description": "Syntax highlighting, error detection, pretty-printing, and proving & processing theorems functions for TPTP language", - "version": "0.1.11", + "version": "0.1.12", "icon": "images/icons/TPTPWorld.png", "repository": { "type": "git", From 0786fb165206855d482668195cf469d187833d4c Mon Sep 17 00:00:00 2001 From: jzxia Date: Tue, 21 Jul 2026 15:55:58 +0800 Subject: [PATCH 7/7] feat(type-checker): move editor cursor to the first type error when LEO-III-STC returns type error(s) --- tptplus/client/src/typeCheck/command.ts | 12 +++-- tptplus/client/src/typeCheck/diagnostics.ts | 52 +++++++++++++++++++++ tptplus/client/src/typeCheck/errors.ts | 34 -------------- 3 files changed, 59 insertions(+), 39 deletions(-) create mode 100644 tptplus/client/src/typeCheck/diagnostics.ts diff --git a/tptplus/client/src/typeCheck/command.ts b/tptplus/client/src/typeCheck/command.ts index 971008f..e817b46 100644 --- a/tptplus/client/src/typeCheck/command.ts +++ b/tptplus/client/src/typeCheck/command.ts @@ -8,10 +8,13 @@ import { getSzsStatusMessage } from '../systemB4TptpOutput'; import { - createLeoIIITypeErrorDiagnostics, formatTypeCheckStatusMessage, getLeoIIITypeErrors } from './errors'; +import { + createLeoIIITypeErrorDiagnostics, + revealFirstTypeError +} from './diagnostics'; const SYSTEM_ON_TPTP_URL = 'https://tptp.org/cgi-bin/SystemOnTPTPFormReply'; const LEO_III_STC = 'Leo-III-STC---'; // SystemB4TPTP will automatically run the latest version of LEO-III-STC it has available @@ -157,10 +160,9 @@ export function registerTypeCheckCommand(): vscode.Disposable { vscode.window.showInformationMessage(`LEO-III-STC type check succeeded.`); } else if (status === 'TypeError') { const typeErrors = getLeoIIITypeErrors(szsOutput ?? output); - diagnostics.set( - document.uri, - createLeoIIITypeErrorDiagnostics(document, typeErrors) - ); + const typeErrorDiagnostics = createLeoIIITypeErrorDiagnostics(document, typeErrors); + diagnostics.set(document.uri, typeErrorDiagnostics); + await revealFirstTypeError(document, typeErrorDiagnostics); vscode.window.showErrorMessage( `LEO-III-STC found type error(s).${outputSuffix}` ); diff --git a/tptplus/client/src/typeCheck/diagnostics.ts b/tptplus/client/src/typeCheck/diagnostics.ts new file mode 100644 index 0000000..c89c1a2 --- /dev/null +++ b/tptplus/client/src/typeCheck/diagnostics.ts @@ -0,0 +1,52 @@ +import * as vscode from 'vscode'; + +import type { LeoIIITypeError } from './errors'; + +const TYPE_CHECK_DIAGNOSTIC_SOURCE = 'LEO-III-STC type checker'; + +/** Creates warning diagnostic from each LEO-III-STC type error. */ +export function createLeoIIITypeErrorDiagnostics( + document: vscode.TextDocument, + typeErrors: LeoIIITypeError[] +): vscode.Diagnostic[] { + const diagnostics: vscode.Diagnostic[] = []; + + for (const typeError of typeErrors) { + const lineIndex = typeError.line - 1; + if (lineIndex < 0 || lineIndex >= document.lineCount) { + continue; + } + + const line = document.lineAt(lineIndex); + const characterIndex = Math.min(typeError.character - 1, line.text.length); + const startPosition = line.range.start.with(undefined, characterIndex); + diagnostics.push({ + range: line.range.with(startPosition, line.range.end), + message: typeError.message, + severity: vscode.DiagnosticSeverity.Warning, + source: TYPE_CHECK_DIAGNOSTIC_SOURCE + }); + } + + return diagnostics; +} + +/** Moves the editor cursor to the first source-located type error. */ +export async function revealFirstTypeError( + document: vscode.TextDocument, + typeErrorDiagnostics: readonly vscode.Diagnostic[] +): Promise { + const firstTypeError = typeErrorDiagnostics[0]; + if (!firstTypeError) { + return; + } + + const position = firstTypeError.range.start; + const range = new vscode.Range(position, position); + const editor = await vscode.window.showTextDocument(document, { + preview: false, + selection: range + }); + editor.selection = new vscode.Selection(position, position); + editor.revealRange(range, vscode.TextEditorRevealType.InCenterIfOutsideViewport); +} diff --git a/tptplus/client/src/typeCheck/errors.ts b/tptplus/client/src/typeCheck/errors.ts index 95bfaf5..5d65aa4 100644 --- a/tptplus/client/src/typeCheck/errors.ts +++ b/tptplus/client/src/typeCheck/errors.ts @@ -1,10 +1,3 @@ -import type * as vscode from 'vscode'; - -const TYPE_CHECK_DIAGNOSTIC_SOURCE = 'LEO-III-STC type checker'; -// DiagnosticSeverity.Warning is 1 in the VS Code API. Keeping this module's -// VS Code dependency type-only also makes the error parser independently testable. -const WARNING_DIAGNOSTIC_SEVERITY: vscode.DiagnosticSeverity = 1; - export interface LeoIIITypeError { formulaName: string; /** One-based source line reported by LEO-III-STC. */ @@ -52,30 +45,3 @@ export function getLeoIIITypeErrors(output: string): LeoIIITypeError[] { return typeErrors; } - -/** Creates warning diagnostics from each valid LEO-III-STC source location. */ -export function createLeoIIITypeErrorDiagnostics( - document: vscode.TextDocument, - typeErrors: LeoIIITypeError[] -): vscode.Diagnostic[] { - const diagnostics: vscode.Diagnostic[] = []; - - for (const typeError of typeErrors) { - const lineIndex = typeError.line - 1; - if (lineIndex < 0 || lineIndex >= document.lineCount) { - continue; - } - - const line = document.lineAt(lineIndex); - const characterIndex = Math.min(typeError.character - 1, line.text.length); - const startPosition = line.range.start.with(undefined, characterIndex); - diagnostics.push({ - range: line.range.with(startPosition, line.range.end), - message: typeError.message, - severity: WARNING_DIAGNOSTIC_SEVERITY, - source: TYPE_CHECK_DIAGNOSTIC_SOURCE - }); - } - - return diagnostics; -}