feat: let ordinary users watch tracked commands

src/app/admin/actions.ts

@@ -30,7 +30,6 @@ import {
   startSchemaTemplate,
   type TemplateMetadata,
 } from '@/lib/server/projectTemplate'
-import { getTrackedCommandState } from '@/lib/server/trackedCommand'
 import { serverAction, submitAction } from '@/lib/server/util'
 import { type ActionResponse } from '@/lib/util'
 
@@ -300,18 +299,6 @@ export const doTemplateCreation = submitAction(
   },
 )
 
-// -- Tracked command infrastructure
-
-export async function isTrackedCommandRunning(key: string) {
-  await requireAdmin()
-  return getTrackedCommandState(key)?.status === 'running'
-}
-
-export async function isTrackedCommandAvailable(key: string) {
-  await requireAdmin()
-  return !!getTrackedCommandState(key)
-}
-
 // -- Toolchain management
 
 export const uninstallToolchainVersion = submitAction(

src/app/admin/components/TemplateManagement.tsx

@@ -26,6 +26,7 @@ export function TemplateManagement(props: TemplateManagementProps) {
       <TrackedCommandForm
         disabled={installedStandardToolchains.length === 0}
         streamCommandKey='create-template'
+        scope='admin'
         trackedCommandAction={doTemplateCreation}
         title='+ Create template'
         successAction={() => router.refresh()}

src/app/admin/components/ToolchainManagement.tsx

@@ -29,6 +29,7 @@ export function ToolchainManagement(props: ToolchainManagementProps) {
       </CatchySuspense>
       <TrackedCommandForm
         streamCommandKey='elan'
+        scope='admin'
         trackedCommandAction={doElanInstall}
         title='+ New Toolchain'
         successAction={() => router.refresh()}

src/app/api/admin/tracked-command/[key]/route.ts

@@ -1,82 +1,18 @@
 import { requireAdmin } from '@/lib/server/auth'
 import { getTrackedCommandState } from '@/lib/server/trackedCommand'
-import { type TrackedCommandEvent, type TrackedCommandExit } from '@/lib/util'
-
-const STREAMING_HEADERS = {
-  'Content-Type': 'text/event-stream',
-  'Cache-Control': 'no-cache',
-  Connection: 'keep-alive',
-  'X-Accel-Buffering': 'no',
-} as const
+import { TRACKED_COMMAND_STREAMING_HEADERS, trackedCommandEventStream } from '@/lib/server/trackedCommandStream'
 
 // Separately handle HEAD without creating a response stream
 export async function HEAD() {
   await requireAdmin()
-  return new Response(null, { headers: STREAMING_HEADERS })
+  return new Response(null, { headers: TRACKED_COMMAND_STREAMING_HEADERS })
 }
 
-/**
- * Return server-sent events for a streaming command
- */
+/** Server-sent events for any tracked command, for administrators.
+ * These commands run unsandboxed as the server user,
+ * so their output is not shown to anybody else. */
 export async function GET(request: Request, context: RouteContext<'/api/admin/tracked-command/[key]'>) {
   await requireAdmin()
   const { key } = await context.params
-  const encoder = new TextEncoder()
-
-  return new Response(
-    new ReadableStream({
-      start(controller) {
-        const send = (msg: TrackedCommandEvent) => {
-          controller.enqueue(encoder.encode(`data: ${JSON.stringify(msg)}\n\n`))
-        }
-
-        const state = getTrackedCommandState(key)
-        if (!state) {
-          send({ type: 'no-stream' })
-          controller.close()
-          return
-        }
-
-        // Replay previous progress
-        for (const data of state.output) send({ type: 'data', data })
-
-        // Option 1 of 2: synchronously exit
-        if (state.status === 'done') {
-          send({ type: 'exit', exit: state.exit })
-          controller.close()
-          return
-        }
-
-        // Option 2 of 2: stream the rest of the output as it happens
-        const emitter = state.emitter
-
-        // nginx will close connections that don't send some message in 60s
-        const keepAliveInterval = setInterval(() => {
-          controller.enqueue(encoder.encode(':\n'))
-        }, 10_000)
-
-        const onData = (data: string) => {
-          send({ type: 'data', data })
-        }
-        emitter.on('data', onData)
-
-        const onExit = (exit: TrackedCommandExit) => {
-          send({ type: 'exit', exit })
-          cleanup()
-        }
-        emitter.on('exit', onExit)
-
-        const cleanup = () => {
-          clearInterval(keepAliveInterval)
-          emitter.off('data', onData)
-          emitter.off('exit', onExit)
-          request.signal.removeEventListener('abort', cleanup) // avoids double-calling cleanup
-          controller.close()
-        }
-        request.signal.addEventListener('abort', cleanup, { once: true })
-        if (request.signal.aborted) cleanup() // oops, the connection was closed when the function started
-      },
-    }),
-    { headers: STREAMING_HEADERS },
-  )
+  return trackedCommandEventStream(request, getTrackedCommandState(key))
 }

src/app/api/tracked-command/[key]/route.ts

@@ -0,0 +1,17 @@
+import { requireAuth } from '@/lib/server/auth'
+import { getUserTrackedCommandState } from '@/lib/server/trackedCommand'
+import { TRACKED_COMMAND_STREAMING_HEADERS, trackedCommandEventStream } from '@/lib/server/trackedCommandStream'
+
+// Separately handle HEAD without creating a response stream
+export async function HEAD() {
+  await requireAuth()
+  return new Response(null, { headers: TRACKED_COMMAND_STREAMING_HEADERS })
+}
+
+/** Server-sent events for a tracked command the requesting user started themselves.
+ * Admin-owned commands are unreachable here, whoever is asking. */
+export async function GET(request: Request, context: RouteContext<'/api/tracked-command/[key]'>) {
+  const { user } = await requireAuth()
+  const { key } = await context.params
+  return trackedCommandEventStream(request, getUserTrackedCommandState(user, key))
+}

src/app/components/SimpleTTY.tsx

@@ -4,10 +4,17 @@ import '@/css/simpletty.css'
 
 import { type ReactNode, useCallback, useEffect, useLayoutEffect, useMemo, useRef, useState } from 'react'
 
-import { type TrackedCommandEvent, type TrackedCommandExit, zTrackedCommandEvent } from '@/lib/util'
+import {
+  type TrackedCommandEvent,
+  type TrackedCommandExit,
+  type TrackedCommandScope,
+  trackedCommandStreamUrl,
+  zTrackedCommandEvent,
+} from '@/lib/util'
 
 interface SimpleTTYProps {
   streamingCommandKey: string
+  scope: TrackedCommandScope
   onExit?: (exit: TrackedCommandExit) => void
 }
 
@@ -49,7 +56,11 @@ type SimpleTTYState = (
  * Custom hook: establish and maintain a connection to the streaming command source for a given
  * key, and return a SimpleTTYState and bonus unexpectedError signal
  */
-function useTerminalConnection(streamingCommandKey: string, onExit?: (exit: TrackedCommandExit) => void) {
+function useTerminalConnection(
+  streamingCommandKey: string,
+  scope: TrackedCommandScope,
+  onExit?: (exit: TrackedCommandExit) => void,
+) {
   const incomingEventMessages = useRef<TrackedCommandEvent[]>([])
   const animationRequest = useRef<ReturnType<typeof requestAnimationFrame> | undefined>(undefined)
   const [state, setState] = useState<SimpleTTYState>({
@@ -159,7 +170,7 @@ function useTerminalConnection(streamingCommandKey: string, onExit?: (exit: Trac
   }, [])
 
   useEffect(() => {
-    const source = new EventSource(`/api/admin/tracked-command/${streamingCommandKey}`)
+    const source = new EventSource(trackedCommandStreamUrl(scope, streamingCommandKey))
     source.onmessage = event => {
       try {
         const data = zTrackedCommandEvent.parse(
@@ -204,14 +215,14 @@ function useTerminalConnection(streamingCommandKey: string, onExit?: (exit: Trac
       incomingEventMessages.current = []
       setState({ type: 'loading', buffer: [], unexpectedError: false, progress: null })
     }
-  }, [streamingCommandKey, updater])
+  }, [scope, streamingCommandKey, updater])
 
   return state
 }
 
-function SimpleTTYSession({ streamingCommandKey, reload, onExit }: SimpleTTYProps & { reload: () => void }) {
+function SimpleTTYSession({ streamingCommandKey, scope, reload, onExit }: SimpleTTYProps & { reload: () => void }) {
   const divRef = useRef<HTMLDivElement>(null)
-  const state = useTerminalConnection(streamingCommandKey, onExit)
+  const state = useTerminalConnection(streamingCommandKey, scope, onExit)
   const backscroll = useMemo(() => state.buffer.join('\n'), [state.buffer])
 
   // Auto-scroller for terminal

src/app/components/TrackedCommandForm.tsx

@@ -2,14 +2,15 @@
 
 import { type CSSProperties, type ReactNode, useEffect, useState } from 'react'
 
-import { isTrackedCommandAvailable, isTrackedCommandRunning } from '@/app/admin/actions'
 import ErrorBox from '@/app/components/ErrorBox'
 import SimpleTTY from '@/app/components/SimpleTTY'
 import { useServerAction, useThrowToBoundary } from '@/lib/client/util'
-import { type ActionResponse, type TrackedCommandExit } from '@/lib/util'
+import { isTrackedCommandAvailable, isTrackedCommandRunning } from '@/lib/server/actions'
+import { type ActionResponse, type TrackedCommandExit, type TrackedCommandScope } from '@/lib/util'
 
 interface TrackedCommandFormProps {
   streamCommandKey: string
+  scope: TrackedCommandScope
   style?: CSSProperties
   title: string
   children: ReactNode
@@ -28,7 +29,7 @@ type FormState =
   | { type: 'conflict' /* Submission blocked because a separate command-run started */ }
 
 /**
- * Present the admin user with a button labeled with the `title` prop.
+ * Present the user with a button labeled with the `title` prop.
  * That button can be expanded to present the body of a <form> (the element's children),
  * that gets submitted to the serverAction `trackedCommandAction`.
  *
@@ -49,6 +50,7 @@ type FormState =
  */
 export default function TrackedCommandForm({
   streamCommandKey,
+  scope,
   style,
   title,
   children,
@@ -68,13 +70,13 @@ export default function TrackedCommandForm({
   const { throwToBoundary } = useThrowToBoundary()
   useEffect(() => {
     if (disabled || !initiallyWatchingTTY) return
-    isTrackedCommandAvailable(streamCommandKey)
+    isTrackedCommandAvailable(scope, streamCommandKey)
       .then(isTTYAvailable => setState(isTTYAvailable ? { type: 'watching' } : { type: 'editing' }))
       .catch(throwToBoundary)
-  }, [disabled, initiallyWatchingTTY, streamCommandKey, throwToBoundary])
+  }, [disabled, initiallyWatchingTTY, scope, streamCommandKey, throwToBoundary])
   const setStateOpening = () => {
     setState({ type: 'opening' })
-    isTrackedCommandRunning(streamCommandKey)
+    isTrackedCommandRunning(scope, streamCommandKey)
       .then(isAlreadyRunning => setState(isAlreadyRunning ? { type: 'watching' } : { type: 'editing' }))
       .catch(throwToBoundary)
   }
@@ -106,6 +108,7 @@ export default function TrackedCommandForm({
         {titleNode}
         <SimpleTTY
           streamingCommandKey={streamCommandKey}
+          scope={scope}
           onExit={exit => {
             if (exit.type === 'success') successAction?.()
             setState({ type: 'watching', exit })

src/app/setup/SetupFlow.tsx

@@ -26,6 +26,7 @@ export default function SetupFlow({ baseUrl }: SetupFlowProps) {
   return (
     <TrackedCommandForm
       streamCommandKey='seed'
+      scope='admin'
       initiallyWatchingTTY
       title='Start Setup'
       trackedCommandAction={doSeed}

src/app/setup/actions.ts

@@ -28,7 +28,7 @@ export const doSeed = submitAction(
     const scriptsDir = path.join(process.cwd(), 'scripts') // scripts/ is a sibling directory
     const scriptsArgs = []
     if (installToolchain) scriptsArgs.push('--install-toolchain')
-    const emitter = startTrackedCommand('seed', path.join(scriptsDir, 'seed-volume.sh'), scriptsArgs)
+    const emitter = startTrackedCommand('seed', { kind: 'admin' }, path.join(scriptsDir, 'seed-volume.sh'), scriptsArgs)
 
     emitter?.on('exit', async exit => {
       // Note: success has already been reported to the client component;

src/lib/server/actions.ts

@@ -10,10 +10,12 @@ import { devModeEmail, devModePassword } from '@leanprover/workbench-shared'
 import { forbidden } from 'next/navigation'
 import z from 'zod'
 
-import { addEmailPasswordUser, getAuth, requireAuth } from '@/lib/server/auth'
+import { addEmailPasswordUser, getAuth, requireAdmin, requireAuth } from '@/lib/server/auth'
 import { getDb } from '@/lib/server/db'
+import { type TrackedCommandScope, zTrackedCommandScope } from '@/lib/util'
 
 import { isDevMode } from './config'
+import { getTrackedCommandState, getUserTrackedCommandState } from './trackedCommand'
 import { submitAction } from './util'
 
 /** Set `isAdmin` on the requesting user. Dev mode only. */
@@ -44,3 +46,26 @@ export const loginDevUser = submitAction(
   },
   { throwIfInvalid: true },
 )
+
+/** The tracked command that the requester may watch at {@link trackedCommandStreamUrl},
+ * under the same authorization as the route that would stream it. */
+async function probeTrackedCommand(rawScope: TrackedCommandScope, key: string) {
+  const scope = zTrackedCommandScope.parse(rawScope)
+  if (scope === 'admin') {
+    await requireAdmin()
+    return getTrackedCommandState(key)
+  }
+  const { user } = await requireAuth()
+  return getUserTrackedCommandState(user, key)
+}
+
+/** Whether a tracked command the requester may watch is currently running. */
+export async function isTrackedCommandRunning(scope: TrackedCommandScope, key: string) {
+  return (await probeTrackedCommand(scope, key))?.status === 'running'
+}
+
+/** Whether the requester has any tracked command output to watch under this key,
+ * running or finished. */
+export async function isTrackedCommandAvailable(scope: TrackedCommandScope, key: string) {
+  return !!(await probeTrackedCommand(scope, key))
+}

src/lib/server/elan.ts

@@ -48,7 +48,7 @@ export async function elanUninstall(leanVersion: string) {
 
 export function startElanInstall(leanVersion: string) {
   const ELAN_HOME = getElanDir()
-  return startTrackedCommand('elan', getElanBin(), ['toolchain', 'install', leanVersion], {
+  return startTrackedCommand('elan', { kind: 'admin' }, getElanBin(), ['toolchain', 'install', leanVersion], {
     env: { ...process.env, ELAN_HOME },
   })
 }

src/lib/server/projectTemplate.ts

@@ -159,5 +159,5 @@ export async function startSchemaTemplate(toolchain: string, schema: TemplateSch
       break
   }
 
-  return startTrackedCommand('create-template', path.join(scriptsDir, script), args)
+  return startTrackedCommand('create-template', { kind: 'admin' }, path.join(scriptsDir, script), args)
 }