lean3_server_file_sync_and_tactic_state_query.ts

1import * as child_process from 'child_process';
2import { ProcessTransport, Connection } from '@leanprover/lean-client-js-node';
3
4async function main() {
5    // 1. Setup the transport to the local lean executable
6    // Ensure 'lean' is in your PATH
7    const transport = new ProcessTransport('lean', '.', []);
8    const conn = new Connection(transport);
9
10    // 2. Start the process
11    conn.connect();
12
13    const testFile = 'test.lean';
14    const content = 'theorem test (n : ℕ) : n + 0 = n := by reflexivity';
15
16    // 3. Sync the file content with the Lean server
17    await conn.sync(testFile, content);
18
19    // 4. Request info (like tactic state) at a specific position (line 1, column 40)
20    const info = await conn.info(testFile, 1, 40);
21
22    if (info.record && info.record.state) {
23        console.log('Tactic State at cursor:');
24        console.log(info.record.state);
25    } else {
26        console.log('No state found at this position.');
27    }
28
29    // 5. Clean up
30    transport.close();
31}
32
33main().catch(err => console.error(err));