From 47cab47c237d187d0a3e185ba7c0e63a709ac205 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Tue, 1 Sep 2026 20:03:54 -0400 Subject: [PATCH 1/5] feat: toolchain management Toolchains can be introduced with a second use of TrackedCommandForm, and modified with the same kind of inline modification form initially used for active editor sessions and duplciated for project templates --- shared/shared.ts | 11 ++ src/app/admin/actions.ts | 50 +++++- .../admin/components/ToolchainManagement.tsx | 167 ++++++++++++++++++ src/app/admin/page.tsx | 4 + src/lib/server/elan.ts | 50 ++++++ 5 files changed, 281 insertions(+), 1 deletion(-) create mode 100644 src/app/admin/components/ToolchainManagement.tsx create mode 100644 src/lib/server/elan.ts diff --git a/shared/shared.ts b/shared/shared.ts index 6fe82a5b..5ff95e0a 100644 --- a/shared/shared.ts +++ b/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. */ diff --git a/src/app/admin/actions.ts b/src/app/admin/actions.ts index 1f4a6bc3..54833879 100644 --- a/src/app/admin/actions.ts +++ b/src/app/admin/actions.ts @@ -3,7 +3,17 @@ 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' @@ -11,6 +21,7 @@ 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) } +}) diff --git a/src/app/admin/components/ToolchainManagement.tsx b/src/app/admin/components/ToolchainManagement.tsx new file mode 100644 index 00000000..2d5259ca --- /dev/null +++ b/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 +} + +export function ToolchainManagement(props: ToolchainManagementProps) { + const router = useRouter() + return ( +
+

Lean Toolchains

+ Loading installed toolchains…

}> + + + router.refresh()} + > + Loading available toolchains…

}> + + + +
+ ) +} + +function ToolchainManagementList(props: ToolchainManagementProps) { + const installedToolchains = use(props.installedToolchainsPromise) + if (installedToolchains.length === 0) return

No installed toolchains.

+ return ( + + ) +} + +function ToolchainRow(props: { toolchain: string }) { + const router = useRouter() + const [confirm, setConfirm] = useState(false) + const [error, action, pending] = useServerAction(uninstallToolchainVersion, () => { + router.refresh() + }) + return ( +
  • +
    +
    {props.toolchain}
    + + {EXPECTED_TOOLCHAIN_ID_RE.test(props.toolchain) /* prevent uninstall of weird-enough-named toolchains */ && ( +
    + {!confirm && ( + + )} + {confirm && ( + <> + + + + )} +
    + )} +
    {error}
    +
    +
    • + ) +} + +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 ( + <> +
    + + + +
    + + + ) +} diff --git a/src/app/admin/page.tsx b/src/app/admin/page.tsx index eb40382b..cb2e522c 100644 --- a/src/app/admin/page.tsx +++ b/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() const systemHealth = fetchHealth() return ( @@ -23,6 +26,7 @@ export default async function AdminPage() { + ) diff --git a/src/lib/server/elan.ts b/src/lib/server/elan.ts new file mode 100644 index 00000000..386041a5 --- /dev/null +++ b/src/lib/server/elan.ts @@ -0,0 +1,50 @@ +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`. + */ +export async function listInstalledToolchains(): Promise { + const ELAN_HOME = getElanDir() + const { stderr, stdout } = await exec(getElanBin(), ['toolchain', 'list'], { + env: { ...process.env, ELAN_HOME }, + }) + 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 }, + }) + 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 }, + }) +} From ad1b0525c594fa7ed47ba0fd29bc94e36107cc57 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Wed, 2 Sep 2026 21:43:13 -0400 Subject: [PATCH 2/5] Reverse order of toolchains --- src/app/admin/page.tsx | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/app/admin/page.tsx b/src/app/admin/page.tsx index cb2e522c..2798fea7 100644 --- a/src/app/admin/page.tsx +++ b/src/app/admin/page.tsx @@ -15,7 +15,7 @@ export const instant = false export default async function AdminPage() { await requireAdmin() const templates = listTemplates() - const installedToolchains = listInstalledToolchains() + const installedToolchains = listInstalledToolchains().then(tc => tc.toReversed()) const systemHealth = fetchHealth() return ( From 79b9d1cc5226a58bed5b19f065464ff98b7757c0 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Sun, 6 Sep 2026 08:44:51 -0400 Subject: [PATCH 3/5] comment on stdout/stderr discrepancy --- src/lib/server/elan.ts | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/lib/server/elan.ts b/src/lib/server/elan.ts index 386041a5..95339306 100644 --- a/src/lib/server/elan.ts +++ b/src/lib/server/elan.ts @@ -21,6 +21,7 @@ export async function listInstalledToolchains(): Promise { const { stderr, stdout } = await exec(getElanBin(), ['toolchain', 'list'], { env: { ...process.env, ELAN_HOME }, }) + // a successful `elan toolchain list` prints nothing on standard output if (stderr.trim().length !== 0) throw new Error(stderr) if (stdout.trim() === 'no installed toolchains') return [] return stdout @@ -34,6 +35,7 @@ export async function elanUninstall(leanVersion: string) { const { stderr, stdout } = await exec(getElanBin(), ['toolchain', 'uninstall', leanVersion], { env: { ...process.env, ELAN_HOME }, }) + // a successful `elan toolchain uninstall ...` produces nothing on standard error if (stdout.trim().length !== 0) throw new Error(stdout) return stderr From 5cd28852e4a1e8644b1815822856b583a155b752 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Tue, 8 Sep 2026 17:01:49 -0400 Subject: [PATCH 4/5] fix: had it exactly backwards --- src/lib/server/elan.ts | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/lib/server/elan.ts b/src/lib/server/elan.ts index 95339306..b0306b9f 100644 --- a/src/lib/server/elan.ts +++ b/src/lib/server/elan.ts @@ -21,7 +21,7 @@ export async function listInstalledToolchains(): Promise { const { stderr, stdout } = await exec(getElanBin(), ['toolchain', 'list'], { env: { ...process.env, ELAN_HOME }, }) - // a successful `elan toolchain list` prints nothing on standard output + // 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 @@ -35,7 +35,7 @@ export async function elanUninstall(leanVersion: string) { const { stderr, stdout } = await exec(getElanBin(), ['toolchain', 'uninstall', leanVersion], { env: { ...process.env, ELAN_HOME }, }) - // a successful `elan toolchain uninstall ...` produces nothing on standard error + // a successful `elan toolchain uninstall ...` prints only to standard error if (stdout.trim().length !== 0) throw new Error(stdout) return stderr From 69de54ce07affe14ea090ec9120f276d80090ecc Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Wed, 9 Sep 2026 12:54:19 -0400 Subject: [PATCH 5/5] add comment --- src/lib/server/elan.ts | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/lib/server/elan.ts b/src/lib/server/elan.ts index b0306b9f..3e1dbd96 100644 --- a/src/lib/server/elan.ts +++ b/src/lib/server/elan.ts @@ -15,6 +15,8 @@ const getElanBin = () => path.join(getElanDir(), 'bin', 'elan') * * 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 { const ELAN_HOME = getElanDir()