feat: quality of life improvements

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'

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'

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'

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'

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'

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'

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'

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'

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<typeof setInterval> | 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, {

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<ActionRespons
   return { ok: true }
 }
 
-export async function startSeed(): Promise<ActionResponse<boolean>> {
-  return doStartSeed()
+export async function startSeed(leanVersion: string | undefined): Promise<ActionResponse<boolean>> {
+  return doStartSeed(leanVersion)
 }
 
 export async function fetchSetupStatus() {

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<string[]> {
+  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<string[]>([])
+  const [leanVersion, setLeanVersion] = useState<string | undefined>()
+  const { data: leanVersions } = useSWR('leanVersions', fetchLeanVersions)
   const logRef = useRef<HTMLDivElement>(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' && (
-            <button className='primary' disabled={!configSaved} onClick={handleStartSeed}>
-              {phase === 'error' ? 'Retry Setup' : 'Start Setup'}
-            </button>
+            <div style={{ display: 'flex', gap: '8px', alignItems: 'center' }}>
+              <button className='primary' disabled={!configSaved} onClick={handleStartSeed}>
+                {phase === 'error' ? 'Retry Setup' : 'Start Setup'}
+              </button>
+              with Lean version:
+              <select
+                value={leanVersion ?? ''}
+                onChange={e => setLeanVersion(e.target.value || undefined)}
+                disabled={!leanVersions}
+              >
+                <option>{leanVersions ? 'Latest' : 'Loading…'}</option>
+                {leanVersions?.map(v => (
+                  <option key={v} value={v}>
+                    {v}
+                  </option>
+                ))}
+              </select>
+            </div>
           )}
 
           {(phase === 'seeding' || phase === 'error') && progress.pct > 0 && (

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<Payload = void, T = void>(
+  fn: (payload: Payload) => Promise<ActionResponse<T>>,
+  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)
+}

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)}`)
       }

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,19 +31,22 @@ export function getSeedState(): Readonly<SeedState> {
   return seedState
 }
 
-export function startSeed(): ActionResponse<boolean> {
+export function startSeed(leanVersion: string | undefined): ActionResponse<boolean> {
   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
 
   // 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'],
   })
 

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<void>((_, 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.

src/lib/util.ts

@@ -1,16 +1,3 @@
-import { useActionState } from 'react'
-
 export type ActionResponse<T = void> = { ok: T } | { error: string }
 
-/** Returns `[error, dispatchAction, pending]`. */
-export function useServerAction<Payload = void, T = void>(
-  fn: (payload: Payload) => Promise<ActionResponse<T>>,
-  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+)?$/

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