From a8b66d621d9f6249677237dc8a9431c655fd4048 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Wed, 2 Sep 2026 21:47:15 -0400 Subject: [PATCH 01/10] feat(admin): simplify initialization flow --- scripts/seed-volume.sh | 162 ++++-------------- src/app/[userName]/NewProjectForm.tsx | 6 +- src/app/[userName]/actions.ts | 28 ++- src/app/admin/actions.ts | 2 - .../admin/components/TemplateManagement.tsx | 20 +-- src/app/setup/SetupFlow.tsx | 118 +++---------- src/app/setup/actions.ts | 64 ++++--- src/app/setup/page.tsx | 12 +- src/lib/server/projectTemplate.ts | 2 +- src/lib/server/seed.ts | 46 ----- src/prisma/schema.prisma | 2 +- templates/hello/Main.lean | 2 - templates/hello/lakefile.toml | 2 - 13 files changed, 131 insertions(+), 335 deletions(-) delete mode 100644 src/lib/server/seed.ts delete mode 100644 templates/hello/Main.lean delete mode 100644 templates/hello/lakefile.toml diff --git a/scripts/seed-volume.sh b/scripts/seed-volume.sh index 5e1de806..86297361 100755 --- a/scripts/seed-volume.sh +++ b/scripts/seed-volume.sh @@ -22,25 +22,25 @@ usage() { cat <<'EOF' Usage: seed-volume.sh [OPTIONS] -Seed the lean-workbench data volume with elan, mathlib packages, and templates. +Seed the lean-workbench data volume with elan and a blank template. Options: - --data-dir DIR Data directory for lean-workbench state - (default: /data) - --lean-version REV Lean version to preinstall (must have a corresponding mathlib tag) - (default: latest v4.* tag on mathlib4) - --help Show this help message + --data-dir DIR Data directory for lean-workbench state + (default: /data) + --install-toolchain Install the latest stable lake toolchain + (default: latest v4.* tag on mathlib4) + --help Show this help message EOF exit 0 } ROOT="/data" -LEAN_VERSION="" +INSTALL_TOOLCHAIN=0 while [[ $# -gt 0 ]]; do case "$1" in --data-dir) ROOT="$2"; shift 2 ;; - --lean-version) LEAN_VERSION="$2"; shift 2 ;; + --install-toolchain) INSTALL_TOOLCHAIN=1; shift 1 ;; --help) usage ;; *) echo "Unknown option: $1"; echo "Try --help"; exit 1 ;; esac @@ -49,140 +49,44 @@ done echo "[seed-volume] Data directory: $ROOT" echo "" -TOTAL=7 +STEP=0 +TOTAL=3 +if (( INSTALL_TOOLCHAIN )); then + TOTAL=4 +fi -# --- Step 1: Create directory structure --- -echo "[[ progress 1/$TOTAL Creating directories ]]" +# ------ +STEP=$(( STEP + 1 )) +echo "[[ progress $STEP/$TOTAL Creating directory structure ]]" mkdir -p "$ROOT"/{workspaces,db,package-sets,templates} -# --- Step 2: Resolve mathlib version --- -echo "[[ progress 2/$TOTAL Resolving mathlib version ]]" -if [ -z "$LEAN_VERSION" ]; then - # Mathlib tags lag behind Lean releases, so let the latest mathlib tag - # drive the Lean toolchain version rather than the other way around. - MATHLIB_REV=$(curl -sSf \ - "https://github.com/leanprover-community/mathlib4/info/refs?service=git-upload-pack" \ - | sed -n 's|.*refs/tags/\(v4\.[^^[:space:]]*\).*|\1|p' \ - | sort -u -V | tail -1) - LEAN_VERSION="$MATHLIB_REV" -else - MATHLIB_REV="$LEAN_VERSION" -fi -TOOLCHAIN="leanprover/lean4:$LEAN_VERSION" -echo "[seed-volume] Installing mathlib tag: $MATHLIB_REV (Lean $LEAN_VERSION)" - -# --- Step 3: Install elan --- -echo "[[ progress 3/$TOTAL Installing elan ]]" +# ------ +STEP=$(( STEP + 1 )) +echo "[[ progress $STEP/$TOTAL Installing elan ]]" ELAN_HOME="$ROOT/elan" if [ ! -x "$ELAN_HOME/bin/elan" ]; then echo "[seed-volume] Downloading elan + Lean toolchain..." mkdir -p "$ELAN_HOME" curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \ - | ELAN_HOME="$ELAN_HOME" sh -s -- -y --default-toolchain "$TOOLCHAIN" --no-modify-path + | ELAN_HOME="$ELAN_HOME" sh -s -- -y --no-modify-path else echo "[seed-volume] elan already installed." fi -export ELAN_HOME -export PATH="$ELAN_HOME/bin:$PATH" -if ! elan toolchain list | grep -Fq -- "$LEAN_VERSION"; then - elan toolchain install "$TOOLCHAIN" +# ------ +if (( INSTALL_TOOLCHAIN )); then + STEP=$(( STEP + 1 )) + echo "[[ progress $STEP/$TOTAL Installing latest toolchain ]]" + ELAN_HOME="$ELAN_HOME" "$ELAN_HOME/bin/elan" install stable fi -echo "[seed-volume] Using Lean $LEAN_VERSION" - -# --- Step 4: Fetch mathlib source --- -echo "[[ progress 4/$TOTAL Fetching mathlib source ]]" -WORK_DIR=$(mktemp -d) -trap 'rm -rf "$WORK_DIR"' EXIT - -echo "$TOOLCHAIN" > "$WORK_DIR/lean-toolchain" -cat > "$WORK_DIR/lakefile.toml" < "$BLANK_TEMPLATE_DIR/metadata.json" < "$WORK_DIR/Main.lean" <<'EOF' -import Mathlib - -#check Nat.add_comm -EOF - -cd "$WORK_DIR" -mkdir -p .lake/packages -git clone --depth 1 --branch "$MATHLIB_REV" --progress https://github.com/leanprover-community/mathlib4 .lake/packages/mathlib -lake --no-ansi update - -# --- Step 5: Download pre-compiled oleans --- -echo "[[ progress 5/$TOTAL Downloading pre-compiled oleans ]]" -lake --no-ansi exe cache get - -# --- Step 6: Install package set --- -echo "[[ progress 6/$TOTAL Installing package set ]]" -PACKAGE_SET_DIR="$ROOT/package-sets/mathlib-$LEAN_VERSION" -# The dir basename is also the template ID, so must satisfy TEMPLATE_ID_RE (no dots). -TEMPLATE_DIR="$ROOT/templates/mathlib-${LEAN_VERSION//./-}" - -rm -rf "$PACKAGE_SET_DIR" -mkdir -p "$PACKAGE_SET_DIR" -for pkg_dir in "$WORK_DIR/.lake/packages"/*/; do - pkg_name=$(basename "$pkg_dir") - echo "[seed-volume] copying package: $pkg_name" - # Store each package at the .lake/packages/ path it occupies in a project; - # see buildProjectMount. - pkg_dest="$PACKAGE_SET_DIR/$pkg_name/.lake/packages/$pkg_name" - mkdir -p "$(dirname "$pkg_dest")" - cp -a "$pkg_dir" "$pkg_dest" -done - -ls -d "$PACKAGE_SET_DIR"/*/ | xargs -n1 basename > "$PACKAGE_SET_DIR/packages.txt" - -# Install mathlib template -rm -rf "$TEMPLATE_DIR" -mkdir -p "$TEMPLATE_DIR" -cp "$WORK_DIR/lean-toolchain" "$TEMPLATE_DIR/" -cp "$WORK_DIR/lakefile.toml" "$TEMPLATE_DIR/" -cp "$WORK_DIR/lake-manifest.json" "$TEMPLATE_DIR/" -cp "$WORK_DIR/Main.lean" "$TEMPLATE_DIR/" -cat > "$TEMPLATE_DIR/metadata.json" < "$HELLO_DIR/lean-toolchain" - cp "$HELLO_SRC/lakefile.toml" "$HELLO_DIR/" - cp "$HELLO_SRC/Main.lean" "$HELLO_DIR/" - cat > "$HELLO_DIR/metadata.json" <('blank') const templates = use(props.templates) + const [chosenTemplate, setChosenTemplate] = useState(templates[0]?.id) + if (!chosenTemplate) { + return <>No project templates are available + } + return ( <> diff --git a/src/app/[userName]/actions.ts b/src/app/[userName]/actions.ts index 1f6cfcd1..186e5c7d 100644 --- a/src/app/[userName]/actions.ts +++ b/src/app/[userName]/actions.ts @@ -26,7 +26,7 @@ export interface ProjectInfo { const zCreateProject = z.object({ name: zValidateProjectName, - template: zTemplateId.default('blank'), + template: zTemplateId, }) export const createProject = submitAction( @@ -38,13 +38,11 @@ export const createProject = submitAction( const user = session.user // Validate template exists - if (template !== 'blank') { - const meta = await readTemplateMetadata(template) - if (meta.packageSet) { - const packagesFile = path.join(getPackageSetsDir(), meta.packageSet, 'packages.txt') - if (!(await existsAsync(packagesFile))) { - throw new Error(`Package set "${meta.packageSet}" not found. Run seed-volume.sh first.`) - } + const { packageSet } = await readTemplateMetadata(template) + if (packageSet) { + const packagesFile = path.join(getPackageSetsDir(), packageSet, 'packages.txt') + if (!(await existsAsync(packagesFile))) { + throw new Error(`Package set "${packageSet}" not found. Run seed-volume.sh first.`) } } @@ -59,16 +57,10 @@ export const createProject = submitAction( const workspace = getProjectDir(user, projectId) await fs.mkdir(workspace, { recursive: true }) - let packageSet: string | undefined - if (template !== 'blank') { - const templateDir = path.join(getTemplatesDir(), template) - // Copy template directory except for metadata.json - await fs.cp(templateDir, workspace, { recursive: true }) - await fs.rm(path.join(workspace, 'metadata.json'), { force: true }) - - const meta = await readTemplateMetadata(template) - packageSet = meta.packageSet - } + const templateDir = path.join(getTemplatesDir(), template) + // Copy template directory except for metadata.json + await fs.cp(templateDir, workspace, { recursive: true }) + await fs.rm(path.join(workspace, 'metadata.json'), { force: true }) // Store project in DB const project = await db.project.create({ diff --git a/src/app/admin/actions.ts b/src/app/admin/actions.ts index dc1469df..080c8878 100644 --- a/src/app/admin/actions.ts +++ b/src/app/admin/actions.ts @@ -99,7 +99,6 @@ const zUpdateOAuth = z.object({ clientSecret: zGithubAuthConfig.shape.clientSecret.optional(), }) -// FIXME: dedup with saveSetupConfig action somehow? export const updateOAuthConfig = submitAction(zUpdateOAuth, async ({ clientId, clientSecret }) => { await requireAdmin() const config = getConfig() @@ -270,7 +269,6 @@ export const editTemplateMetadata = submitAction( await requireAdmin() try { - if (id === 'blank') throw new Error('cannot modify blank template') const config = await readTemplateMetadata(id) if (name) config.name = name if (!description) { diff --git a/src/app/admin/components/TemplateManagement.tsx b/src/app/admin/components/TemplateManagement.tsx index 23f9aa23..a2701dfc 100644 --- a/src/app/admin/components/TemplateManagement.tsx +++ b/src/app/admin/components/TemplateManagement.tsx @@ -103,17 +103,15 @@ function TemplateRow(props: TemplateInfo) { - {id !== 'blank' && ( - - )} + {/* Error message */}
{editError}
diff --git a/src/app/setup/SetupFlow.tsx b/src/app/setup/SetupFlow.tsx index fc005c99..23aeecbc 100644 --- a/src/app/setup/SetupFlow.tsx +++ b/src/app/setup/SetupFlow.tsx @@ -1,117 +1,43 @@ 'use client' -import { LEAN_VERSION_RE } from '@leanprover/workbench-shared' import { redirect, useRouter } from 'next/navigation' import { useState } from 'react' -import z from 'zod' import TrackedCommandForm from '@/app/components/TrackedCommandForm' -import { useServerAction, useThrowingSWR } from '@/lib/client/util' import { useConfigCtx } from '@/lib/contexts' -import { type SetupStatus } from '@/lib/server/seed' -import { doSeed, saveSetupConfig } from './actions' - -/** Fetch mathlib4 v4.* tags, newest-first, paginating until exhausted. */ -async function fetchLeanVersions(): Promise { - const versions: string[] = [] - // This relies on version tags being returned first. - const res: Response = await fetch('https://api.github.com/repos/leanprover-community/mathlib4/tags?per_page=100') - if (!res.ok) throw new Error(`GitHub API ${res.status}`) - const data = z.array(z.object({ name: z.string() })).parse(await res.json()) - for (const item of data) if (LEAN_VERSION_RE.test(item.name)) versions.push(item.name) - return versions -} +import { doSeed } from './actions' interface SetupFlowProps { baseUrl: string - statusOnMount: SetupStatus } -export default function SetupFlow({ baseUrl, statusOnMount }: SetupFlowProps) { +export default function SetupFlow({ baseUrl }: SetupFlowProps) { const router = useRouter() const cfg = useConfigCtx() const [wasCompleteOnMount] = useState(cfg.isSetupComplete) - // Redirect to index on new visits, but keep the page open during actual setup if (wasCompleteOnMount) redirect('/') - const [setupStatus, setSetupStatus] = useState(statusOnMount) - const { data: leanVersions } = useThrowingSWR('leanVersions', fetchLeanVersions) - - const [configError, saveConfigAction, savingConfig] = useServerAction(saveSetupConfig, () => - setSetupStatus('configured'), - ) - return ( - <> -

Setup

-

Configuration

- {setupStatus === 'not-configured' ? ( -
-

GitHub Authentication

-

- Create a{' '} - - GitHub OAuth App - - . When prompted, set the "Redirect URI" to -

- {`${baseUrl}/api/auth/callback/github`} -

- Then enter the client ID and secret of your OAuth App here. -

-
- - -
-
- - -
- -
- ) : ( -
Configuration saved.
- )} - - {configError &&
{configError}
} - -
- -

Initialize Data Volume

-

- Install elan, download pre-compiled Mathlib, and set up project templates. This may take several minutes. -

- - { - router.refresh() - router.push('/') - }, - }} - > - - - + { + router.refresh() + router.push('/admin') + }, + }} + > + + + ) } diff --git a/src/app/setup/actions.ts b/src/app/setup/actions.ts index cfb0af39..230e9d29 100644 --- a/src/app/setup/actions.ts +++ b/src/app/setup/actions.ts @@ -1,28 +1,46 @@ 'use server' +import { getDataDir } from '@leanprover/workbench-shared/node' +import path from 'path' import z from 'zod' -import { initAuth, requireAdmin } from '@/lib/server/auth' -import { getConfig, saveConfig, zGithubAuthConfig } from '@/lib/server/config' -import { startSeed } from '@/lib/server/seed' +import { requireAdmin } from '@/lib/server/auth' +import { getConfig, isDevMode, saveConfig } from '@/lib/server/config' +import { startTrackedCommand } from '@/lib/server/trackedCommand' import { submitAction } from '@/lib/server/util' - -export const saveSetupConfig = submitAction(zGithubAuthConfig, async githubAuth => { - await requireAdmin() - - const cfg = getConfig() - if (cfg.isSetupComplete) return { error: 'Setup already completed' } - - cfg.githubAuth = githubAuth - await saveConfig() - - // Reinitialize auth with new configuration - await initAuth() - - return { ok: true } -}) - -export const doSeed = submitAction(z.object({ leanVersion: z.string().optional() }), async ({ leanVersion }) => { - await requireAdmin() - return startSeed(leanVersion) -}) +import { type ActionResponse } from '@/lib/util' + +export const doSeed = submitAction( + z.object({ baseUrl: z.string(), installToolchain: z.boolean().optional() }), + async ({ baseUrl, installToolchain }): Promise> => { + await requireAdmin() + + const cfg = getConfig() + if (cfg.isSetupComplete) return { error: 'Already seeded' } + if (cfg.baseUrl !== baseUrl) { + if (isDevMode()) { + cfg.baseUrl = baseUrl + await saveConfig() + } else { + return { error: `Server is configured to run on ${cfg.baseUrl}, but is being accessed via ${baseUrl}` } + } + } + + const scriptsDir = path.join(process.cwd(), 'scripts') // scripts/ is a sibling directory + const scriptsArgs = ['--data-dir', getDataDir()] + if (installToolchain) scriptsArgs.push('--install-toolchain') + const emitter = startTrackedCommand('seed', path.join(scriptsDir, 'seed-volume.sh'), scriptsArgs) + + emitter?.on('exit', async exit => { + // Note: success has already been reported to the client component; + // if the saveConfig() fails, the config state will be out of sync + // (We're basically pretending saveConfig() will never fail here.) + if (exit.type === 'success') { + getConfig().isSetupComplete = true + await saveConfig() + } + }) + + return { ok: !!emitter } + }, +) diff --git a/src/app/setup/page.tsx b/src/app/setup/page.tsx index cd3f6ff2..e95dae82 100644 --- a/src/app/setup/page.tsx +++ b/src/app/setup/page.tsx @@ -2,7 +2,6 @@ import { headers } from 'next/headers' import { requireAdmin } from '@/lib/server/auth' import { getConfig, isDevMode } from '@/lib/server/config' -import { fetchSetupStatus } from '@/lib/server/seed' import SetupFlow from './SetupFlow' @@ -11,6 +10,13 @@ export const instant = false export default async function Setup() { await requireAdmin() // redirects to ./unauthorized.tsx for login const baseUrl = isDevMode() ? `http://${(await headers()).get('host')}` : getConfig().baseUrl - const statusOnMount = await fetchSetupStatus() - return + return ( + <> +

Setup Data Volume

+

+ Install elan and set up an initial project template. This may take several minutes. +

+ + + ) } diff --git a/src/lib/server/projectTemplate.ts b/src/lib/server/projectTemplate.ts index 83e77678..7b968bed 100644 --- a/src/lib/server/projectTemplate.ts +++ b/src/lib/server/projectTemplate.ts @@ -43,7 +43,7 @@ export interface TemplateInfo { export async function listTemplates(): Promise { const templatesDir = getTemplatesDir() - const result: TemplateInfo[] = [{ id: 'blank', name: 'Blank', description: 'Empty workspace' }] + const result: TemplateInfo[] = [] const entries = await fs.readdir(templatesDir, { withFileTypes: true }) for (const entry of entries) { diff --git a/src/lib/server/seed.ts b/src/lib/server/seed.ts deleted file mode 100644 index ce3621fe..00000000 --- a/src/lib/server/seed.ts +++ /dev/null @@ -1,46 +0,0 @@ -import 'server-only' - -import path from 'node:path' - -import { LEAN_VERSION_RE } from '@leanprover/workbench-shared' -import { getDataDir } from '@leanprover/workbench-shared/node' - -import { type ActionResponse } from '@/lib/util' - -import { getConfig, hasGithubAuth, saveConfig } from './config' -import { getTrackedCommandState, startTrackedCommand } from './trackedCommand' - -export function startSeed(leanVersion: string | undefined): ActionResponse { - const cfg = getConfig() - if (cfg.isSetupComplete) return { error: 'Already seeded' } - if (!cfg.githubAuth) return { error: 'Configure GitHub authentication first' } - if (leanVersion && !LEAN_VERSION_RE.test(leanVersion)) return { error: `Invalid Lean version ${leanVersion}` } - - const scriptsDir = path.join(process.cwd(), 'scripts') // scripts/ is a sibling directory - const scriptsArgs = [path.join(scriptsDir, 'seed-volume.sh'), '--data-dir', getDataDir()] - if (leanVersion) scriptsArgs.push('--lean-version', leanVersion) - const emitter = startTrackedCommand('seed', 'bash', scriptsArgs) - - emitter?.on('exit', async exit => { - // Note: success has already been reported to the client component; - // if the saveConfig() fails, the config state will be out of sync - // (We're basically pretending saveConfig() will never fail here.) - if (exit.type === 'success') { - getConfig().isSetupComplete = true - await saveConfig() - } - }) - - return { ok: !!emitter } -} - -export type SetupStatus = 'not-configured' | 'configured' | 'show-tty' | 'seeded' - -export async function fetchSetupStatus(): Promise { - const cfg = getConfig() - if (cfg.isSetupComplete) return 'seeded' - if (!hasGithubAuth(cfg)) return 'not-configured' - const st = getTrackedCommandState('seed') - if (!st) return 'configured' - return 'show-tty' -} diff --git a/src/prisma/schema.prisma b/src/prisma/schema.prisma index 22ffcf4e..ff167624 100644 --- a/src/prisma/schema.prisma +++ b/src/prisma/schema.prisma @@ -115,7 +115,7 @@ model Project { createdAt DateTime @default(now()) updatedAt DateTime @default(now()) @updatedAt /// Which template the project was created from. - template String @default("blank") + template String isPublic Boolean @default(false) packageSets ProjectPackageSet[] diff --git a/templates/hello/Main.lean b/templates/hello/Main.lean deleted file mode 100644 index ec2c947e..00000000 --- a/templates/hello/Main.lean +++ /dev/null @@ -1,2 +0,0 @@ -def main : IO Unit := - IO.println "Hello, world!" diff --git a/templates/hello/lakefile.toml b/templates/hello/lakefile.toml deleted file mode 100644 index 4884add0..00000000 --- a/templates/hello/lakefile.toml +++ /dev/null @@ -1,2 +0,0 @@ -name = "hello" -version = "0.1.0" From 873674647f2858b0afc59022cbf9e7ff786e53ba Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Thu, 3 Sep 2026 11:40:20 -0400 Subject: [PATCH 02/10] generate db migration --- .../migration.sql | 19 +++++++++++++++++++ src/prisma/migrations/migration_lock.toml | 3 +++ 2 files changed, 22 insertions(+) create mode 100644 src/prisma/migrations/20260903153928_no_blank_templates/migration.sql create mode 100644 src/prisma/migrations/migration_lock.toml diff --git a/src/prisma/migrations/20260903153928_no_blank_templates/migration.sql b/src/prisma/migrations/20260903153928_no_blank_templates/migration.sql new file mode 100644 index 00000000..da885bbc --- /dev/null +++ b/src/prisma/migrations/20260903153928_no_blank_templates/migration.sql @@ -0,0 +1,19 @@ +-- RedefineTables +PRAGMA defer_foreign_keys=ON; +PRAGMA foreign_keys=OFF; +CREATE TABLE "new_project" ( + "id" TEXT NOT NULL PRIMARY KEY, + "userId" TEXT NOT NULL, + "name" TEXT NOT NULL, + "createdAt" DATETIME NOT NULL DEFAULT CURRENT_TIMESTAMP, + "updatedAt" DATETIME NOT NULL DEFAULT CURRENT_TIMESTAMP, + "template" TEXT NOT NULL, + "isPublic" BOOLEAN NOT NULL DEFAULT false, + CONSTRAINT "project_userId_fkey" FOREIGN KEY ("userId") REFERENCES "user" ("id") ON DELETE CASCADE ON UPDATE CASCADE +); +INSERT INTO "new_project" ("createdAt", "id", "isPublic", "name", "template", "updatedAt", "userId") SELECT "createdAt", "id", "isPublic", "name", "template", "updatedAt", "userId" FROM "project"; +DROP TABLE "project"; +ALTER TABLE "new_project" RENAME TO "project"; +CREATE UNIQUE INDEX "project_userId_name_key" ON "project"("userId", "name"); +PRAGMA foreign_keys=ON; +PRAGMA defer_foreign_keys=OFF; diff --git a/src/prisma/migrations/migration_lock.toml b/src/prisma/migrations/migration_lock.toml new file mode 100644 index 00000000..2a5a4441 --- /dev/null +++ b/src/prisma/migrations/migration_lock.toml @@ -0,0 +1,3 @@ +# Please do not edit this file manually +# It should be added in your version-control system (e.g., Git) +provider = "sqlite" From 7ab544bb26db5b7f8b2feb1e4fff2b4a7bed185b Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Fri, 4 Sep 2026 18:35:13 -0400 Subject: [PATCH 03/10] review fixes --- scripts/seed-volume.sh | 38 +++---------------------------------- src/app/setup/SetupFlow.tsx | 9 +++++++-- src/app/setup/page.tsx | 6 +----- 3 files changed, 11 insertions(+), 42 deletions(-) diff --git a/scripts/seed-volume.sh b/scripts/seed-volume.sh index 86297361..c0b8d9e3 100755 --- a/scripts/seed-volume.sh +++ b/scripts/seed-volume.sh @@ -1,47 +1,15 @@ #!/bin/bash -# # Seed the lean-workbench data volume with everything needed to run. -# -# This is the one-stop setup script. Run it before `make build` / `make serve`. -# It is idempotent — safe to re-run. -# -# What it does: -# 1. Creates the directory structure under $ROOT -# 2. Populates package-sets/ and templates/ -# 3. Seeds the "hello" template into templates/ -# -# Progress markers: -# Lines matching [[ progress STEP/TOTAL LABEL ]] are parsed by the setup UI -# to drive a progress bar. -# -set -euo pipefail - -SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)" - -usage() { - cat <<'EOF' -Usage: seed-volume.sh [OPTIONS] -Seed the lean-workbench data volume with elan and a blank template. - -Options: - --data-dir DIR Data directory for lean-workbench state - (default: /data) - --install-toolchain Install the latest stable lake toolchain - (default: latest v4.* tag on mathlib4) - --help Show this help message -EOF - exit 0 -} +set -euo pipefail ROOT="/data" +SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)" INSTALL_TOOLCHAIN=0 while [[ $# -gt 0 ]]; do case "$1" in - --data-dir) ROOT="$2"; shift 2 ;; --install-toolchain) INSTALL_TOOLCHAIN=1; shift 1 ;; - --help) usage ;; *) echo "Unknown option: $1"; echo "Try --help"; exit 1 ;; esac done @@ -68,7 +36,7 @@ if [ ! -x "$ELAN_HOME/bin/elan" ]; then echo "[seed-volume] Downloading elan + Lean toolchain..." mkdir -p "$ELAN_HOME" curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \ - | ELAN_HOME="$ELAN_HOME" sh -s -- -y --no-modify-path + | ELAN_HOME="$ELAN_HOME" sh -s -- -y --no-modify-path --default-toolchain none else echo "[seed-volume] elan already installed." fi diff --git a/src/app/setup/SetupFlow.tsx b/src/app/setup/SetupFlow.tsx index 23aeecbc..661a336d 100644 --- a/src/app/setup/SetupFlow.tsx +++ b/src/app/setup/SetupFlow.tsx @@ -1,7 +1,7 @@ 'use client' import { redirect, useRouter } from 'next/navigation' -import { useState } from 'react' +import { useState, useSyncExternalStore } from 'react' import TrackedCommandForm from '@/app/components/TrackedCommandForm' import { useConfigCtx } from '@/lib/contexts' @@ -16,6 +16,11 @@ export default function SetupFlow({ baseUrl }: SetupFlowProps) { const router = useRouter() const cfg = useConfigCtx() const [wasCompleteOnMount] = useState(cfg.isSetupComplete) + const observedBase = useSyncExternalStore( + () => () => {}, + () => window.location.origin, + () => baseUrl, + ) if (wasCompleteOnMount) redirect('/') return ( @@ -37,7 +42,7 @@ export default function SetupFlow({ baseUrl }: SetupFlowProps) { {' '} Install latest stable toolchain? - + ) } diff --git a/src/app/setup/page.tsx b/src/app/setup/page.tsx index e95dae82..d5ae2b6a 100644 --- a/src/app/setup/page.tsx +++ b/src/app/setup/page.tsx @@ -1,7 +1,4 @@ -import { headers } from 'next/headers' - import { requireAdmin } from '@/lib/server/auth' -import { getConfig, isDevMode } from '@/lib/server/config' import SetupFlow from './SetupFlow' @@ -9,14 +6,13 @@ export const instant = false export default async function Setup() { await requireAdmin() // redirects to ./unauthorized.tsx for login - const baseUrl = isDevMode() ? `http://${(await headers()).get('host')}` : getConfig().baseUrl return ( <>

Setup Data Volume

Install elan and set up an initial project template. This may take several minutes.

- + ) } From 9a54d1bb254959db12f3b57aa2581b8ac23c700b Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Fri, 4 Sep 2026 22:12:33 -0400 Subject: [PATCH 04/10] pass back baseUrl --- src/app/setup/page.tsx | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/app/setup/page.tsx b/src/app/setup/page.tsx index d5ae2b6a..57c89e81 100644 --- a/src/app/setup/page.tsx +++ b/src/app/setup/page.tsx @@ -1,4 +1,5 @@ import { requireAdmin } from '@/lib/server/auth' +import { getConfig } from '@/lib/server/config' import SetupFlow from './SetupFlow' @@ -12,7 +13,7 @@ export default async function Setup() {

Install elan and set up an initial project template. This may take several minutes.

- + ) } From ad87f8ee4850a4bddd9400ed4cfd0297fffd85bb Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Sat, 5 Sep 2026 12:20:06 -0400 Subject: [PATCH 05/10] don't pass deactivated --data-dir argument to seed-volume --- src/app/setup/actions.ts | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/app/setup/actions.ts b/src/app/setup/actions.ts index 230e9d29..43d1aef2 100644 --- a/src/app/setup/actions.ts +++ b/src/app/setup/actions.ts @@ -27,7 +27,7 @@ export const doSeed = submitAction( } const scriptsDir = path.join(process.cwd(), 'scripts') // scripts/ is a sibling directory - const scriptsArgs = ['--data-dir', getDataDir()] + const scriptsArgs = [] if (installToolchain) scriptsArgs.push('--install-toolchain') const emitter = startTrackedCommand('seed', path.join(scriptsDir, 'seed-volume.sh'), scriptsArgs) From 4b493e50424ee51d949662f8cd9a4bdb99c97a21 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Sat, 5 Sep 2026 12:21:30 -0400 Subject: [PATCH 06/10] remove inactive SCRIPT_DIR --- scripts/seed-volume.sh | 1 - 1 file changed, 1 deletion(-) diff --git a/scripts/seed-volume.sh b/scripts/seed-volume.sh index c0b8d9e3..3d9177f8 100755 --- a/scripts/seed-volume.sh +++ b/scripts/seed-volume.sh @@ -4,7 +4,6 @@ set -euo pipefail ROOT="/data" -SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)" INSTALL_TOOLCHAIN=0 while [[ $# -gt 0 ]]; do From 86bf718f98f1174640f541241a8c0cd5d382ef09 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Sat, 5 Sep 2026 12:34:15 -0400 Subject: [PATCH 07/10] lint --- src/app/setup/actions.ts | 1 - 1 file changed, 1 deletion(-) diff --git a/src/app/setup/actions.ts b/src/app/setup/actions.ts index 43d1aef2..ce9e7796 100644 --- a/src/app/setup/actions.ts +++ b/src/app/setup/actions.ts @@ -1,6 +1,5 @@ 'use server' -import { getDataDir } from '@leanprover/workbench-shared/node' import path from 'path' import z from 'zod' From a890e05902ab37495c062d79199d237563759252 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Sat, 5 Sep 2026 14:14:25 -0400 Subject: [PATCH 08/10] retain COLLATE NOCASE --- .../migrations/20260903153928_no_blank_templates/migration.sql | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/prisma/migrations/20260903153928_no_blank_templates/migration.sql b/src/prisma/migrations/20260903153928_no_blank_templates/migration.sql index da885bbc..6c3bbef7 100644 --- a/src/prisma/migrations/20260903153928_no_blank_templates/migration.sql +++ b/src/prisma/migrations/20260903153928_no_blank_templates/migration.sql @@ -4,7 +4,7 @@ PRAGMA foreign_keys=OFF; CREATE TABLE "new_project" ( "id" TEXT NOT NULL PRIMARY KEY, "userId" TEXT NOT NULL, - "name" TEXT NOT NULL, + "name" TEXT NOT NULL COLLATE NOCASE, "createdAt" DATETIME NOT NULL DEFAULT CURRENT_TIMESTAMP, "updatedAt" DATETIME NOT NULL DEFAULT CURRENT_TIMESTAMP, "template" TEXT NOT NULL, From cc8d45bd9570887842253b8cf024d67d47d2ec0c Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Sat, 5 Sep 2026 14:18:03 -0400 Subject: [PATCH 09/10] match create-*.sh's LEAN_WORKBENCH_DATA_DIR pattern --- scripts/seed-volume.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/seed-volume.sh b/scripts/seed-volume.sh index 3d9177f8..6cc47f53 100755 --- a/scripts/seed-volume.sh +++ b/scripts/seed-volume.sh @@ -3,7 +3,7 @@ set -euo pipefail -ROOT="/data" +ROOT=${LEAN_WORKBENCH_DATA_DIR:?No data directory was specified} INSTALL_TOOLCHAIN=0 while [[ $# -gt 0 ]]; do From e9e6ecc06ea401bd8d501874bfc0c5310df2f450 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Sun, 6 Sep 2026 08:50:41 -0400 Subject: [PATCH 10/10] usage for seed-volume --- scripts/seed-volume.sh | 3 +++ 1 file changed, 3 insertions(+) diff --git a/scripts/seed-volume.sh b/scripts/seed-volume.sh index 6cc47f53..29f1820b 100755 --- a/scripts/seed-volume.sh +++ b/scripts/seed-volume.sh @@ -1,5 +1,8 @@ #!/bin/bash # Seed the lean-workbench data volume with everything needed to run. +# Should be idempotent and safe to rerun. +# +# usage: seed-volume.sh [--install-toolchain] set -euo pipefail