From 9cc494db8baec28e50b58633dc59f6a15ec3067b Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Mon, 11 May 2026 07:37:49 -0400 Subject: [PATCH] feat: quality of life improvements --- src/app/[userName]/NewProjectForm.tsx | 2 +- src/app/[userName]/ProjectRow.tsx | 2 +- src/app/admin/components/AllowlistEditor.tsx | 2 +- src/app/admin/components/HealthMonitor.tsx | 2 +- src/app/admin/components/OAuthConfig.tsx | 2 +- .../components/RegistrationModeControl.tsx | 2 +- src/app/admin/components/SessionRow.tsx | 2 +- src/app/admin/components/UserRow.tsx | 2 +- src/app/api/setup-events/route.ts | 6 ++- src/app/setup/actions.ts | 6 +-- src/app/setup/page.tsx | 40 ++++++++++++++++--- src/lib/client/util.ts | 15 +++++++ src/lib/server/config.ts | 1 + src/lib/server/seed.ts | 9 +++-- src/lib/server/vscodeServer.ts | 8 ++-- src/lib/util.ts | 15 +------ start.sh | 20 +++++++--- 17 files changed, 93 insertions(+), 43 deletions(-) create mode 100644 src/lib/client/util.ts diff --git a/src/app/[userName]/NewProjectForm.tsx b/src/app/[userName]/NewProjectForm.tsx index 6ef3cd2..7b409c8 100644 --- a/src/app/[userName]/NewProjectForm.tsx +++ b/src/app/[userName]/NewProjectForm.tsx @@ -1,6 +1,6 @@ 'use client' -import { useServerAction } from '@/lib/util' +import { useServerAction } from '@/lib/client/util' import { useRouter } from 'next/navigation' import { useState } from 'react' import useSWR from 'swr' diff --git a/src/app/[userName]/ProjectRow.tsx b/src/app/[userName]/ProjectRow.tsx index 8f84b02..c72cac2 100644 --- a/src/app/[userName]/ProjectRow.tsx +++ b/src/app/[userName]/ProjectRow.tsx @@ -1,6 +1,6 @@ 'use client' -import { useServerAction } from '@/lib/util' +import { useServerAction } from '@/lib/client/util' import { Route } from 'next' import Link from 'next/link' import { useRouter } from 'next/navigation' diff --git a/src/app/admin/components/AllowlistEditor.tsx b/src/app/admin/components/AllowlistEditor.tsx index f11c6e8..9b7a1d1 100644 --- a/src/app/admin/components/AllowlistEditor.tsx +++ b/src/app/admin/components/AllowlistEditor.tsx @@ -1,6 +1,6 @@ 'use client' -import { useServerAction } from '@/lib/util' +import { useServerAction } from '@/lib/client/util' import { useRouter } from 'next/navigation' import { startTransition, useRef } from 'react' import { addAllowedUser, removeAllowedUser } from '../actions' diff --git a/src/app/admin/components/HealthMonitor.tsx b/src/app/admin/components/HealthMonitor.tsx index 6d60faf..05119e7 100644 --- a/src/app/admin/components/HealthMonitor.tsx +++ b/src/app/admin/components/HealthMonitor.tsx @@ -1,6 +1,6 @@ 'use client' -import { useServerAction } from '@/lib/util' +import { useServerAction } from '@/lib/client/util' import { startTransition, useState } from 'react' import useSWR from 'swr' import { fetchDiskUsage, fetchHealth } from '../actions' diff --git a/src/app/admin/components/OAuthConfig.tsx b/src/app/admin/components/OAuthConfig.tsx index 0bea076..6268016 100644 --- a/src/app/admin/components/OAuthConfig.tsx +++ b/src/app/admin/components/OAuthConfig.tsx @@ -1,6 +1,6 @@ 'use client' -import { useServerAction } from '@/lib/util' +import { useServerAction } from '@/lib/client/util' import { useState } from 'react' import useSWR from 'swr' import { fetchOAuthConfig, updateOAuthConfig } from '../actions' diff --git a/src/app/admin/components/RegistrationModeControl.tsx b/src/app/admin/components/RegistrationModeControl.tsx index 894ea2a..cb78c88 100644 --- a/src/app/admin/components/RegistrationModeControl.tsx +++ b/src/app/admin/components/RegistrationModeControl.tsx @@ -1,7 +1,7 @@ 'use client' +import { useServerAction } from '@/lib/client/util' import type { RegistrationMode } from '@/lib/server/config' -import { useServerAction } from '@/lib/util' import { useRouter } from 'next/navigation' import { startTransition, useState } from 'react' import { setRegistrationMode } from '../actions' diff --git a/src/app/admin/components/SessionRow.tsx b/src/app/admin/components/SessionRow.tsx index a09b197..a11693e 100644 --- a/src/app/admin/components/SessionRow.tsx +++ b/src/app/admin/components/SessionRow.tsx @@ -1,7 +1,7 @@ 'use client' +import { useServerAction } from '@/lib/client/util' import type { EditorSessionInfo } from '@/lib/server/editorSessions' -import { useServerAction } from '@/lib/util' import { useRouter } from 'next/navigation' import { startTransition } from 'react' import { killEditorSession } from '../actions' diff --git a/src/app/admin/components/UserRow.tsx b/src/app/admin/components/UserRow.tsx index 65c4a11..618b55a 100644 --- a/src/app/admin/components/UserRow.tsx +++ b/src/app/admin/components/UserRow.tsx @@ -1,6 +1,6 @@ 'use client' -import { useServerAction } from '@/lib/util' +import { useServerAction } from '@/lib/client/util' import { useRouter } from 'next/navigation' import { startTransition, useState } from 'react' import { deleteUser, toggleAdmin } from '../actions' diff --git a/src/app/api/setup-events/route.ts b/src/app/api/setup-events/route.ts index cd38c96..6b8c6ea 100644 --- a/src/app/api/setup-events/route.ts +++ b/src/app/api/setup-events/route.ts @@ -3,11 +3,12 @@ import { getSeedState } from '@/lib/server/seed' export async function GET() { const encoder = new TextEncoder() + let interval: ReturnType | undefined const stream = new ReadableStream({ start(controller) { let cursor = 0 - const interval = setInterval(() => { + interval = setInterval(() => { const st = getSeedState() while (cursor < st.events.length) { const event = st.events[cursor++] @@ -24,6 +25,9 @@ export async function GET() { } }, 500) }, + cancel() { + clearInterval(interval) + }, }) return new Response(stream, { diff --git a/src/app/setup/actions.ts b/src/app/setup/actions.ts index 142dc1a..9e8d9af 100644 --- a/src/app/setup/actions.ts +++ b/src/app/setup/actions.ts @@ -3,7 +3,7 @@ import { initAuth } from '@/lib/server/auth' import { getConfig, hasGithubAuth, saveConfig, zGithubAuthConfig } from '@/lib/server/config' import { startSeed as doStartSeed, getSeedState } from '@/lib/server/seed' -import { ActionResponse } from '@/lib/util' +import type { ActionResponse } from '@/lib/util' import z from 'zod' const zSetupConfig = z.object({ @@ -33,8 +33,8 @@ export async function saveSetupConfig(formData: FormData): Promise> { - return doStartSeed() +export async function startSeed(leanVersion: string | undefined): Promise> { + return doStartSeed(leanVersion) } export async function fetchSetupStatus() { diff --git a/src/app/setup/page.tsx b/src/app/setup/page.tsx index cb861d7..5517d12 100644 --- a/src/app/setup/page.tsx +++ b/src/app/setup/page.tsx @@ -1,14 +1,27 @@ 'use client' +import { useServerAction } from '@/lib/client/util' import { ConfigCtx } from '@/lib/contexts' -import { useServerAction } from '@/lib/util' +import { LEAN_VERSION_RE } from '@/lib/util' import Link from 'next/link' import { redirect } from 'next/navigation' import { useContext, useEffect, useRef, useState } from 'react' +import useSWR from 'swr' import { fetchSetupStatus, saveSetupConfig, startSeed } from './actions' type Phase = 'config' | 'seeding' | 'done' | 'error' +/** Fetch mathlib4 v4.* tags, newest-first, paginating until exhausted. */ +async function fetchLeanVersions(): Promise { + const versions: string[] = [] + // 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 }[] + 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 [wasCompleteOnMount] = useState(cfg.isSetupComplete) @@ -20,6 +33,8 @@ export default function Setup() { const [seedError, setSeedError] = useState('') const [progress, setProgress] = useState({ pct: 0, label: '' }) const [logs, setLogs] = useState([]) + const [leanVersion, setLeanVersion] = useState() + const { data: leanVersions } = useSWR('leanVersions', fetchLeanVersions) const logRef = useRef(null) const [configError, saveConfigAction, savingConfig] = useServerAction( @@ -90,7 +105,7 @@ export default function Setup() { setLogs([]) setProgress({ pct: 0, label: 'Starting...' }) setPhase('seeding') - const result = await startSeed() + const result = await startSeed(leanVersion) if ('error' in result) { setSeedError(result.error) setPhase('error') @@ -168,9 +183,24 @@ export default function Setup() { ) : ( <> {phase !== 'seeding' && ( - +
+ + with Lean version: + +
)} {(phase === 'seeding' || phase === 'error') && progress.pct > 0 && ( diff --git a/src/lib/client/util.ts b/src/lib/client/util.ts new file mode 100644 index 0000000..3c38a14 --- /dev/null +++ b/src/lib/client/util.ts @@ -0,0 +1,15 @@ +import type { ActionResponse } from '@/lib/util' +import { useActionState } from 'react' + +/** Returns `[error, dispatchAction, pending]`. */ +export function useServerAction( + fn: (payload: Payload) => Promise>, + onSuccess?: (_: T) => void, +) { + return useActionState(async (_: string | null, payload: Payload) => { + const result = await fn(payload) + if ('error' in result) return result.error + onSuccess?.(result.ok) + return null + }, null) +} diff --git a/src/lib/server/config.ts b/src/lib/server/config.ts index 555e19f..c4707b4 100644 --- a/src/lib/server/config.ts +++ b/src/lib/server/config.ts @@ -138,6 +138,7 @@ function ensureConfigWatcher() { .on('change', () => { try { loadConfig() + console.log('Reloaded config') } catch (e: unknown) { console.error(`Failed to reload config: ${String(e)}`) } diff --git a/src/lib/server/seed.ts b/src/lib/server/seed.ts index 3c42d96..f9aeb96 100644 --- a/src/lib/server/seed.ts +++ b/src/lib/server/seed.ts @@ -1,4 +1,4 @@ -import { ActionResponse } from '@/lib/util' +import { type ActionResponse, LEAN_VERSION_RE } from '@/lib/util' import { spawn } from 'node:child_process' import path from 'node:path' import 'server-only' @@ -31,11 +31,12 @@ export function getSeedState(): Readonly { return seedState } -export function startSeed(): ActionResponse { +export function startSeed(leanVersion: string | undefined): ActionResponse { const cfg = getConfig() if (cfg.isSetupComplete) return { error: 'Already seeded' } if (!cfg.githubAuth) return { error: 'Configure GitHub authentication first' } if (seedState.inProgress) return { error: 'Seeding already in progress' } + if (leanVersion && !LEAN_VERSION_RE.test(leanVersion)) return { error: 'Invalid Lean version' } seedState.inProgress = true seedState.events.length = 0 @@ -43,7 +44,9 @@ export function startSeed(): ActionResponse { // scripts/ is a sibling directory const scriptsDir = path.join(process.cwd(), 'scripts') - const child = spawn('bash', [path.join(scriptsDir, 'seed-volume.sh'), '--data-dir', getDataDir()], { + const args = [path.join(scriptsDir, 'seed-volume.sh'), '--data-dir', getDataDir()] + if (leanVersion) args.push('--lean-version', leanVersion) + const child = spawn('bash', args, { stdio: ['ignore', 'pipe', 'pipe'], }) diff --git a/src/lib/server/vscodeServer.ts b/src/lib/server/vscodeServer.ts index f268560..0d9e6e6 100644 --- a/src/lib/server/vscodeServer.ts +++ b/src/lib/server/vscodeServer.ts @@ -227,15 +227,15 @@ export class VscodeServerHandle { await Promise.race([ // Reject if errors occur before setup is finished. new Promise((_, reject) => { - proc.once('error', err => { - reject(err) - }) proc.once('close', () => { this.proc = undefined reject(new Error(`${this.description} exited before binding port`)) }) + proc.once('error', err => { + reject(new Error(`${this.description} failed to start: ${String(err)}`)) + }) workspaceConfigPipe.once('error', err => { - reject(err) + reject(new Error(`${this.description} failed to write workspace file: ${String(err)}`)) }) }), // Wait for the server to start listening and for Nginx to be ready. diff --git a/src/lib/util.ts b/src/lib/util.ts index 4b10029..14b12e9 100644 --- a/src/lib/util.ts +++ b/src/lib/util.ts @@ -1,16 +1,3 @@ -import { useActionState } from 'react' - export type ActionResponse = { ok: T } | { error: string } -/** Returns `[error, dispatchAction, pending]`. */ -export function useServerAction( - fn: (payload: Payload) => Promise>, - onSuccess?: (_: T) => void, -) { - return useActionState(async (_: string | null, payload: Payload) => { - const result = await fn(payload) - if ('error' in result) return result.error - onSuccess?.(result.ok) - return null - }, null) -} +export const LEAN_VERSION_RE = /^v4\.\d+\.\d+(-rc\d+)?$/ diff --git a/start.sh b/start.sh index 0b11450..a8edd3d 100755 --- a/start.sh +++ b/start.sh @@ -25,13 +25,20 @@ if [ "${NODE_ENV}" = "production" ]; then cd "${SCRIPT_DIR}" && node_modules/.bin/next start --port 3002 & else # Dev mode: ${SCRIPT_DIR} is mounted read-only by the host. - # Make build-time container writes succeed by putting them on tmpfs. - # NOTE: also tried a full tmpfs overlay on ${SCRIPT_DIR}; + # Make build-time container writes succeed by directing them to a tmpfs. + # NOTE: also tried a tmpfs overlay on all of ${SCRIPT_DIR}; # but inotify events for HMR don't propagate in that case; # and per https://github.com/vercel/next.js/issues/80665, polling doesn't work. - for f in node_modules collab-server/node_modules vscode-workbench/node_modules .next package.json package-lock.json next-env.d.ts; do - mkdir -p $(dirname "/tmp/workbench.tmpfs/$f") - cp -r "${SCRIPT_DIR}/$f" "/tmp/workbench.tmpfs/$f" + mkdir -p /tmp/workbench.tmpfs + mountpoint -q /tmp/workbench.tmpfs || mount -t tmpfs tmpfs /tmp/workbench.tmpfs + for d in node_modules collab-server/node_modules vscode-workbench/node_modules .next; do + mkdir -p "/tmp/workbench.tmpfs/$d.upper" "/tmp/workbench.tmpfs/$d.work" + mount -t overlay overlay \ + -o "lowerdir=${SCRIPT_DIR}/$d,upperdir=/tmp/workbench.tmpfs/$d.upper,workdir=/tmp/workbench.tmpfs/$d.work" \ + "${SCRIPT_DIR}/$d" + done + for f in package.json package-lock.json next-env.d.ts; do + cp "${SCRIPT_DIR}/$f" "/tmp/workbench.tmpfs/$f" mount --bind "/tmp/workbench.tmpfs/$f" "${SCRIPT_DIR}/$f" done @@ -57,3 +64,6 @@ trap 'kill $APP_PID $NGINX_PID 2>/dev/null' EXIT echo "[start.sh] Nginx listening on http://localhost:3000" wait -n $APP_PID $NGINX_PID + +# Show oom-killer events from the last 10 seconds, in case that is what caused us to exit +dmesg --ctime --since '10 sec ago' 2>/dev/null | grep --ignore-case 'killed process' | tail -5 \ No newline at end of file