diff --git a/scripts/seed-volume.sh b/scripts/seed-volume.sh index 5e1de806..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, mathlib packages, and templates. - -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 -EOF - exit 0 -} +set -euo pipefail ROOT="/data" -LEAN_VERSION="" +SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)" +INSTALL_TOOLCHAIN=0 while [[ $# -gt 0 ]]; do case "$1" in - --data-dir) ROOT="$2"; shift 2 ;; - --lean-version) LEAN_VERSION="$2"; shift 2 ;; - --help) usage ;; + --install-toolchain) INSTALL_TOOLCHAIN=1; shift 1 ;; *) echo "Unknown option: $1"; echo "Try --help"; exit 1 ;; esac done @@ -49,140 +17,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 --default-toolchain none 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" < "$WORK_DIR/Main.lean" <<'EOF' -import Mathlib -#check Nat.add_comm +# ----- +STEP=$(( STEP + 1 )) +echo "[[ progress $STEP/$TOTAL Creating a blank template ]]" +BLANK_TEMPLATE_DIR="$ROOT/templates/blank" +mkdir -p "$BLANK_TEMPLATE_DIR" +cat > "$BLANK_TEMPLATE_DIR/metadata.json" < 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 d8efefc1..975ded90 100644 --- a/src/app/admin/actions.ts +++ b/src/app/admin/actions.ts @@ -102,7 +102,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() @@ -273,7 +272,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 c6e25877..4de61a10 100644 --- a/src/app/admin/components/TemplateManagement.tsx +++ b/src/app/admin/components/TemplateManagement.tsx @@ -105,17 +105,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..661a336d 100644 --- a/src/app/setup/SetupFlow.tsx +++ b/src/app/setup/SetupFlow.tsx @@ -1,117 +1,48 @@ '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 { useState, useSyncExternalStore } from 'react' 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'), + const observedBase = useSyncExternalStore( + () => () => {}, + () => window.location.origin, + () => baseUrl, ) + if (wasCompleteOnMount) redirect('/') 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..57c89e81 100644 --- a/src/app/setup/page.tsx +++ b/src/app/setup/page.tsx @@ -1,8 +1,5 @@ -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 { getConfig } from '@/lib/server/config' import SetupFlow from './SetupFlow' @@ -10,7 +7,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/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/lib/server/util.ts b/src/lib/server/util.ts index c8cdc5d0..115f9707 100644 --- a/src/lib/server/util.ts +++ b/src/lib/server/util.ts @@ -132,7 +132,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/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" 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"