feat: add hub with login.

Author: mchav

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "repl"]
+	path = repl
+	url = https://github.com/leanprover-community/repl

Dockerfile

@@ -13,7 +13,8 @@ COPY . /opt/build
 
 RUN mkdir -p /opt/bin \
   && cabal build exe:sabela \
-  && cp "$(cabal list-bin sabela)" /opt/bin/sabela
+  && cp "$(cabal list-bin sabela)" /opt/bin/sabela \
+  && strip /opt/bin/sabela
 
 # Pre-install dataframe package in build stage so we can copy the store
 RUN cabal install dataframe
@@ -24,26 +25,10 @@ FROM haskell:9.12.2-bookworm
 RUN apt-get update && apt-get install -y --no-install-recommends \
   python3 \
   python3-venv \
-  tini \
+  curl \
   && rm -rf /var/lib/apt/lists/*
 
-
-# Install Python ML packages in a venv (no cache, no .pyc)
-ENV VIRTUAL_ENV="/opt/venv"
-RUN python3 -m venv $VIRTUAL_ENV
-ENV PATH="$VIRTUAL_ENV/bin:${PATH}"
-RUN pip install --no-cache-dir --no-compile numpy pandas scikit-learn matplotlib \
-  && find $VIRTUAL_ENV -name '__pycache__' -exec rm -rf {} + 2>/dev/null || true
-
-# Install elan (Lean 4 toolchain manager)
-ENV ELAN_HOME="/root/.elan"
-ENV PATH="${ELAN_HOME}/bin:${PATH}"
-RUN curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
-     | sh -s -- -y --default-toolchain leanprover/lean4:v4.29.0
-
-# Verify installations
-RUN python3 --version && lean --version && lake --version
-
+# ---------- Assemble final image ----------
 WORKDIR /opt/sabela
 
 # Copy compiled binary
@@ -61,6 +46,27 @@ COPY ./examples /opt/sabela/examples/
 
 ENV CABAL_DIR="/root/.cabal"
 
-ENTRYPOINT ["/usr/bin/tini", "--"]
-
+# Entrypoint script prepends EFS tool paths to PATH at runtime
+# (avoids hardcoding PATH in task definition, which broke GHC discovery)
+COPY <<'SCRIPT' /opt/bin/start.sh
+#!/bin/sh
+# Add EFS-mounted tools to PATH if they exist
+[ -d "/mnt/sabela/python/venv/bin" ] && export PATH="/mnt/sabela/python/venv/bin:$PATH"
+[ -d "/mnt/sabela/lean/.elan/bin" ] && export PATH="/mnt/sabela/lean/.elan/bin:$PATH"
+
+# If a user work directory is specified (3rd arg = sabela's 2nd arg), set it up
+WORKDIR="${3:-.}"
+if echo "$WORKDIR" | grep -q "^/mnt/sabela/users/"; then
+  mkdir -p "$WORKDIR"
+  # Copy examples into user dir if not already there
+  if [ ! -d "$WORKDIR/examples" ]; then
+    cp -r /opt/sabela/examples "$WORKDIR/examples"
+  fi
+fi
+
+exec "$@"
+SCRIPT
+RUN chmod +x /opt/bin/start.sh
+
+ENTRYPOINT ["/opt/bin/start.sh"]
 CMD ["/opt/bin/sabela", "3000", "."]

examples/lean-tactics.md

@@ -0,0 +1,106 @@
+# Lean 4: Commands and Tactic Proofs
+
+This notebook demonstrates Lean 4's dual nature as both a programming language and a proof assistant. We define data types and functions (commands), then prove properties about them (tactics).
+
+## Defining a binary tree
+
+An inductive type for binary trees with values at the leaves:
+
+```lean4
+inductive Tree (α : Type) where
+  | leaf : α → Tree α
+  | node : Tree α → Tree α → Tree α
+deriving Repr
+```
+
+## Computing with trees
+
+Recursive functions over our tree type — size counts leaves, depth measures the longest path:
+
+```lean4
+def Tree.size : Tree α → Nat
+  | .leaf _ => 1
+  | .node l r => l.size + r.size
+
+def Tree.depth : Tree α → Nat
+  | .leaf _ => 0
+  | .node l r => 1 + max l.depth r.depth
+
+def Tree.map (f : α → β) : Tree α → Tree β
+  | .leaf x => .leaf (f x)
+  | .node l r => .node (l.map f) (r.map f)
+
+-- Test with a small tree
+def exTree := Tree.node (Tree.node (Tree.leaf 1) (Tree.leaf 2)) (Tree.leaf 3)
+
+#eval exTree.size   -- 3
+#eval exTree.depth  -- 2
+```
+
+## Proving size is always positive
+
+Every tree has at least one leaf, so size is always at least 1:
+
+```lean4
+theorem Tree.size_pos (t : Tree α) : t.size ≥ 1 := by
+  induction t with
+  | leaf _ => simp [Tree.size]
+  | node l r ihl ihr => simp [Tree.size]; omega
+```
+
+## Map preserves structure
+
+Mapping a function over a tree doesn't change its shape:
+
+```lean4
+theorem Tree.size_map (f : α → β) (t : Tree α) : (t.map f).size = t.size := by
+  induction t with
+  | leaf _ => simp [Tree.map, Tree.size]
+  | node l r ihl ihr => simp [Tree.map, Tree.size, ihl, ihr]
+
+theorem Tree.depth_map (f : α → β) (t : Tree α) : (t.map f).depth = t.depth := by
+  induction t with
+  | leaf _ => simp [Tree.map, Tree.depth]
+  | node l r ihl ihr => simp [Tree.map, Tree.depth, ihl, ihr]
+```
+
+## Depth bounds size
+
+The depth of a tree is always less than its size (since depth counts edges on the longest path, while size counts all leaves):
+
+```lean4
+theorem Tree.depth_lt_size (t : Tree α) : t.depth < t.size := by
+  induction t with
+  | leaf _ => simp [Tree.size, Tree.depth]
+  | node l r ihl ihr =>
+    simp [Tree.size, Tree.depth]
+    omega
+```
+
+## A verified lookup function
+
+Define a mirroring operation and prove it is involutive (applying it twice gives back the original):
+
+```lean4
+def Tree.mirror : Tree α → Tree α
+  | .leaf x => .leaf x
+  | .node l r => .node r.mirror l.mirror
+
+theorem Tree.mirror_mirror (t : Tree α) : t.mirror.mirror = t := by
+  induction t with
+  | leaf _ => simp [Tree.mirror]
+  | node l r ihl ihr => simp [Tree.mirror, ihl, ihr]
+```
+
+## Composing proofs
+
+We can combine earlier results. Mirror preserves size because it just swaps children:
+
+```lean4
+theorem Tree.size_mirror (t : Tree α) : t.mirror.size = t.size := by
+  induction t with
+  | leaf _ => simp [Tree.mirror, Tree.size]
+  | node l r ihl ihr =>
+    simp [Tree.mirror, Tree.size, ihl, ihr]
+    omega
+```

examples/matplotlib-demo.md

@@ -5,6 +5,8 @@ Python cells can render matplotlib plots inline using base64-encoded PNG.
 ## Setup
 
 ```python
+# pip: matplotlib
+# pip: numpy
 import matplotlib
 matplotlib.use('Agg')
 import matplotlib.pyplot as plt

examples/tutorial-lean-integration.md

@@ -57,13 +57,13 @@ Lean's real power is theorem proving. A theorem is a type whose inhabitants are
 theorem one_plus_one : 1 + 1 = 2 := rfl
 
 -- Proof by simplification
-theorem add_zero (n : Nat) : n + 0 = n := by simp
+theorem my_add_zero (n : Nat) : n + 0 = n := by simp
 
 -- Proof by induction
-theorem add_comm (m n : Nat) : m + n = n + m := by
+theorem my_add_comm (m n : Nat) : m + n = n + m := by
   induction m with
   | zero => simp
-  | succ m ih => simp [Nat.succ_add, ih]
+  | succ m ih => omega
 ```
 
 When a proof succeeds, Sabela shows a green checkmark with "No goals". When it fails, you see the remaining proof state.
@@ -84,12 +84,12 @@ def double (n : Nat) := n * 2
 Lean's standard library is available. Imports from any cell are automatically hoisted to the top of the document.
 
 ```lean4
-import Lean.Data.HashMap
+import Std.Data.HashMap
 
 -- This works because the import is hoisted
-def myMap := Lean.HashMap.empty.insert "key" 42
+def myMap : Std.HashMap String Nat := Std.HashMap.ofList [("key", 42)]
 
-#eval myMap.find? "key"
+#eval myMap.get? "key"
 ```
 
 ## Using Mathlib
@@ -138,15 +138,15 @@ putStrLn $ "Fibonacci(15) from Lean: " ++ _bridge_lean_result
 
 ## Reactivity
 
-When you edit a Lean cell, only that cell and all cells below it are re-checked (Lean elaborates top-to-bottom). Cells above the edit point are cached by the LSP server, so edits at the bottom of a notebook are fast.
+When you edit a Lean cell, that cell and all cells below it are re-executed. Cells are evaluated sequentially from top to bottom, with each cell's environment building on the previous one.
 
 ## Cell execution model
 
-Unlike Haskell cells which run individually, all Lean cells are assembled into a single `.lean` file and sent to the Lean language server. This means:
+Lean cells are executed one at a time through a JSON REPL, with each cell's definitions chained into the next cell's environment. This means:
 
 - Definitions naturally flow downward
 - Errors in one cell may affect cells below it
-- The LSP provides incremental checking — only changed regions are re-elaborated
+- Each cell gets individual feedback (output or errors)
 
 ## Tips
 

infra/Dockerfile.efs-builder

@@ -0,0 +1,16 @@
+FROM haskell:9.12.2-bookworm
+
+RUN apt-get update && apt-get install -y --no-install-recommends \
+  python3 \
+  python3-venv \
+  curl \
+  && rm -rf /var/lib/apt/lists/*
+
+# Copy the REPL source so it's available at runtime
+COPY ./repl /opt/repl
+
+# Copy the build script
+COPY ./infra/build-efs.sh /opt/build-efs.sh
+RUN chmod +x /opt/build-efs.sh
+
+CMD ["/opt/build-efs.sh"]

infra/build-efs.sh

@@ -0,0 +1,53 @@
+#!/usr/bin/env bash
+set -euo pipefail
+
+EFS="/mnt/efs"
+
+echo "=== EFS Builder: populating $EFS ==="
+
+# ---------- Python venv ----------
+echo "[1/4] Creating Python venv..."
+python3 -m venv "$EFS/python/venv"
+"$EFS/python/venv/bin/pip" install --no-cache-dir --no-compile \
+  numpy pandas scikit-learn matplotlib
+find "$EFS/python/venv" -name '__pycache__' -exec rm -rf {} + 2>/dev/null || true
+echo "  Python venv ready at $EFS/python/venv"
+
+# ---------- Lean 4 toolchain ----------
+echo "[2/4] Installing Lean 4 toolchain..."
+export ELAN_HOME="$EFS/lean/.elan"
+curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
+  | sh -s -- -y --default-toolchain leanprover/lean4:v4.29.0
+export PATH="$ELAN_HOME/bin:$PATH"
+echo "  Lean installed: $(lean --version)"
+
+# ---------- Lean REPL ----------
+echo "[3/4] Building Lean REPL..."
+cp -a /opt/repl "$EFS/lean/repl"
+cd "$EFS/lean/repl"
+lake build
+echo "  REPL binary at $EFS/lean/repl/.lake/build/bin/repl"
+
+# ---------- Lean + Mathlib ----------
+echo "[4/4] Building Lean + Mathlib (this takes a while)..."
+mkdir -p "$EFS/lean/lean-base"
+cd "$EFS/lean/lean-base"
+cat > lakefile.toml <<'TOML'
+name = "scratch"
+version = "0.1.0"
+
+[[lean_lib]]
+name = "Scratch"
+
+[[require]]
+name = "mathlib"
+scope = "leanprover-community"
+TOML
+echo 'leanprover/lean4:v4.29.0' > lean-toolchain
+lake build
+echo "  Mathlib built at $EFS/lean/lean-base"
+
+echo ""
+echo "=== EFS Builder complete ==="
+echo "Contents:"
+du -sh "$EFS/python" "$EFS/lean" 2>/dev/null || true