)
diff --git a/src/app/components/Error.tsx b/src/app/components/Error.tsx
index 418c6104..51866e51 100644
--- a/src/app/components/Error.tsx
+++ b/src/app/components/Error.tsx
@@ -1,3 +1,5 @@
+import type React from 'react'
+
export default function Error({ children }: { children: React.ReactNode }) {
return (
{
- authClient.signIn.social({
+ onClick={async () => {
+ await authClient.signIn.social({
provider: 'github',
})
}}
diff --git a/src/app/setup/actions.ts b/src/app/setup/actions.ts
index a48ec65c..7a8dedad 100644
--- a/src/app/setup/actions.ts
+++ b/src/app/setup/actions.ts
@@ -21,7 +21,7 @@ export async function saveSetupConfig(formData: FormData): Promise
{
// This relies on version tags being returned first.
const res: Response = await fetch('https://api.github.com/repos/leanprover-community/mathlib4/tags?per_page=100')
if (!res.ok) throw new Error(`GitHub API ${res.status}`)
- const data = (await res.json()) as { name: string }[]
+ const data = z.array(z.object({ name: z.string() })).parse(await res.json())
for (const item of data) if (LEAN_VERSION_RE.test(item.name)) versions.push(item.name)
return versions
}
export default function Setup() {
- const cfg = useContext(ConfigCtx)
+ const cfg = useConfigCtx()
const [wasCompleteOnMount] = useState(cfg.isSetupComplete)
// Redirect to index on new visits, but keep the page open during actual setup
if (wasCompleteOnMount) redirect('/')
@@ -46,7 +47,7 @@ export default function Setup() {
// Sync with server state on mount (handles page reload during seeding).
useEffect(() => {
- fetchSetupStatus().then(status => {
+ void fetchSetupStatus().then(status => {
if (status.configSaved) setConfigSaved(true)
if (status.seeded) setPhase('done')
else if (status.seeding) setPhase('seeding')
@@ -62,36 +63,44 @@ export default function Setup() {
// Stream seed events whenever we're in the seeding phase.
useEffect(() => {
- if (phase !== 'seeding') return
+ if (phase !== 'seeding') return undefined
const source = new EventSource('/api/setup-events')
source.onmessage = event => {
- const data = JSON.parse(event.data)
- if (data.type === 'progress') {
- const pct = Math.round((data.step / data.total) * 100)
- setProgress({ pct, label: `${data.label} (${data.step}/${data.total})` })
- } else if (data.type === 'log') {
- setLogs(prev => [...prev, data.line])
- } else if (data.type === 'done') {
- source.close()
- setProgress({ pct: 100, label: '' })
- setPhase('done')
- } else if (data.type === 'error') {
- source.close()
- setSeedError(data.message)
- setPhase('error')
- }
- }
- source.onerror = () => {
- source.close()
- fetchSetupStatus().then(status => {
- if (status.seeded) {
+ const data = zSeedEvent.parse(JSON.parse(event.data as string /* EventSources ensure this in practice */))
+ switch (data.type) {
+ case 'progress': {
+ const pct = Math.round((data.step / data.total) * 100)
+ setProgress({ pct, label: `${data.label} (${data.step}/${data.total})` })
+ break
+ }
+ case 'log': {
+ setLogs(prev => [...prev, data.line])
+ break
+ }
+ case 'done': {
+ source.close()
setProgress({ pct: 100, label: '' })
setPhase('done')
- } else if (!status.seeding) {
- setSeedError('Connection lost')
+ break
+ }
+ case 'error': {
+ source.close()
+ setSeedError(data.message)
setPhase('error')
+ break
}
- })
+ }
+ }
+ source.onerror = async () => {
+ source.close()
+ const status = await fetchSetupStatus()
+ if (status.seeded) {
+ setProgress({ pct: 100, label: '' })
+ setPhase('done')
+ } else if (!status.seeding) {
+ setSeedError('Connection lost')
+ setPhase('error')
+ }
}
return () => source.close()
}, [phase])
@@ -210,12 +219,10 @@ export default function Setup() {
- {(phase === 'seeding' || phase === 'error') && (
-
- {phase === 'seeding' && }
- {progress.label || 'Starting...'}
-
- )}
+
+ {phase === 'seeding' && }
+ {progress.label || 'Starting...'}
+
)}
diff --git a/src/lib/contexts.ts b/src/lib/contexts.ts
index 39eab41c..b6211a59 100644
--- a/src/lib/contexts.ts
+++ b/src/lib/contexts.ts
@@ -1,6 +1,6 @@
'use client'
-import { createContext } from 'react'
+import { createContext, useContext } from 'react'
import type { RegistrationMode } from '@/lib/server/config'
@@ -11,7 +11,11 @@ export interface Config {
registrationMode: RegistrationMode
}
-/** Read-only UI configuration derived from the server configuration. */
-// We set this in `RootLayout`.
-// eslint-disable-next-line @typescript-eslint/no-explicit-any
-export const ConfigCtx = createContext
(null as any)
+/** Read-only UI configuration derived from the server configuration, set in RootLayout */
+export const ConfigCtx = createContext(null)
+
+export function useConfigCtx() {
+ const cfg = useContext(ConfigCtx)
+ if (!cfg) throw new Error('useConfigCtx called outside of a ConfigCtx')
+ return cfg
+}
diff --git a/src/lib/rcMap.ts b/src/lib/rcMap.ts
index 0d4e6cd7..d30bdf09 100644
--- a/src/lib/rcMap.ts
+++ b/src/lib/rcMap.ts
@@ -18,7 +18,7 @@ export class RcMap implements AsyncDisposable {
this.entries.set(key, resource)
}
resource.count++
- const value = await resource.value.catch(err => {
+ const value = await resource.value.catch((err: unknown) => {
if (--resource.count === 0) this.entries.delete(key)
throw err
})
diff --git a/src/lib/server/collabServer.ts b/src/lib/server/collabServer.ts
index 2a052575..bce726fe 100644
--- a/src/lib/server/collabServer.ts
+++ b/src/lib/server/collabServer.ts
@@ -121,7 +121,7 @@ export class CollabServerHandle implements AsyncDisposable {
if (this.disposing) return this.disposing
this.disposing = (async () => {
if (this.starting) {
- await this.starting!.catch(() => {})
+ await this.starting.catch(() => {})
if (this.proc) {
await new Promise(resolve => {
this.proc!.once('close', () => {
diff --git a/src/lib/server/dirToken.ts b/src/lib/server/dirToken.ts
index 4ec29934..de0bb142 100644
--- a/src/lib/server/dirToken.ts
+++ b/src/lib/server/dirToken.ts
@@ -43,8 +43,8 @@ export function mintSignedDirToken(rootDir: string): string {
* or `null` if the token is invalid or expired. */
export function verifySignedDirToken(token: string): string | null {
const parts = token.split('.')
- if (parts.length !== 3) return null
- const [rootDirB64, exp, sig] = parts
+ const [rootDirB64, exp, sig, ...rest] = parts
+ if (rootDirB64 === undefined || exp === undefined || sig === undefined || rest.length != 0) return null
const expected = hmac(`${rootDirB64}.${exp}`)
if (sig.length !== expected.length || !crypto.timingSafeEqual(Buffer.from(sig), Buffer.from(expected))) {
return null
diff --git a/src/lib/server/editorSessions.ts b/src/lib/server/editorSessions.ts
index cb7fd71c..bd9c52f3 100644
--- a/src/lib/server/editorSessions.ts
+++ b/src/lib/server/editorSessions.ts
@@ -247,8 +247,8 @@ export async function initEditorSessions() {
for (const servers of m['vscServers'].values()) {
for (const s of servers) Object.setPrototypeOf(s, VscodeServerHandle.prototype)
}
- await m['mounts'].forEach(mount => Object.setPrototypeOf(mount, ProjectMountHandle.prototype))
- await m['collabServers'].forEach(collab => Object.setPrototypeOf(collab, CollabServerHandle.prototype))
+ await m['mounts'].forEach(mount => Object.setPrototypeOf(mount, ProjectMountHandle.prototype) as unknown)
+ await m['collabServers'].forEach(collab => Object.setPrototypeOf(collab, CollabServerHandle.prototype) as unknown)
}
}
diff --git a/src/lib/server/seed.ts b/src/lib/server/seed.ts
index c756f455..4e38a7dd 100644
--- a/src/lib/server/seed.ts
+++ b/src/lib/server/seed.ts
@@ -3,19 +3,10 @@ import 'server-only'
import { spawn } from 'node:child_process'
import path from 'node:path'
-import { type ActionResponse, LEAN_VERSION_RE } from '@/lib/util'
+import { type ActionResponse, LEAN_VERSION_RE, type SeedEvent } from '@/lib/util'
import { getConfig, getDataDir, saveConfig } from './config'
-export interface SeedEvent {
- type: 'log' | 'progress' | 'done' | 'error'
- line?: string
- step?: number
- total?: number
- label?: string
- message?: string
-}
-
export interface SeedState {
inProgress: boolean
events: SeedEvent[]
@@ -57,7 +48,7 @@ export function startSeed(leanVersion: string | undefined): ActionResponse {
// Git reads `$HOME/.config/git/config` as the global config.
const name = user.displayName?.trim() || user.name
- const email = user.email?.trim()
+ const email = user.email.trim()
const userBlock = ['[user]']
if (name) userBlock.push(`\tname = ${name}`)
if (email) userBlock.push(`\temail = ${email}`)
diff --git a/src/lib/server/util.ts b/src/lib/server/util.ts
index 2553b0ad..f1a0231a 100644
--- a/src/lib/server/util.ts
+++ b/src/lib/server/util.ts
@@ -18,7 +18,7 @@ export function serverAction(
): (raw: z.input) => Promise> {
return async raw => {
const parsed = schema.safeParse(raw)
- if (!parsed.success) return { error: parsed.error.issues[0].message }
+ if (!parsed.success) return { error: parsed.error.issues[0]!.message }
return handler(parsed.data)
}
}
diff --git a/src/lib/server/vscodeServer.ts b/src/lib/server/vscodeServer.ts
index ee3fde68..e30e3262 100644
--- a/src/lib/server/vscodeServer.ts
+++ b/src/lib/server/vscodeServer.ts
@@ -315,12 +315,13 @@ export class VscodeServerHandle implements AsyncDisposable {
/** Start a debugger in the extension host of the VSCode server. */
async enableDebugger() {
- if (!this.proc) return
+ const proc = this.proc
+ if (!proc) return
// Send SIGUSR1 to the (assumed unique) extension host descendant of code-server:
// https://nodejs.org/api/process.html#signal-events
- const root = (await readProcesses()).get(this.proc.pid!)
+ const root = (await readProcesses()).get(proc.pid!)
// Give up if parent has exited while we read proc table
- if (!this.proc) return
+ if (this.proc !== proc) return
const stack = root ? [root] : []
while (stack.length > 0) {
const proc = stack.pop()!
diff --git a/src/lib/util.ts b/src/lib/util.ts
index 959e247a..d824d189 100644
--- a/src/lib/util.ts
+++ b/src/lib/util.ts
@@ -1,4 +1,4 @@
-import z from 'zod'
+import { z } from 'zod'
/** Server actions respond with data of this shape. */
export type ActionResponse = { ok: T } | { error: string }
@@ -27,3 +27,19 @@ export const zProjectName = z.string().regex(ALPHANUM_NAME_RE, 'Invalid project
export const zTemplateId = z.string().regex(TEMPLATE_ID_RE, 'Invalid template ID')
export const LEAN_VERSION_RE = /^v4\.\d+\.\d+(-rc\d+)?$/
+
+export const zSeedEvent = z.discriminatedUnion('type', [
+ z.object({ type: z.literal('log'), line: z.string() }),
+ z.object({ type: z.literal('progress'), step: z.number(), total: z.number(), label: z.string() }),
+ z.object({ type: z.literal('done') }),
+ z.object({ type: z.literal('error'), message: z.string() }),
+])
+export type SeedEvent = z.infer
+
+/** Assert a field in `formData` is a string or absent, return the empty string if it's absent */
+export function formString(formData: FormData, name: string): string {
+ const value = formData.get(name)
+ if (value === null) return ''
+ if (typeof value === 'string') return value
+ throw new Error(`form field '${name}' is a File unexpectedly`)
+}
diff --git a/src/proxy.ts b/src/proxy.ts
index 2e863de6..07f13c79 100644
--- a/src/proxy.ts
+++ b/src/proxy.ts
@@ -2,7 +2,7 @@ import { NextRequest, NextResponse } from 'next/server'
import { getConfig } from './lib/server/config'
-export async function proxy(request: NextRequest) {
+export function proxy(request: NextRequest) {
const cfg = getConfig()
if (!cfg.isSetupComplete) {
const path = request.nextUrl.pathname
diff --git a/tsconfig.json b/tsconfig.json
index 2327183f..c88ece4d 100644
--- a/tsconfig.json
+++ b/tsconfig.json
@@ -21,7 +21,11 @@
],
"paths": {
"@/*": ["./src/*"]
- }
+ },
+ "noFallthroughCasesInSwitch": true,
+ "noImplicitOverride": true,
+ "noImplicitReturns": true,
+ "noUncheckedIndexedAccess": true
},
// Subfolders of `.next/` duplicated since without that `next dev` tries to rewrite this config.
"include": [
diff --git a/vscode-workbench/src/collabServer.ts b/vscode-workbench/src/collabServer.ts
index 111e79e1..47f6b5b5 100644
--- a/vscode-workbench/src/collabServer.ts
+++ b/vscode-workbench/src/collabServer.ts
@@ -89,7 +89,7 @@ export async function connectToCollabServer(
}
const color = AWARENESS_CURSOR_COLORS.reduce(
(acc, c) => (counts.get(acc)! <= counts.get(c)! ? acc : c),
- AWARENESS_CURSOR_COLORS[0],
+ AWARENESS_CURSOR_COLORS[0]!,
)
awarenessProvider.setAwarenessField(AWARENESS_USER_KEY, {
diff --git a/vscode-workbench/src/extension.ts b/vscode-workbench/src/extension.ts
index bf12b898..bd00e923 100644
--- a/vscode-workbench/src/extension.ts
+++ b/vscode-workbench/src/extension.ts
@@ -35,7 +35,7 @@ async function ensureProjectFolderOpen(mdata: WorkspaceMetadata, log: vs.LogOutp
const expected = bwrapProjectDir(mdata.project.name)
if (
vs.workspace.workspaceFolders?.length === 1 &&
- path.resolve(vs.workspace.workspaceFolders[0].uri.fsPath) === path.resolve(expected)
+ path.resolve(vs.workspace.workspaceFolders[0]!.uri.fsPath) === path.resolve(expected)
)
return true
diff --git a/vscode-workbench/src/panel.ts b/vscode-workbench/src/panel.ts
index d08f2092..0cfb983e 100644
--- a/vscode-workbench/src/panel.ts
+++ b/vscode-workbench/src/panel.ts
@@ -70,7 +70,7 @@ export class WorkbenchPanelProvider implements vs.TreeDataProvider, v
if (!sels) continue
filePath = sels.filePath
if (0 < sels.selections.length) {
- const active = sels.selections[0].active
+ const active = sels.selections[0]!.active
const pos = new vs.Position(active.line, active.character)
sel = new vs.Selection(pos, pos)
break
diff --git a/vscode-workbench/src/remoteSelections.ts b/vscode-workbench/src/remoteSelections.ts
index 4d45cd39..c2adbf4b 100644
--- a/vscode-workbench/src/remoteSelections.ts
+++ b/vscode-workbench/src/remoteSelections.ts
@@ -117,10 +117,10 @@ export class RemoteSelectionDecorator implements vs.Disposable {
const decos = this.decorationsFor(clientId, user.color)
const beforeRanges: vs.DecorationOptions[] = []
const afterRanges: vs.DecorationOptions[] = []
- if (selection?.filePath === filePath) {
+ if (selection.filePath === filePath) {
for (const s of selection.selections) {
const range = new vs.Range(s.anchor.line, s.anchor.character, s.active.line, s.active.character)
- const opts = { range, hoverMessage: user?.name }
+ const opts = { range, hoverMessage: user.name }
// Is `active` at the start or the end of the selection?
if (
s.active.line < s.anchor.line ||
diff --git a/vscode-workbench/src/textBinding.ts b/vscode-workbench/src/textBinding.ts
index d8ff6e30..0123500e 100644
--- a/vscode-workbench/src/textBinding.ts
+++ b/vscode-workbench/src/textBinding.ts
@@ -192,8 +192,8 @@ export class YTextBinding implements vs.Disposable {
* Work items are atomic w.r.t. all other work items
* (but not w.r.t. other `async` operations). */
private enqueueTransaction(work: () => Promise): void {
- this.mutex = this.mutex.then(work).catch(e => {
- this.log.error(e)
+ this.mutex = this.mutex.then(work).catch((e: unknown) => {
+ this.log.error(e instanceof Error ? e.message : String(e))
})
}
@@ -257,7 +257,7 @@ export class YTextBinding implements vs.Disposable {
Y.applyUpdate(this.localYdoc, Y.encodeStateAsUpdate(this.hs.document))
this.localYdoc.on('update', this.onLocalUpdate)
- const remoteStr = this.remoteYtext.toString()
+ const remoteStr = this.remoteYtext.toJSON()
const localStr = this.doc.getText()
if (remoteStr === localStr) {
this.log.trace('[initFromRemote] synced without edit')
@@ -414,7 +414,7 @@ export class YTextBinding implements vs.Disposable {
if (this.ensureSyncTimeout) clearTimeout(this.ensureSyncTimeout)
this.ensureSyncTimeout = setTimeout(() => {
this.enqueueTransaction(async () => {
- const localYtextStr = this.localYtext.toString()
+ const localYtextStr = this.localYtext.toJSON()
const docStr = this.doc.getText()
if (docStr !== localYtextStr) {
this.log.debug('[ensureSync] doc<->localYdoc desync, overwriting')
diff --git a/vscode-workbench/src/vscode.proposed.extensionsAny.d.ts b/vscode-workbench/src/vscode.proposed.extensionsAny.d.ts
index ccf5a631..caaffee5 100644
--- a/vscode-workbench/src/vscode.proposed.extensionsAny.d.ts
+++ b/vscode-workbench/src/vscode.proposed.extensionsAny.d.ts
@@ -6,7 +6,7 @@
declare module 'vscode' {
// https://github.com/microsoft/vscode/issues/145307 @alexdima
- export interface Extension<_T> {
+ export interface Extension {
/**
* `true` when the extension is associated to another extension host.
*
diff --git a/vscode-workbench/test/collab.test.ts b/vscode-workbench/test/collab.test.ts
index 4c448008..bc85299f 100644
--- a/vscode-workbench/test/collab.test.ts
+++ b/vscode-workbench/test/collab.test.ts
@@ -8,7 +8,7 @@ import { Logger } from '../src/util'
const delay = (ms: number) => new Promise(r => setTimeout(r, ms))
-const logLevel: vs.LogLevel = vs.LogLevel.Debug as unknown as vs.LogLevel // cast prevents TS from complaining
+const logLevel = vs.LogLevel.Debug as vs.LogLevel // cast prevents TS from complaining
const consoleLog: Logger = {
logLevel,
trace: (m, ...a) => {
@@ -90,7 +90,7 @@ async function waitForQuiescence(bindings: YTextBinding[], timeoutMs: number): P
let prev = ''
let stableIters = 0
while (performance.now() < deadline) {
- const snap = bindings.map(b => b.remoteYtext.toString() + '|' + b.doc.getText()).join('|')
+ const snap = bindings.map(b => b.remoteYtext.toJSON() + '|' + b.doc.getText()).join('|')
if (snap === prev) {
if (stableIters++ >= 5) return
} else {
@@ -132,14 +132,14 @@ suite('Collaborative editing', () => {
vs.workspace.openTextDocument({ content: '', language: 'plaintext' }),
])
const bindings = docs.map(
- (doc, i) => new YTextBinding(doc, clients[i], consoleLog, true, ensureSyncTimeoutMs, DOC_NAME),
+ (doc, i) => new YTextBinding(doc, clients[i]!, consoleLog, true, ensureSyncTimeoutMs, DOC_NAME),
)
// Route document changes to the matching binding
// (`YTextBindingManager.onDidChangeTextDocument` does this in production).
const changeSub = vs.workspace.onDidChangeTextDocument(e => {
const i = docs.indexOf(e.document)
- if (i >= 0) bindings[i].onLocalChange(e)
+ if (i >= 0) bindings[i]!.onLocalChange(e)
})
return {
@@ -166,12 +166,12 @@ suite('Collaborative editing', () => {
await waitForInitialSync(handles.bindings, 1_000)
// Type on doc0 and confirm the change reaches doc1.
- const ed0 = await vs.window.showTextDocument(handles.docs[0], { viewColumn: COLUMNS[0], preview: false })
+ const ed0 = await vs.window.showTextDocument(handles.docs[0]!, { viewColumn: COLUMNS[0], preview: false })
ed0.selection = new vs.Selection(0, 0, 0, 0)
const text = 'PROBE\n'
await vs.commands.executeCommand('default:type', { text })
await waitForQuiescence(handles.bindings, 1_000)
- assert.strictEqual(handles.docs[1].getText(), text)
+ assert.strictEqual(handles.docs[1]!.getText(), text)
await handles.dispose()
})
@@ -181,19 +181,19 @@ suite('Collaborative editing', () => {
const rng = mulberry32(0xc0ffee)
const NUM_EDITS = 100
for (let i = 0; i < NUM_EDITS; i++) {
- await randomEditOn(handles.docs[i % 2], COLUMNS[i % 2], rng)
+ await randomEditOn(handles.docs[i % 2]!, COLUMNS[i % 2]!, rng)
}
}
const assertEqualStates = (handles: TestHandles) => {
const [d0, d1] = handles.docs.map(d => d.getText())
- const [y0, y1] = handles.bindings.map(b => b.remoteYtext.toString())
+ const [y0, y1] = handles.bindings.map(b => b.remoteYtext.toJSON())
// Sanity check - YJs CRDT replicas converge.
- assert.strictEqual(y0, y1, diffMessage('Y.Text replicas (client0 vs client1)', y0, y1))
+ assert.strictEqual(y0, y1, diffMessage('Y.Text replicas (client0 vs client1)', y0!, y1!))
// Whether docs correctly track CRDT replicas.
- assert.strictEqual(d0, y0, diffMessage('doc0 vs its Y.Text', d0, y0))
- assert.strictEqual(d1, y1, diffMessage('doc1 vs its Y.Text', d1, y1))
+ assert.strictEqual(d0, y0, diffMessage('doc0 vs its Y.Text', d0!, y0!))
+ assert.strictEqual(d1, y1, diffMessage('doc1 vs its Y.Text', d1!, y1!))
}
test('Concurrent edits settle on equal states', async function () {
@@ -214,11 +214,11 @@ suite('Collaborative editing', () => {
await waitForInitialSync(handles.bindings, 1_000)
// Ensure both documents are visible:
// only `TextEditor.edit`s are expected to converge without ensureSync.
- await vs.window.showTextDocument(handles.docs[0], { viewColumn: COLUMNS[0], preview: false })
- await vs.window.showTextDocument(handles.docs[1], { viewColumn: COLUMNS[1], preview: false })
+ await vs.window.showTextDocument(handles.docs[0]!, { viewColumn: COLUMNS[0], preview: false })
+ await vs.window.showTextDocument(handles.docs[1]!, { viewColumn: COLUMNS[1], preview: false })
await makeConcurrentEdits(handles)
await waitForQuiescence(handles.bindings, 3_000)
- await assertEqualStates(handles)
+ assertEqualStates(handles)
await handles.dispose()
})
})