feat: template creation in the admin menu

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 <<EOF
+name = "$TEMPLATE_ID"
+version = "0.1.0"
+defaultTargets = ["Main"]
+
+[[lean_lib]]
+name = "Main"
+EOF
+
+echo "[[ progress 2/4 Building project ]]"
+lake --no-ansi --keep-toolchain build
+
+echo "[[ progress 3/4 Constructing template ]]"
+TEMPLATE_DIR="$WORK_DIR/template"
+mkdir "$TEMPLATE_DIR"
+
+mv "$BUILD_DIR/metadata.json" "$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/"
+
+echo "[[ progress 4/4 Placing template ]]"
+TEMPLATE_PLACED="$ROOT/templates/$TEMPLATE_ID"
+mv "$TEMPLATE_DIR" "$TEMPLATE_PLACED"
+
+echo "Template $TEMPLATE_ID created successfully!"

scripts/create-tagged-lib.sh

@@ -0,0 +1,111 @@
+#!/bin/bash
+# Create a Mathlib or closely-related-to-Mathlib (e.g. CSLib) project
+# usage: create-tagged-lib.sh WORK_DIR TEMPLATE_ID LIBRARY_GITHUB LIBRARY_ID LIBRARY_GIT_TAG
+#
+# example:
+# create-tagged-lib.sh /tmp/abcd new-template leanprover/cslib cslib v4.32.0
+#
+# expects $WORK_DIR/build/Main.lean to 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
+LIBRARY_GITHUB="$1"; shift 1
+LIBRARY_ID="$1"; shift 1
+LIBRARY_GIT_TAG="$1"; shift 1
+TOOLCHAIN="leanprover/lean4:$LIBRARY_GIT_TAG"
+
+trap 'rm -rf "$WORK_DIR"' EXIT
+
+if [ -d "$ROOT/templates/$TEMPLATE_ID" ]; then
+  echo "ERROR: template '$TEMPLATE_ID' already exists"
+  exit 1
+fi
+
+if [ -d "$ROOT/package-sets/$TEMPLATE_ID" ]; then
+  echo "ERROR: package set '$TEMPLATE_ID' already exists"
+  exit 1
+fi
+
+echo "[[ progress 1/8 Constructing project ]]"
+BUILD_DIR="$WORK_DIR/build"
+cd "$BUILD_DIR"
+
+echo "$TOOLCHAIN" > lean-toolchain
+
+cat > lakefile.toml <<EOF
+name = "$TEMPLATE_ID"
+version = "0.1.0"
+defaultTargets = ["Main"]
+
+[[require]]
+name = "$LIBRARY_ID"
+git = "https://github.com/$LIBRARY_GITHUB"
+rev = "$LIBRARY_GIT_TAG"
+
+[[lean_lib]]
+name = "Main"
+EOF
+
+echo "[[ progress 2/8 Acquiring source for $LIBRARY_ID ]]"
+mkdir -p .lake/packages
+git clone --filter=tree:0 --branch "$LIBRARY_GIT_TAG" --progress "https://github.com/$LIBRARY_GITHUB" ".lake/packages/$LIBRARY_ID"
+
+echo "[[ progress 3/8 Acquiring project dependencies ]]"
+MATHLIB_NO_CACHE_ON_UPDATE=1 lake --keep-toolchain --no-ansi update
+
+echo "[[ progress 4/8 Downloading Mathlib cache ]]"
+lake --no-ansi exe cache get
+
+echo "[[ progress 5/8 Building project ]]"
+lake --no-ansi build
+
+echo "[[ progress 6/8 Constructing package set ]]"
+PACKAGE_SET_DIR="$WORK_DIR/package-set"
+mkdir "$PACKAGE_SET_DIR"
+
+for pkg_dir in "$BUILD_DIR/.lake/packages"/*/; do
+  pkg_name=$(basename "$pkg_dir")
+  echo "[package set] copying package: $pkg_name"
+  pkg_dest="$PACKAGE_SET_DIR/$pkg_name/.lake/packages/$pkg_name"
+  mkdir -p "$(dirname "$pkg_dest")"
+  mv --strip-trailing-slashes "$pkg_dir" "$pkg_dest"
+done
+
+ls -d "$PACKAGE_SET_DIR"/*/ | xargs -n1 basename > "$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"

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 <https://github.com/leanprover-community/mathlib4>.
+ *  - If `match[1] === 'lean4-nightly'`,
+ *    then `match[2]` is a candidate for a tag of <https://github.com/leanprover-community/mathlib4-nightly-testing/>
+ */
+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<typeof zWorkspaceMetadata>

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<ActionResponse<boolean>> => {
+    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'