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..2798fea7 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().then(tc => tc.toReversed()) 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..3e1dbd96 --- /dev/null +++ b/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 { + 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 }, + }) +}