Skip to content

Commit 0c78f9f

Browse files
FedericoPonziFedericoPonzi
authored
Add tlaplus-formatter support (#327)
Add tlaplus-formatter support Signed-off-by: Federico Ponzi <me@fponzi.me>
1 parent 2413a13 commit 0c78f9f

File tree

6 files changed

+334
-0
lines changed

6 files changed

+334
-0
lines changed

‎.github/workflows/release.yml‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -37,6 +37,8 @@ jobs:
3737
run: wget https://github.com/tlaplus/tlaplus/releases/download/v1.8.0/tla2tools.jar -O tools/tla2tools.jar
3838
- name: Get (latest) CommunityModules
3939
run: wget https://github.com/tlaplus/CommunityModules/releases/latest/download/CommunityModules-deps.jar -O tools/CommunityModules-deps.jar
40+
- name: Get (latest) TLA+ Formatter
41+
run: wget https://github.com/FedericoPonzi/tlaplus-formatter/releases/latest/download/tlaplus-formatter.jar -O tools/tlaplus-formatter.jar
4042
- name: Prepare Release
4143
run: |
4244
## Create a git commit to use its date as the extension's version number below.

‎package.json‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -672,6 +672,12 @@
672672
"default": true,
673673
"description": "Mark proof step states using whole line."
674674
},
675+
"tlaplus.formatter.enabled": {
676+
"type": "boolean",
677+
"scope": "window",
678+
"default": true,
679+
"markdownDescription": "Enable the TLA+ document formatter. [More info](https://github.com/FedericoPonzi/tlaplus-formatter/)"
680+
},
675681
"tlaplus.moduleSearchPaths": {
676682
"type": "array",
677683
"items": {

‎src/formatters/tlaFormatter.ts‎

Lines changed: 147 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,147 @@
1+
import * as vscode from 'vscode';
2+
import * as path from 'path';
3+
import * as fs from 'fs';
4+
import { createHash } from 'crypto';
5+
import { spawn } from 'child_process';
6+
import { getJavaPath } from '../tla2tools';
7+
import { moduleSearchPaths } from '../paths';
8+
9+
const CFG_FORMATTER_ENABLED = 'tlaplus.formatter.enabled';
10+
const FORMATTER_JAR_NAME = 'tlaplus-formatter.jar';
11+
12+
/**
13+
* Builds `-DTLA-Library=...` with all module search paths (user-configured,
14+
* TLC standard/community modules, TLAPS) so the formatter's SANY can resolve
15+
* any EXTENDS'd modules. Paths using the `jarfile:` scheme are dropped because
16+
* Java's SANY resolves those from its own classpath.
17+
*/
18+
function makeFormatterTlaLibraryOpt(documentDir?: string): string {
19+
const allPaths: string[] = [];
20+
if (documentDir) {
21+
allPaths.push(documentDir);
22+
}
23+
for (const source of moduleSearchPaths.getSources()) {
24+
const sourcePaths = moduleSearchPaths.getSourcePaths(source.name);
25+
if (sourcePaths) {
26+
allPaths.push(...sourcePaths);
27+
}
28+
}
29+
const fsPaths = allPaths.filter(p => !p.startsWith('jar:') && !p.startsWith('jarfile:'));
30+
return '-DTLA-Library=' + fsPaths.join(path.delimiter);
31+
}
32+
33+
export function extractModuleName(text: string): string | null {
34+
const regex = /^-{4,}\s*MODULE\s+(\w+)/m;
35+
const match = regex.exec(text);
36+
if (match && match[1]) {
37+
return match[1];
38+
}
39+
return null;
40+
}
41+
42+
function generateHash(input: string, algorithm: string): string {
43+
const hash = createHash(algorithm);
44+
hash.update(input);
45+
return hash.digest('hex');
46+
}
47+
48+
export function registerDocumentFormatter(context: vscode.ExtensionContext): void {
49+
const formatterJarPath = path.join(context.extensionPath, 'tools', FORMATTER_JAR_NAME);
50+
51+
context.subscriptions.push(
52+
vscode.languages.registerDocumentFormattingEditProvider('tlaplus', {
53+
provideDocumentFormattingEdits(
54+
document: vscode.TextDocument
55+
): vscode.ProviderResult<vscode.TextEdit[]> {
56+
const enabled = vscode.workspace.getConfiguration().get<boolean>(CFG_FORMATTER_ENABLED, true);
57+
if (!enabled) {
58+
vscode.window.showInformationMessage(
59+
'TLA+ formatter is disabled. Enable it via the "tlaplus.formatter.enabled" setting.'
60+
);
61+
return [];
62+
}
63+
64+
return new Promise((resolve, reject) => {
65+
const inputText = document.getText();
66+
// The filename must match the module name for SANY to parse it.
67+
// Prefer the on-disk filename; fall back to parsing the header.
68+
const moduleName = (document.uri.scheme === 'file' && document.fileName.endsWith('.tla'))
69+
? path.basename(document.fileName, '.tla')
70+
: extractModuleName(inputText);
71+
if (!moduleName) {
72+
vscode.window.showErrorMessage('Could not extract module name from the document.');
73+
return resolve([]);
74+
}
75+
76+
// Create a unique temp folder based on content hash.
77+
const md5Hash = generateHash(inputText, 'md5');
78+
const tempDir = path.join(context.globalStorageUri.fsPath, md5Hash);
79+
80+
try {
81+
fs.mkdirSync(tempDir, { recursive: true });
82+
} catch (err) {
83+
if ((err as NodeJS.ErrnoException).code !== 'EEXIST') {
84+
return reject(err);
85+
}
86+
}
87+
88+
const tempInputPath = path.join(tempDir, moduleName + '.tla');
89+
const tempOutputPath = tempInputPath;
90+
fs.writeFileSync(tempInputPath, inputText);
91+
92+
// Add the document's directory to the TLA-Library path so
93+
// SANY can resolve EXTENDed modules relative to it.
94+
const documentDir = document.uri.scheme === 'file'
95+
? path.dirname(document.uri.fsPath)
96+
: undefined;
97+
98+
const javaPath = getJavaPath();
99+
const stderrChunks: string[] = [];
100+
const spawnArgs = [
101+
makeFormatterTlaLibraryOpt(documentDir),
102+
'-jar', formatterJarPath,
103+
'-v', 'ERROR',
104+
tempInputPath,
105+
tempOutputPath
106+
];
107+
const javaProcess = spawn(javaPath, spawnArgs, {
108+
cwd: documentDir
109+
});
110+
111+
javaProcess.stdout.on('data', (data) => {
112+
console.log(`Formatter STDOUT: ${data}`);
113+
});
114+
115+
javaProcess.stderr.on('data', (data) => {
116+
stderrChunks.push(data.toString());
117+
console.error(`Formatter STDERR: ${data}`);
118+
});
119+
120+
javaProcess.on('error', (error) => {
121+
vscode.window.showErrorMessage(`Formatter failed: ${error.message}`);
122+
reject(error);
123+
});
124+
125+
javaProcess.on('close', (code) => {
126+
if (code !== 0) {
127+
const stderr = stderrChunks.join('').trim();
128+
const msg = stderr
129+
? `Formatter error: ${stderr}`
130+
: `Formatter failed with exit code ${code}`;
131+
vscode.window.showErrorMessage(msg);
132+
fs.rmSync(tempDir, { recursive: true, force: true });
133+
return reject(new Error(msg));
134+
}
135+
const formattedText = fs.readFileSync(tempOutputPath, 'utf8');
136+
const edit = [vscode.TextEdit.replace(
137+
new vscode.Range(0, 0, document.lineCount, 0),
138+
formattedText
139+
)];
140+
fs.rmSync(tempDir, { recursive: true, force: true });
141+
resolve(edit);
142+
});
143+
});
144+
}
145+
})
146+
);
147+
}

‎src/main.ts‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@ import { exportModuleToTex, exportModuleToPdf, CMD_EXPORT_TLA_TO_TEX,
2020
CMD_EXPORT_TLA_TO_PDF } from './commands/exportModule';
2121
import { TlaOnTypeFormattingEditProvider } from './formatters/tla';
2222
import { CfgOnTypeFormattingEditProvider } from './formatters/cfg';
23+
import { registerDocumentFormatter } from './formatters/tlaFormatter';
2324
import { TlaCodeActionProvider } from './actions';
2425
import { TlaDocumentSymbolsProvider } from './symbols/tlaSymbols';
2526
import { LANG_TLAPLUS, LANG_TLAPLUS_CFG } from './common';
@@ -280,6 +281,8 @@ export async function activate(context: vscode.ExtensionContext): Promise<void>
280281
syncTlcStatisticsSetting()
281282
.catch((err) => console.error(err))
282283
.then(() => listenTlcStatConfigurationChanges(context.subscriptions));
284+
285+
registerDocumentFormatter(context);
283286
}
284287

285288
export function deactivate() {

‎tests/suite/formatters/tlaFormatter.test.ts‎

Lines changed: 176 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,176 @@
1+
import * as assert from 'assert';
2+
import * as vscode from 'vscode';
3+
import * as path from 'path';
4+
import * as fs from 'fs';
5+
import * as os from 'os';
6+
import { extractModuleName } from '../../../src/formatters/tlaFormatter';
7+
import { applyDocEdits, replaceDocContents } from '../document';
8+
9+
const UNFORMATTED =
10+
'This is some text explaining the spec.\n' +
11+
'---------------------- MODULE HourClock ----------------------\n' +
12+
'EXTENDS Naturals, TLC\n' +
13+
'VARIABLE hr\n' +
14+
'HCini == hr \\in (1 .. 12)\n' +
15+
'HCnxt == hr\' = IF hr # 12 THEN hr + 1 ELSE 1\n' +
16+
'HC == HCini /\\ [][HCnxt]_hr\n' +
17+
'--------------------------------------------------------------\n' +
18+
'THEOREM HC => []HCini\n' +
19+
'==============================================================\n' +
20+
'This is post text\n' +
21+
'Has multiple lines in it.\n';
22+
23+
const EXPECTED =
24+
'This is some text explaining the spec.\n' +
25+
'---------------------- MODULE HourClock ----------------------\n' +
26+
'EXTENDS Naturals, TLC\n' +
27+
'VARIABLE hr\n' +
28+
'HCini == hr \\in ( 1 .. 12 )\n' +
29+
'HCnxt == hr\' = IF hr # 12 THEN hr + 1 ELSE 1\n' +
30+
'HC == HCini /\\ [] [HCnxt]_hr\n' +
31+
'--------------------------------------------------------------\n' +
32+
'THEOREM HC => [] HCini\n' +
33+
'==============================================================\n' +
34+
'This is post text\n' +
35+
'Has multiple lines in it.\n';
36+
37+
async function formatDocument(doc: vscode.TextDocument): Promise<void> {
38+
const edits = await vscode.commands.executeCommand<vscode.TextEdit[]>(
39+
'vscode.executeFormatDocumentProvider',
40+
doc.uri,
41+
{ insertSpaces: true, tabSize: 4 } as vscode.FormattingOptions
42+
);
43+
assert.ok(edits && edits.length > 0, `Expected formatting edits but got ${edits ? edits.length : 'null'}`);
44+
await applyDocEdits(doc.uri, edits);
45+
}
46+
47+
suite('TLA+ Document Formatter Test Suite', () => {
48+
suite('extractModuleName', () => {
49+
test('Extracts module name from standard header', () => {
50+
const text = '---- MODULE MySpec ----\nVARIABLE x\n====';
51+
assert.strictEqual(extractModuleName(text), 'MySpec');
52+
});
53+
54+
test('Extracts module name with multiple dashes', () => {
55+
const text = '---------- MODULE TestModule ----------\n====';
56+
assert.strictEqual(extractModuleName(text), 'TestModule');
57+
});
58+
59+
test('Returns null for text without module declaration', () => {
60+
const text = 'VARIABLE x\nx == 1';
61+
assert.strictEqual(extractModuleName(text), null);
62+
});
63+
64+
test('Extracts module name with underscores', () => {
65+
const text = '---- MODULE My_Spec_V2 ----\n====';
66+
assert.strictEqual(extractModuleName(text), 'My_Spec_V2');
67+
});
68+
69+
test('Extracts first module name when multiple present', () => {
70+
const text = '---- MODULE First ----\n---- MODULE Second ----\n====';
71+
assert.strictEqual(extractModuleName(text), 'First');
72+
});
73+
74+
test('Ignores MODULE keyword in comments', () => {
75+
const text = '\\* Notes: MODULE Fake\n---- MODULE RealSpec ----\n====';
76+
assert.strictEqual(extractModuleName(text), 'RealSpec');
77+
});
78+
});
79+
80+
suite('Document formatting', () => {
81+
let tempDir: string;
82+
83+
suiteSetup(async () => {
84+
// Trigger extension activation by opening a tlaplus document.
85+
const doc = await vscode.workspace.openTextDocument({ language: 'tlaplus' });
86+
await vscode.window.showTextDocument(doc);
87+
await vscode.commands.executeCommand('workbench.action.closeActiveEditor');
88+
});
89+
90+
setup(() => {
91+
tempDir = fs.mkdtempSync(path.join(os.tmpdir(), 'tlaplus-fmt-test-'));
92+
});
93+
94+
teardown(async () => {
95+
await vscode.commands.executeCommand('workbench.action.closeActiveEditor');
96+
if (fs.existsSync(tempDir)) {
97+
fs.rmSync(tempDir, { recursive: true, force: true });
98+
}
99+
});
100+
101+
test('Formats a saved TLA+ file', async function() {
102+
const isWin = process.platform === 'win32';
103+
this.timeout(isWin ? 60000 : 30000);
104+
105+
const filePath = path.join(tempDir, 'HourClock.tla');
106+
fs.writeFileSync(filePath, UNFORMATTED, 'utf-8');
107+
108+
const doc = await vscode.workspace.openTextDocument(filePath);
109+
if (doc.languageId !== 'tlaplus') {
110+
await vscode.languages.setTextDocumentLanguage(doc, 'tlaplus');
111+
}
112+
await vscode.window.showTextDocument(doc);
113+
114+
await formatDocument(doc);
115+
assert.strictEqual(doc.getText(), EXPECTED);
116+
});
117+
118+
test('Formats an unsaved TLA+ document', async function() {
119+
const isWin = process.platform === 'win32';
120+
this.timeout(isWin ? 60000 : 30000);
121+
122+
const doc = await vscode.workspace.openTextDocument({ language: 'tlaplus', content: UNFORMATTED });
123+
await vscode.window.showTextDocument(doc);
124+
125+
await formatDocument(doc);
126+
assert.strictEqual(doc.getText(), EXPECTED);
127+
});
128+
129+
test('Formats unsaved buffer modifications of a saved file', async function() {
130+
const isWin = process.platform === 'win32';
131+
this.timeout(isWin ? 60000 : 30000);
132+
133+
// Save a minimal placeholder to disk.
134+
const filePath = path.join(tempDir, 'HourClock.tla');
135+
fs.writeFileSync(filePath, '---- MODULE HourClock ----\n====\n', 'utf-8');
136+
137+
const doc = await vscode.workspace.openTextDocument(filePath);
138+
if (doc.languageId !== 'tlaplus') {
139+
await vscode.languages.setTextDocumentLanguage(doc, 'tlaplus');
140+
}
141+
await vscode.window.showTextDocument(doc);
142+
143+
// Replace the buffer with unformatted content without saving.
144+
await replaceDocContents(doc, UNFORMATTED);
145+
assert.ok(doc.isDirty, 'Document should have unsaved changes');
146+
147+
await formatDocument(doc);
148+
assert.strictEqual(doc.getText(), EXPECTED);
149+
});
150+
151+
test('Does not format when formatter is disabled', async function() {
152+
const isWin = process.platform === 'win32';
153+
this.timeout(isWin ? 60000 : 30000);
154+
155+
const config = vscode.workspace.getConfiguration();
156+
await config.update('tlaplus.formatter.enabled', false, vscode.ConfigurationTarget.Global);
157+
158+
try {
159+
const doc = await vscode.workspace.openTextDocument({ language: 'tlaplus', content: UNFORMATTED });
160+
await vscode.window.showTextDocument(doc);
161+
162+
const edits = await vscode.commands.executeCommand<vscode.TextEdit[]>(
163+
'vscode.executeFormatDocumentProvider',
164+
doc.uri,
165+
{ insertSpaces: true, tabSize: 4 } as vscode.FormattingOptions
166+
);
167+
168+
const noEdits = !edits || edits.length === 0;
169+
assert.ok(noEdits, `Expected no edits when formatter is disabled but got ${edits?.length}`);
170+
assert.strictEqual(doc.getText(), UNFORMATTED, 'Document should remain unchanged');
171+
} finally {
172+
await config.update('tlaplus.formatter.enabled', undefined, vscode.ConfigurationTarget.Global);
173+
}
174+
});
175+
});
176+
});

‎tools/tlaplus-formatter.jar‎

5.57 MB
Binary file not shown.

0 commit comments

Comments
 (0)