feat(admin): simplify initialization flow

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" <<EOF
-name = "mathlib-project"
-version = "0.1.0"
 
-[[require]]
-name = "mathlib"
-git = "https://github.com/leanprover-community/mathlib4"
-rev = "$MATHLIB_REV"
+# -----
+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" <<EOF
+{ "name": "Blank", "description": "Empty workspace" }
 EOF
-cat > "$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/<pkg> 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" <<EOF
-{ "name": "Lean $LEAN_VERSION + Mathlib", "description": "Pre-built Mathlib dependency", "packageSet": "mathlib-$LEAN_VERSION" }
-EOF
-
-# --- Step 7: Seed hello template ---
-echo "[[ progress 7/$TOTAL Installing templates ]]"
-HELLO_DIR="$ROOT/templates/hello"
-if [ -d "$HELLO_DIR" ]; then
-  echo "[seed-volume] hello template already exists, skipping."
-else
-  # scripts/ and templates/ are sibling directories.
-  HELLO_SRC="$SCRIPT_DIR/../templates/hello"
-  if [ ! -d "$HELLO_SRC" ]; then
-    echo "[seed-volume] WARNING: hello template source not found, skipping."
-  else
-    mkdir -p "$HELLO_DIR"
-    echo "$TOOLCHAIN" > "$HELLO_DIR/lean-toolchain"
-    cp "$HELLO_SRC/lakefile.toml" "$HELLO_DIR/"
-    cp "$HELLO_SRC/Main.lean" "$HELLO_DIR/"
-    cat > "$HELLO_DIR/metadata.json" <<EOF
-{ "name": "Lean $LEAN_VERSION", "description": "Minimal Lean project" }
-EOF
-    echo "[seed-volume] hello template installed."
-  fi
-fi
-
-# --- Summary ---
-OLEAN_COUNT=$(find "$PACKAGE_SET_DIR" -name "*.olean" | wc -l)
-TOTAL_SIZE=$(du -sh "$PACKAGE_SET_DIR" | cut -f1)
-PKG_COUNT=$(wc -l < "$PACKAGE_SET_DIR/packages.txt")
-
-echo ""
-echo "[seed-volume] Done."
-echo "  Package set: $PACKAGE_SET_DIR"
-echo "  Template:    $TEMPLATE_DIR"
-echo "  Packages:    $PKG_COUNT"
-echo "  .olean files: $OLEAN_COUNT"
-echo "  Total size:  $TOTAL_SIZE"
+echo "Finished seeding Workbench"

src/app/[userName]/NewProjectForm.tsx

@@ -64,8 +64,12 @@ export function NewProjectForm(props: NewProjectProps) {
 }
 
 function NewProjectSelection(props: NewProjectProps & { createPending: boolean }) {
-  const [chosenTemplate, setChosenTemplate] = useState<string>('blank')
   const templates = use(props.templates)
+  const [chosenTemplate, setChosenTemplate] = useState<string | undefined>(templates[0]?.id)
+  if (!chosenTemplate) {
+    return <>No project templates are available</>
+  }
+
   return (
     <>
       <input type='hidden' name='template' value={chosenTemplate} />

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 = path.join(getWorkspacesDir(), user.name, 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({

src/app/admin/actions.ts

@@ -100,7 +100,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()
@@ -271,7 +270,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) {

src/app/admin/components/TemplateManagement.tsx

@@ -105,17 +105,15 @@ function TemplateRow(props: TemplateInfo) {
           <button hidden={!showForm} type='submit' disabled={editPending}>
             {editPending ? 'Saving...' : 'Save'}
           </button>
-          {id !== 'blank' && (
-            <button
-              onClick={e => {
-                e.preventDefault()
-                setShowForm(v => !v)
-              }}
-              disabled={editPending}
-            >
-              {showForm ? 'Cancel' : 'Edit'}
-            </button>
-          )}
+          <button
+            onClick={e => {
+              e.preventDefault()
+              setShowForm(v => !v)
+            }}
+            disabled={editPending}
+          >
+            {showForm ? 'Cancel' : 'Edit'}
+          </button>
         </div>
         {/* Error message */}
         <div style={{ gridArea: 'error', color: '#f00' }}>{editError}</div>