feat: toolchain management

shared/shared.ts

@@ -36,6 +36,17 @@ export const zValidateProjectName = z
   .regex(ALPHANUM_NAME_RE, 'Invalid project name')
 export const zTemplateId = z.string().regex(TEMPLATE_ID_RE, 'Invalid template ID')
 
+/**
+ * Expected form of a toolchain (not necessarily exhaustive, must be command-line-argument-safe)
+ * Examples: `lean4`, `leanprover/lean4:v4.32.1`, `leanprover/lean4-nightly:nightly-2026-08-27`
+ */
+export const EXPECTED_TOOLCHAIN_ID_RE = /^[a-z][a-z0-9:/_.-]*$/
+
+export const LEAN_STABLE_VERSION_RE = /^v4\.[0-9]+\.[0-9]+$/
+export const LEAN_BETA_VERSION_RE = /^v4\.[0-9]+\.[0-9]+-rc[0-9]+$/
+export const LEAN_NIGHTLY_VERSION_RE = /^nightly-[0-9-]+$/
+
+/** Matches stable or beta Lean versions (not nightly) */
 export const LEAN_VERSION_RE = /^v4\.\d+\.\d+(-rc\d+)?$/
 
 /** Metadata of a Lean Workbench project workspace. */

src/app/admin/actions.ts

@@ -3,14 +3,25 @@
 import { execFileSync } from 'node:child_process'
 import fs from 'node:fs/promises'
 
-import { zProjectId, zTemplateId, zUserId, zUserName, zValidateUserName } from '@leanprover/workbench-shared'
+import {
+  EXPECTED_TOOLCHAIN_ID_RE,
+  LEAN_BETA_VERSION_RE,
+  LEAN_NIGHTLY_VERSION_RE,
+  LEAN_STABLE_VERSION_RE,
+  zProjectId,
+  zTemplateId,
+  zUserId,
+  zUserName,
+  zValidateUserName,
+} from '@leanprover/workbench-shared'
 import { getDataDir, getUserRootDir, getWorkspacesDir } from '@leanprover/workbench-shared/node'
 import z from 'zod'
 
 import { initAuth, requireAdmin } from '@/lib/server/auth'
 import { getConfig, saveConfig, zGithubAuthConfig } from '@/lib/server/config'
 import { getDb } from '@/lib/server/db'
 import { getEditorSessionManager } from '@/lib/server/editorSessions'
+import { elanUninstall, startElanInstall } from '@/lib/server/elan'
 import { readTemplateMetadata, saveTemplateMetadata, type TemplateMetadata } from '@/lib/server/projectTemplate'
 import { getTrackedCommandState } from '@/lib/server/trackedCommand'
 import { serverAction, submitAction } from '@/lib/server/util'
@@ -277,3 +288,40 @@ export async function isTrackedCommandAvailable(key: string) {
   await requireAdmin()
   return !!getTrackedCommandState(key)
 }
+
+// -- Toolchain management
+
+export const uninstallToolchainVersion = submitAction(
+  z.object({ toolchain: z.string().regex(EXPECTED_TOOLCHAIN_ID_RE) }),
+  async ({ toolchain }) => {
+    await requireAdmin()
+    try {
+      const output = await elanUninstall(toolchain)
+      if (output.length === 0) return { ok: 'elan succeeded with no output' }
+      const [_all, _info, info] = output[output.length - 1]!.match(/^(info: )?(.*)$/)!
+      return { ok: info }
+    } catch (e) {
+      return { error: e instanceof Error ? e.message : String(e) }
+    }
+  },
+)
+
+const zChannel = (channel: string, regex: RegExp) =>
+  z
+    .string()
+    .startsWith(`${channel} `)
+    .transform(s => s.slice(channel.length + 1))
+    .pipe(z.string().regex(regex))
+
+const zToolchainInstallRequest = z.object({
+  selectedToolchain: z.union([
+    zChannel('stable', LEAN_STABLE_VERSION_RE),
+    zChannel('beta', LEAN_BETA_VERSION_RE),
+    zChannel('nightly', LEAN_NIGHTLY_VERSION_RE),
+  ]),
+})
+
+export const doElanInstall = submitAction(zToolchainInstallRequest, async ({ selectedToolchain }) => {
+  await requireAdmin()
+  return { ok: !!startElanInstall(selectedToolchain) }
+})

src/app/admin/components/ToolchainManagement.tsx

@@ -0,0 +1,167 @@
+'use client'
+
+import {
+  EXPECTED_TOOLCHAIN_ID_RE,
+  LEAN_BETA_VERSION_RE,
+  LEAN_NIGHTLY_VERSION_RE,
+  LEAN_STABLE_VERSION_RE,
+} from '@leanprover/workbench-shared'
+import { useRouter } from 'next/navigation'
+import { use, useState } from 'react'
+import z from 'zod'
+
+import { doElanInstall, uninstallToolchainVersion } from '@/app/admin/actions'
+import CatchySuspense from '@/app/components/CatchySuspense'
+import TrackedCommandForm from '@/app/components/TrackedCommandForm'
+import { useServerAction, useThrowingSWR } from '@/lib/client/util'
+
+interface ToolchainManagementProps {
+  installedToolchainsPromise: Promise<string[]>
+}
+
+export function ToolchainManagement(props: ToolchainManagementProps) {
+  const router = useRouter()
+  return (
+    <section>
+      <h2>Lean Toolchains</h2>
+      <CatchySuspense loading={<p>Loading installed toolchains&hellip;</p>}>
+        <ToolchainManagementList {...props} />
+      </CatchySuspense>
+      <TrackedCommandForm
+        streamCommandKey='elan'
+        trackedCommandAction={doElanInstall}
+        title='+ New Toolchain'
+        successAction={() => router.refresh()}
+      >
+        <CatchySuspense loading={<p>Loading available toolchains&hellip;</p>}>
+          <NewToolchainForm />
+        </CatchySuspense>
+      </TrackedCommandForm>
+    </section>
+  )
+}
+
+function ToolchainManagementList(props: ToolchainManagementProps) {
+  const installedToolchains = use(props.installedToolchainsPromise)
+  if (installedToolchains.length === 0) return <p className='empty'>No installed toolchains.</p>
+  return (
+    <ul className='project-list'>
+      {installedToolchains.map(toolchain => (
+        <ToolchainRow key={toolchain} toolchain={toolchain} />
+      ))}
+    </ul>
+  )
+}
+
+function ToolchainRow(props: { toolchain: string }) {
+  const router = useRouter()
+  const [confirm, setConfirm] = useState(false)
+  const [error, action, pending] = useServerAction(uninstallToolchainVersion, () => {
+    router.refresh()
+  })
+  return (
+    <li>
+      <form className='simple-action-form' action={action}>
+        <div style={{ gridArea: 'name' }}>{props.toolchain}</div>
+        <input type='hidden' name='toolchain' value={props.toolchain} />
+        {EXPECTED_TOOLCHAIN_ID_RE.test(props.toolchain) /* prevent uninstall of weird-enough-named toolchains */ && (
+          <div className='actions' style={{ gridArea: 'actions' }}>
+            {!confirm && (
+              <button type='button' onClick={() => setConfirm(true)}>
+                Remove Toolchain
+              </button>
+            )}
+            {confirm && (
+              <>
+                <button className='delete' disabled={pending} type='submit'>
+                  Confirm Removing Toolchain
+                </button>
+                <button disabled={pending} type='button' onClick={() => setConfirm(false)}>
+                  Cancel
+                </button>
+              </>
+            )}
+          </div>
+        )}
+        <div style={{ gridArea: 'error', color: '#f00' }}>{error}</div>
+      </form>
+    </li>
+  )
+}
+
+const zLeanRelease = z.object({ name: z.string(), created_at: z.iso.datetime() })
+const zLeanReleases = z.object({
+  version: z.literal('1'),
+  stable: z.array(zLeanRelease.transform(tc => ({ type: 'stable' as const, ...tc }))),
+  beta: z.array(zLeanRelease.transform(tc => ({ type: 'beta' as const, ...tc }))),
+  nightly: z.array(zLeanRelease.transform(tc => ({ type: 'nightly' as const, ...tc }))),
+})
+
+function NewToolchainForm() {
+  const { data: toolchainsAvailable } = useThrowingSWR(
+    'release.llo',
+    async () => {
+      const res = await fetch('https://release.lean-lang.org')
+      if (!res.ok) throw new Error(`release.lean-lang.org returned error (${res.status})`)
+      return zLeanReleases.parse(await res.json())
+    },
+    { suspense: true, revalidateIfStale: false, revalidateOnFocus: false, revalidateOnReconnect: false },
+  )
+
+  const [stable, setStable] = useState(true)
+  const [beta, setBeta] = useState(true)
+  const [nightly, setNightly] = useState(false)
+  const count = (stable ? 1 : 0) + (beta ? 1 : 0) + (nightly ? 1 : 0)
+
+  const all = [
+    stable ? toolchainsAvailable.stable.filter(tc => LEAN_STABLE_VERSION_RE.test(tc.name)) : [],
+    beta ? toolchainsAvailable.beta.filter(tc => LEAN_BETA_VERSION_RE.test(tc.name)) : [],
+    nightly ? toolchainsAvailable.nightly.filter(tc => LEAN_NIGHTLY_VERSION_RE.test(tc.name)) : [],
+  ]
+    .flat()
+    .toSorted((a, b) => (a.created_at > b.created_at ? -1 : a.created_at < b.created_at ? 1 : 0))
+
+  return (
+    <>
+      <div className='check-seq'>
+        <label>
+          <input
+            id='tc-stable'
+            type='checkbox'
+            checked={stable}
+            disabled={stable && count === 1}
+            onChange={() => setStable(s => !s)}
+          />
+          Stable
+        </label>
+        <label>
+          <input
+            id='tc-beta'
+            type='checkbox'
+            checked={beta}
+            disabled={beta && count === 1}
+            onChange={() => setBeta(s => !s)}
+          />
+          Beta
+        </label>
+        <label>
+          <input
+            id='tc-nightly'
+            type='checkbox'
+            checked={nightly}
+            disabled={nightly && count === 1}
+            onChange={() => setNightly(s => !s)}
+          />
+          Nightly
+        </label>
+      </div>
+      <select name='selectedToolchain' defaultValue={`stable ${toolchainsAvailable.stable[0]?.name}`}>
+        {all.map(({ type, name }) => (
+          <option key={`${type} ${name}`} value={`${type} ${name}`}>
+            {name}
+          </option>
+        ))}
+      </select>
+    </>
+  )
+}

src/app/admin/page.tsx

@@ -1,4 +1,5 @@
 import { requireAdmin } from '@/lib/server/auth'
+import { listInstalledToolchains } from '@/lib/server/elan'
 import { listTemplates } from '@/lib/server/projectTemplate'
 
 import { fetchHealth } from './actions'
@@ -7,12 +8,14 @@ import { HealthMonitor } from './components/HealthMonitor'
 import { OAuthConfig } from './components/OAuthConfig'
 import { SessionViewer } from './components/SessionViewer'
 import { TemplateManagement } from './components/TemplateManagement'
+import { ToolchainManagement } from './components/ToolchainManagement'
 import { UserManagement } from './components/UserManagement'
 
 export const instant = false
 export default async function AdminPage() {
   await requireAdmin()
   const templates = listTemplates()
+  const installedToolchains = listInstalledToolchains().then(tc => tc.toReversed())
   const systemHealth = fetchHealth()
 
   return (
@@ -23,6 +26,7 @@ export default async function AdminPage() {
       <SessionViewer />
       <AccessControl />
       <HealthMonitor systemHealth={systemHealth} />
+      <ToolchainManagement installedToolchainsPromise={installedToolchains} />
       <TemplateManagement templates={templates} />
     </div>
   )

src/lib/server/elan.ts

@@ -0,0 +1,54 @@
+import { execFile } from 'node:child_process'
+import path from 'node:path'
+import { promisify } from 'node:util'
+
+import { getElanDir } from '@leanprover/workbench-shared/node'
+
+import { startTrackedCommand } from './trackedCommand'
+
+const exec = promisify(execFile)
+
+const getElanBin = () => path.join(getElanDir(), 'bin', 'elan')
+
+/**
+ * Queries `elan` for a list of installed toolchains.
+ *
+ * Results for normally-installed release or nightly toolchains are in long-form, e.g.
+ * `leanprover/lean4-nightly:nightly-2026-08-27` or `leanprover/lean4:v4.32.2`.
+ * The `leanprover/lean4` part is the "origin" (see
+ * https://lean-lang.org/doc/reference/latest/Build-Tools-and-Distribution/Managing-Toolchains-with-Elan/)
+ */
+export async function listInstalledToolchains(): Promise<string[]> {
+  const ELAN_HOME = getElanDir()
+  const { stderr, stdout } = await exec(getElanBin(), ['toolchain', 'list'], {
+    env: { ...process.env, ELAN_HOME },
+  })
+  // a successful `elan toolchain list` prints only to standard output
+  if (stderr.trim().length !== 0) throw new Error(stderr)
+  if (stdout.trim() === 'no installed toolchains') return []
+  return stdout
+    .split('\n')
+    .map(tc => tc.trim())
+    .filter(tc => tc.length > 0)
+}
+
+export async function elanUninstall(leanVersion: string) {
+  const ELAN_HOME = getElanDir()
+  const { stderr, stdout } = await exec(getElanBin(), ['toolchain', 'uninstall', leanVersion], {
+    env: { ...process.env, ELAN_HOME },
+  })
+  // a successful `elan toolchain uninstall ...` prints only to standard error
+  if (stdout.trim().length !== 0) throw new Error(stdout)
+
+  return stderr
+    .split('\n')
+    .map(tc => tc.trim())
+    .filter(tc => tc.length > 0)
+}
+
+export function startElanInstall(leanVersion: string) {
+  const ELAN_HOME = getElanDir()
+  return startTrackedCommand('elan', getElanBin(), ['toolchain', 'install', leanVersion], {
+    env: { ...process.env, ELAN_HOME },
+  })
+}