288 lines
9.9 KiB
TypeScript
288 lines
9.9 KiB
TypeScript
/* The wiki's Lean session (client-side).
|
|
*
|
|
* One websocket to the lean4web server (`/websocket/<project>`), through
|
|
* which the wiki plays the part of a Lean editor's language client: open a
|
|
* document, send edits, ask for the goal at the cursor (the server's
|
|
* `$/lean/plainGoal`), and read the diagnostics — whose severity-3 entries
|
|
* are Lean's `#check`/`#eval` style messages, shown in the Messages pane.
|
|
*
|
|
* The session lives at module scope on purpose: the book may move the Lean
|
|
* page between its full-page and pane hosts (unmounting the editor), but a
|
|
* running Lean elaboration and its open document are expensive to restart —
|
|
* so they outlive the component, and the editor simply re-attaches. */
|
|
import { RpcSocket } from '~/utils/lean/lsp'
|
|
|
|
export type LeanPhase = 'idle' | 'connecting' | 'initializing' | 'ready' | 'lost'
|
|
|
|
export interface LeanInfoMessage { line: number, text: string }
|
|
|
|
/* the shape the Lean server publishes per diagnostic (a slice of LSP) */
|
|
export interface LeanDiagnostic {
|
|
range: { start: { line: number, character: number }, end: { line: number, character: number } }
|
|
severity?: number
|
|
message: string
|
|
source?: string
|
|
}
|
|
|
|
const DOCUMENT_NAME = 'Main.lean'
|
|
const FALLBACK_PROJECT = 'MathlibDemo'
|
|
|
|
interface LeanSession {
|
|
phase: Ref<LeanPhase>
|
|
goals: Ref<string[]>
|
|
messages: Ref<LeanInfoMessage[]>
|
|
busy: Ref<boolean>
|
|
version: Ref<string | null>
|
|
error: Ref<string | null>
|
|
text: Ref<string>
|
|
/* the uri the lean server knows this buffer by — LSP requests must
|
|
* name the document the server opened, not the editor's local one */
|
|
serverDocUri: Ref<string>
|
|
start: () => Promise<void>
|
|
retry: () => void
|
|
change: (text: string) => void
|
|
cursorAt: (line: number, character: number) => void
|
|
request: <T>(method: string, params?: unknown) => Promise<T>
|
|
onDiagnostics: (cb: (diags: LeanDiagnostic[]) => void) => () => void
|
|
}
|
|
|
|
let singleton: LeanSession | null = null
|
|
|
|
export function useLeanSession(): LeanSession {
|
|
const config = useRuntimeConfig()
|
|
const leanUrl = String(config.public.leanUrl || '')
|
|
|
|
if (!singleton && import.meta.client && leanUrl) singleton = createSession(leanUrl)
|
|
|
|
/* a dormant stand-in keeps the component honest on the server, where
|
|
* there is nothing to speak to */
|
|
return singleton ?? {
|
|
phase: ref('idle') as Ref<LeanPhase>,
|
|
goals: ref([]) as Ref<string[]>,
|
|
messages: ref([]) as Ref<LeanInfoMessage[]>,
|
|
busy: ref(false) as Ref<boolean>,
|
|
version: ref(null) as Ref<string | null>,
|
|
error: ref(null) as Ref<string | null>,
|
|
text: ref('') as Ref<string>,
|
|
serverDocUri: ref('') as Ref<string>,
|
|
start: async () => {},
|
|
retry: () => {},
|
|
change: () => {},
|
|
cursorAt: () => {},
|
|
request: async () => { throw new Error('no lean session') },
|
|
onDiagnostics: () => () => {},
|
|
}
|
|
}
|
|
|
|
function createSession(leanUrl: string): LeanSession {
|
|
const phase = ref<LeanPhase>('idle')
|
|
const goals = ref<string[]>([])
|
|
const messages = ref<LeanInfoMessage[]>([])
|
|
const busy = ref(false)
|
|
const version = ref<string | null>(null)
|
|
const error = ref<string | null>(null)
|
|
const text = ref('')
|
|
const serverDocUri = ref('')
|
|
|
|
let rpc: RpcSocket | null = null
|
|
let docUri = `${FALLBACK_PROJECT}/${DOCUMENT_NAME}`
|
|
let sentVersion = 0
|
|
let lastSentText = ''
|
|
const cursor = { line: 0, character: 0 }
|
|
const diagListeners = new Set<(diags: LeanDiagnostic[]) => void>()
|
|
let lastDiags: LeanDiagnostic[] = []
|
|
|
|
let changeTimer: ReturnType<typeof setTimeout> | undefined
|
|
let goalTimer: ReturnType<typeof setTimeout> | undefined
|
|
|
|
const wsBase = leanUrl.replace(/\/+$/, '').replace(/^http/, 'ws')
|
|
|
|
async function pickProject(): Promise<string> {
|
|
try {
|
|
// the server's REST endpoints carry no CORS headers — probing them from
|
|
// another origin only earns a blocked request, so stay quiet cross-origin
|
|
// and name the canonical project (the websocket is CORS-free)
|
|
if (new URL(leanUrl, window.location.href).origin !== window.location.origin) {
|
|
return FALLBACK_PROJECT
|
|
}
|
|
const res = await fetch(`${leanUrl.replace(/\/+$/, '')}/api/projects`)
|
|
const projects = (await res.json()) as Array<{ folder: string, config?: { default?: boolean, hidden?: boolean } }>
|
|
const visible = projects.filter(p => !p.config?.hidden)
|
|
return (visible.find(p => p.config?.default) ?? visible[0])?.folder || FALLBACK_PROJECT
|
|
}
|
|
catch { return FALLBACK_PROJECT }
|
|
}
|
|
|
|
function handleNotification(method: string, params: unknown) {
|
|
const p = params as Record<string, any> | undefined
|
|
if (method === '$/lean/fileProgress') {
|
|
busy.value = Array.isArray(p?.processing) && p.processing.length > 0
|
|
return
|
|
}
|
|
if (method === 'textDocument/publishDiagnostics') {
|
|
const raw = Array.isArray(p?.diagnostics) ? p.diagnostics as LeanDiagnostic[] : []
|
|
// the server marks some diagnostics silent (elaboration noise); the
|
|
// wiki shows errors/warnings in the editor, info in the Messages pane
|
|
const diags = raw.filter(d => !('isSilent' in d && (d as any).isSilent))
|
|
lastDiags = diags
|
|
messages.value = diags
|
|
.filter(d => d.severity === 3)
|
|
.map(d => ({ line: d.range.start.line + 1, text: d.message }))
|
|
for (const cb of diagListeners) cb(diags)
|
|
}
|
|
}
|
|
|
|
async function connect() {
|
|
phase.value = 'connecting'
|
|
error.value = null
|
|
const project = await pickProject()
|
|
docUri = `${project}/${DOCUMENT_NAME}`
|
|
// a fresh document identity means the buffer below re-sends as new
|
|
sentVersion = 0
|
|
lastSentText = ''
|
|
|
|
try {
|
|
rpc = new RpcSocket(`${wsBase}/websocket/${project}`, {
|
|
onNotification: handleNotification,
|
|
onClose: () => {
|
|
if (phase.value !== 'idle' && phase.value !== 'lost') {
|
|
phase.value = 'lost'
|
|
busy.value = false
|
|
}
|
|
},
|
|
})
|
|
await rpc.whenOpen
|
|
|
|
phase.value = 'initializing'
|
|
const init = await rpc.request<{
|
|
serverInfo?: { name?: string, version?: string }
|
|
}>('initialize', {
|
|
processId: null,
|
|
clientInfo: { name: 'mathew', version: '0.1.0' },
|
|
rootUri: '',
|
|
capabilities: {
|
|
general: { positionEncodings: ['utf-16'] },
|
|
workspace: { configuration: false, workspaceFolders: false, applyEdit: true },
|
|
window: {
|
|
showMessage: {},
|
|
showDocument: { support: true },
|
|
workDoneProgress: true,
|
|
configuration: true,
|
|
},
|
|
textDocument: {
|
|
synchronization: { didChange: true, willSave: false, didSave: false },
|
|
publishDiagnostics: { relatedInformation: true, versionSupport: true },
|
|
hover: { contentFormat: ['markdown', 'plaintext'] },
|
|
definition: { linkSupport: true },
|
|
documentHighlight: {},
|
|
completion: {
|
|
completionItem: {
|
|
snippetSupport: true,
|
|
documentationFormat: ['markdown', 'plaintext'],
|
|
insertTextFormat: { valueSet: [1, 2] },
|
|
additionalTextEditsSupport: true,
|
|
},
|
|
contextSupport: true,
|
|
},
|
|
},
|
|
},
|
|
initializationOptions: { hasWidgets: true },
|
|
})
|
|
version.value = init.serverInfo?.version ?? null
|
|
rpc.notify('initialized', {})
|
|
rpc.notify('textDocument/didOpen', {
|
|
textDocument: { uri: docUri, languageId: 'lean4', version: 1, text: text.value },
|
|
})
|
|
sentVersion = 1
|
|
lastSentText = text.value
|
|
phase.value = 'ready'
|
|
void refreshGoal()
|
|
}
|
|
catch (err) {
|
|
error.value = err instanceof Error ? err.message : String(err)
|
|
phase.value = 'lost'
|
|
}
|
|
}
|
|
|
|
async function refreshGoal() {
|
|
if (!rpc || phase.value !== 'ready') return
|
|
try {
|
|
const res = await rpc.request<{ goals?: string[], rendered?: string } | null>(
|
|
'$/lean/plainGoal',
|
|
{ textDocument: { uri: docUri }, position: cursor },
|
|
)
|
|
// the server answers `null` away from tactic goals; `rendered` is the
|
|
// goals as a markdown fence — the array is the honest plain text
|
|
goals.value = res?.goals ?? []
|
|
}
|
|
catch { /* raced by a newer edit (ContentModified) — the next ask wins */ }
|
|
}
|
|
|
|
function sendChange() {
|
|
if (!rpc || phase.value !== 'ready' || text.value === lastSentText) return
|
|
sentVersion += 1
|
|
// LSP allows one change spanning the whole document — simple and exact
|
|
const endLine = Math.max(lastSentText.split('\n').length - 1, 0)
|
|
const endChar = lastSentText.slice(lastSentText.lastIndexOf('\n') + 1).length
|
|
rpc.notify('textDocument/didChange', {
|
|
textDocument: { uri: docUri, version: sentVersion },
|
|
contentChanges: [{
|
|
range: { start: { line: 0, character: 0 }, end: { line: endLine, character: endChar } },
|
|
text: text.value,
|
|
}],
|
|
})
|
|
lastSentText = text.value
|
|
void refreshGoal()
|
|
}
|
|
|
|
return {
|
|
phase,
|
|
goals,
|
|
messages,
|
|
busy,
|
|
version,
|
|
error,
|
|
text,
|
|
|
|
async start() {
|
|
if (phase.value !== 'idle') return
|
|
await connect()
|
|
},
|
|
|
|
retry() {
|
|
try { rpc?.close() }
|
|
catch { /* gone */ }
|
|
rpc = null
|
|
goals.value = []
|
|
messages.value = []
|
|
busy.value = false
|
|
void connect()
|
|
},
|
|
|
|
change(newText) {
|
|
text.value = newText
|
|
clearTimeout(changeTimer)
|
|
changeTimer = setTimeout(sendChange, 400)
|
|
},
|
|
|
|
cursorAt(line, character) {
|
|
cursor.line = line
|
|
cursor.character = character
|
|
clearTimeout(goalTimer)
|
|
goalTimer = setTimeout(() => void refreshGoal(), 200)
|
|
},
|
|
|
|
request<T>(method: string, params?: unknown) {
|
|
if (!rpc || phase.value !== 'ready') return Promise.reject(new Error('lean is not ready'))
|
|
return rpc.request<T>(method, params)
|
|
},
|
|
|
|
onDiagnostics(cb) {
|
|
diagListeners.add(cb)
|
|
// a freshly (re)attached editor wants the current marks at once
|
|
cb(lastDiags)
|
|
return () => diagListeners.delete(cb)
|
|
},
|
|
}
|
|
}
|