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/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..02d1b28 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 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)) { + return undefined; + } + if (/^% SZS status \S+/.test(line)) { + return line; + } + } + + return undefined; +} + +/** 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]; +} + +/** 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..e817b46 --- /dev/null +++ b/tptplus/client/src/typeCheck/command.ts @@ -0,0 +1,191 @@ +import * as path from 'path'; +import * as vscode from 'vscode'; + +import { errorMessage } from '../errorMessage'; +import { + getSzsOutput, + getSzsStatus, + getSzsStatusMessage +} from '../systemB4TptpOutput'; +import { + 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 +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(); + + // 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}`, String(TYPE_CHECK_TIMEOUT_SEC)); + form.append( + 'UPLOADProblem', + new Blob([document.getText()], { type: 'text/plain' }), + path.basename(document.fileName) || 'problem.p' + ); + + 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; + + 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 output = await requestLeoIIITypeCheck(document); + if (output === undefined) { + vscode.window.showInformationMessage('LEO-III-STC type check cancelled.'); + return; + } + 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, + 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') { + const typeErrors = getLeoIIITypeErrors(szsOutput ?? output); + 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}` + ); + } 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/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 new file mode 100644 index 0000000..5d65aa4 --- /dev/null +++ b/tptplus/client/src/typeCheck/errors.ts @@ -0,0 +1,47 @@ +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; +} + +/** 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[] = []; + 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; +} diff --git a/tptplus/client/test/systemB4TptpOutput.test.js b/tptplus/client/test/systemB4TptpOutput.test.js new file mode 100644 index 0000000..a1554da --- /dev/null +++ b/tptplus/client/test/systemB4TptpOutput.test.js @@ -0,0 +1,142 @@ +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('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..85279fd --- /dev/null +++ b/tptplus/client/test/typeCheckErrors.test.js @@ -0,0 +1,57 @@ +const test = require('node:test'); +const assert = require('node:assert/strict'); + +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 = [ + '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-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 ea11ee8..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", @@ -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": [ @@ -162,7 +176,9 @@ "vscode:prepublish": "npm run compile", "compile": "tsc -b", "watch": "tsc -b -w", - "postinstall": "cd client && npm install && cd ../server && npm install && cd .." + "postinstall": "cd client && npm install && cd ../server && npm install && cd ..", + "pretest:unit": "npm run compile", + "test:unit": "node --test client/test/*.test.js" }, "devDependencies": { "@types/node": "^16.18.34",