diff --git a/scripts/create-basic.sh b/scripts/create-basic.sh new file mode 100755 index 00000000..5a15b26b --- /dev/null +++ b/scripts/create-basic.sh @@ -0,0 +1,59 @@ +#!/bin/bash +# Create a minimal Lean template +# usage: create-basic.sh WORK_DIR TEMPLATE_ID TOOLCHAIN +# +# example: +# create-basic.sh /tmp/abcd new-template leanprover/lean4:v4.32.0 +# +# expects $WORK_DIR/build/Main.lean must exist + +set -euo pipefail + +ROOT=${LEAN_WORKBENCH_DATA_DIR:?No data directory was specified} +export ELAN_HOME="$ROOT/elan" +export PATH="$ELAN_HOME/bin:$PATH" + +WORK_DIR="$1"; shift 1 +TEMPLATE_ID="$1"; shift 1 +TOOLCHAIN="$1"; shift 1 + +trap 'rm -rf "$WORK_DIR"' EXIT + +if [ -d "$ROOT/templates/$TEMPLATE_ID" ]; then + echo "ERROR: template '$TEMPLATE_ID' already exists" + exit 1 +fi + +echo "[[ progress 1/4 Constructing project ]]" +BUILD_DIR="$WORK_DIR/build" +cd "$BUILD_DIR" + +echo "$TOOLCHAIN" > lean-toolchain + +cat > lakefile.toml < lean-toolchain + +cat > lakefile.toml < "$PACKAGE_SET_DIR/packages.txt" + +echo "[[ progress 7/8 Constructing template ]]" +TEMPLATE_DIR="$WORK_DIR/template" +mkdir -p "$TEMPLATE_DIR" + +mv "$BUILD_DIR/lean-toolchain" "$TEMPLATE_DIR/" +mv "$BUILD_DIR/lakefile.toml" "$TEMPLATE_DIR/" +mv "$BUILD_DIR/lake-manifest.json" "$TEMPLATE_DIR/" +mv "$BUILD_DIR/Main.lean" "$TEMPLATE_DIR/" +mv "$BUILD_DIR/metadata.json" "$TEMPLATE_DIR/" + +echo "[[ progress 8/8 Placing package set and template ]]" +# NOTE: it's possible for the first placement to succeed and the second to fail; +# the package set placement won't be rolled back if this happens. +PACKAGE_SET_PLACED="$ROOT/package-sets/$TEMPLATE_ID" +TEMPLATE_PLACED="$ROOT/templates/$TEMPLATE_ID" + +mv "$PACKAGE_SET_DIR" "$PACKAGE_SET_PLACED" +mv "$TEMPLATE_DIR" "$TEMPLATE_PLACED" + +# --- Summary --- +OLEAN_COUNT=$(find "$PACKAGE_SET_PLACED" -name "*.olean" | wc -l) +TOTAL_SIZE=$(du -sh "$PACKAGE_SET_PLACED" | cut -f1) +PKG_COUNT=$(wc -l < "$PACKAGE_SET_PLACED/packages.txt") + +echo "" +echo "[create-template] Done." +echo " Package set: $PACKAGE_SET_PLACED" +echo " Template: $TEMPLATE_PLACED" +echo " Packages: $PKG_COUNT" +echo " .olean files: $OLEAN_COUNT" +echo " Total size: $TOTAL_SIZE" diff --git a/shared/shared.ts b/shared/shared.ts index 5ff95e0a..9d09fef0 100644 --- a/shared/shared.ts +++ b/shared/shared.ts @@ -42,12 +42,59 @@ export const zTemplateId = z.string().regex(TEMPLATE_ID_RE, 'Invalid template ID */ export const EXPECTED_TOOLCHAIN_ID_RE = /^[a-z][a-z0-9:/_.-]*$/ +/** + * Expected form of a standard installed stable/beta/nightly toolchain. + * - If `match[1] === 'lean'`, + * then `match[2]` is a candidate for a tag of . + * - If `match[1] === 'lean4-nightly'`, + * then `match[2]` is a candidate for a tag of + */ +export const STANDARD_TOOLCHAIN_ID_RE = /^leanprover\/(lean4|lean4-nightly):([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+)?$/ +export const LEAN_VERSION_RE = /^v4\.(\d+)\.(\d+)(-rc(\d+))?$/ + +/** + * Compares two lean versions matching `LEAN_VERSION_RE`. + * + * ``` + * leanVersionCompare("v4.1.3", "v4.32.2") < 0 + * leanVersionCompare("v4.30.4", "v4.31.0-rc1") < 0 + * leanVersionCompare("v4.31.1-rc10", "v4.31.0-rc9") > 0 + * ``` + */ +export function leanVersionCompare(v1: string, v2: string) { + const m1 = v1.match(LEAN_VERSION_RE) + const m2 = v2.match(LEAN_VERSION_RE) + if (!m1 || !m2) throw new Error(`Either ${v1} and/or ${v2} are not valid Lean version numbers`) + const [primary1, primary2] = [Number(m1[1]), Number(m2[1])] + if (primary1 !== primary2) return primary1 - primary2 + const [secondary1, secondary2] = [Number(m1[2]), Number(m2[2])] + if (secondary1 !== secondary2) return secondary1 - secondary2 + if (!m1[4]) return m2[4] ? 1 : 0 + if (!m2[4]) return -1 + return Number(m1[4]) - Number(m2[4]) +} + +/** + * Does a toolchain match STANDARD_TOOLCHAIN_ID_RE and do Lean, Mathlib, and CSLib + * work with the lean module system at that version? + * + * For stable releases, returns true for v4.27.0 and beyond. + * For nighties, very conservatively returns true in February 2026 and beyond. + */ +export function toolchainHasModules(toolchain: string) { + const m = toolchain.match(STANDARD_TOOLCHAIN_ID_RE) + if (!m) return false + if (m[1] === 'lean4') { + return LEAN_VERSION_RE.test(m[2]!) && leanVersionCompare(m[2]!, 'v4.27.0') >= 0 + } + return LEAN_NIGHTLY_VERSION_RE.test(m[2]!) && m[2]! >= 'nightly-2026-02-01' +} /** Metadata of a Lean Workbench project workspace. */ export type WorkspaceMetadata = z.infer diff --git a/src/app/admin/actions.ts b/src/app/admin/actions.ts index 54833879..dc1469df 100644 --- a/src/app/admin/actions.ts +++ b/src/app/admin/actions.ts @@ -8,6 +8,7 @@ import { LEAN_BETA_VERSION_RE, LEAN_NIGHTLY_VERSION_RE, LEAN_STABLE_VERSION_RE, + STANDARD_TOOLCHAIN_ID_RE, zProjectId, zTemplateId, zUserId, @@ -22,7 +23,13 @@ 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 { + getAvailableTemplateSchemas, + readTemplateMetadata, + saveTemplateMetadata, + 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' @@ -279,6 +286,32 @@ export const editTemplateMetadata = submitAction( }, ) +export async function availableTemplateSchemas(toolchain: string) { + await requireAdmin() + return getAvailableTemplateSchemas(toolchain) +} + +const zTemplateCreation = z.object({ + toolchain: z.string().regex(STANDARD_TOOLCHAIN_ID_RE), + schema: z.enum(['basic', 'mathlib', 'cslib']), +}) + +export const doTemplateCreation = submitAction( + zTemplateCreation, + async ({ toolchain, schema }): Promise> => { + await requireAdmin() + + try { + const emitter = await startSchemaTemplate(toolchain, schema) + return { ok: !!emitter } + } catch (e) { + return { error: e instanceof Error ? e.message : String(e) } + } + }, +) + +// -- Tracked command infrastructure + export async function isTrackedCommandRunning(key: string) { await requireAdmin() return getTrackedCommandState(key)?.status === 'running' diff --git a/src/app/admin/components/TemplateManagement.tsx b/src/app/admin/components/TemplateManagement.tsx index fcd7cf1e..23f9aa23 100644 --- a/src/app/admin/components/TemplateManagement.tsx +++ b/src/app/admin/components/TemplateManagement.tsx @@ -1,32 +1,47 @@ 'use client' +import { STANDARD_TOOLCHAIN_ID_RE, toolchainHasModules } from '@leanprover/workbench-shared' +import { useRouter } from 'next/navigation' import { use, useState } from 'react' -import { editTemplateMetadata } from '@/app/admin/actions' +import { availableTemplateSchemas, doTemplateCreation, editTemplateMetadata } from '@/app/admin/actions' import CatchySuspense from '@/app/components/CatchySuspense' -import { useServerAction } from '@/lib/client/util' +import TrackedCommandForm from '@/app/components/TrackedCommandForm' +import { useServerAction, useThrowingSWR } from '@/lib/client/util' import { type TemplateInfo } from '@/lib/server/projectTemplate' interface TemplateManagementProps { - templates: Promise + templatesPromise: Promise + installedToolchainsPromise: Promise } export function TemplateManagement(props: TemplateManagementProps) { + const router = useRouter() + const templates = use(props.templatesPromise) + const installedStandardToolchains = use(props.installedToolchainsPromise).filter(tc => toolchainHasModules(tc)) + return ( -
-

Project Templates

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

}> + + + + ) } -function TemplateManagementList(props: TemplateManagementProps) { - const templates = use(props.templates) +function TemplateManagementList(props: { templates: TemplateInfo[] }) { return (
    - {templates.map(template => ( + {props.templates.map(template => ( ))}
@@ -106,3 +121,57 @@ function TemplateRow(props: TemplateInfo) { ) } + +export function TemplateCreationForm(props: { installedToolchains: string[] }) { + const [toolchain, setToolchain] = useState(props.installedToolchains[0]!) + const [_toolchain, namespace, tag] = toolchain.match(STANDARD_TOOLCHAIN_ID_RE)! + const { data: schemas } = useThrowingSWR( + `toolchain-schema-${namespace}-${tag}`, + async () => { + const schemaIds = await availableTemplateSchemas(toolchain) + return schemaIds.map(key => { + switch (key) { + case 'basic': + return { key, name: 'Basic Lean template' } + case 'mathlib': + return { key, name: 'Mathlib template' } + case 'cslib': + return { key, name: 'CSLib template' } + } + }) + }, + { + fallbackData: [{ key: 'basic', name: 'Loading…' } as const], + revalidateIfStale: false, + revalidateOnFocus: false, + revalidateOnReconnect: false, + }, + ) + + return ( + <> + + + + ) +} diff --git a/src/app/admin/components/ToolchainManagement.tsx b/src/app/admin/components/ToolchainManagement.tsx index 2d5259ca..33cb3348 100644 --- a/src/app/admin/components/ToolchainManagement.tsx +++ b/src/app/admin/components/ToolchainManagement.tsx @@ -155,7 +155,7 @@ function NewToolchainForm() { Nightly - {all.map(({ type, name }) => (