feat: Add Lean and Python sessions with examples.

Author: mchav

.dockerignore

@@ -0,0 +1,9 @@
+dist-newstyle/
+.git/
+*.log
+test/
+.github/
+scripts/
+*.md
+!README.md
+!CHANGELOG.md

.gitignore

@@ -22,3 +22,4 @@ cabal.project.local~
 .HTF/
 .ghc.environment.*
 .DS_Store
+.sabela_cell.py

CLAUDE.md

@@ -30,13 +30,22 @@ The system has three layers: a Haskell backend (Servant/Warp), a static frontend
 
 | Module | Role |
 |--------|------|
+| `Sabela.Model` | Core domain types: `Notebook`, `Cell`, `NotebookEvent`, `CellError` |
+| `Sabela.State` | Composed `App` record with focused subsystems (`Environment`, `EventBus`, `NotebookStore`, `SessionManager`, `DependencyTracker`, `WidgetStore`, `BridgeStore`) |
 | `Sabela.Session` | Spawns and manages a GHCi subprocess; uses marker-based output capture to separate cell results |
-| `Sabela.Model` | Core data types: `AppState`, `Notebook`, `Cell`, `NotebookEvent` |
+| `Sabela.LeanSession` | Lean 4 LSP client session management |
+| `Sabela.PythonSession` | Python REPL subprocess management |
+| `Sabela.SessionTypes` | `SessionBackend` record-of-functions interface shared by all language backends |
 | `Sabela.Handlers` | Cell execution, reactivity engine, dependency tracking, session lifecycle |
+| `Sabela.Reactivity` | Pure execution planning: `ExecutionPlan`, topological ordering, error message generation |
+| `Sabela.Deps` | Pure metadata collection and merging for cabal dependencies |
+| `Sabela.Bridge` | Pure preamble generation for cross-language bridge values and widgets |
+| `Sabela.Topo` | Dependency graph construction and topological sort |
 | `Sabela.Server` | Servant HTTP API, SSE event streaming, file explorer, IDE helpers |
 | `Sabela.Api` | Request/response DTOs |
 | `Sabela.Output` | MIME type parsing, rich output helpers (HTML, SVG, Markdown, LaTeX, JSON) |
 | `Sabela.Errors` | Parses GHCi stderr to extract structured error locations |
+| `Sabela.LeanLsp` | LSP wire protocol types and helpers for Lean integration |
 
 ### Key Data Flow
 
@@ -84,6 +93,6 @@ Notebooks are plain Markdown files. Code blocks become executable cells; prose b
 
 - Module namespace: `Sabela.*`
 - HTTP handler functions use `H` suffix (e.g., `runCellH`, `getNotebookH`)
-- State parameters named `st` (AppState) or `rn` (ReactiveNotebook)
+- State parameters named `app` (App) or `rn` (ReactiveNotebook)
 - All file paths are canonicalized and security-checked to be within the work directory
 - Formatter: fourmolu with 4-space indent, 80-column limit, leading commas (see `fourmolu.yaml`)

Dockerfile

@@ -12,28 +12,68 @@ COPY . /opt/build
 
 RUN cabal install --installdir=/opt/bin --install-method=copy
 
-FROM haskell:9.8.4-slim-bullseye
+# Pre-install dataframe package in build stage so we can copy the store
+RUN cabal install dataframe
+
+# ---------- Runtime ----------
+FROM debian:bullseye-slim
 
-RUN apt-get update && apt-get install -y \
+RUN apt-get update && apt-get install -y --no-install-recommends \
   ca-certificates \
   libgmp10 \
+  libtinfo5 \
+  libffi-dev \
+  python3 \
+  python3-pip \
   tini \
+  curl \
   && rm -rf /var/lib/apt/lists/*
 
+# Install GHC + cabal via GHCup (minimal footprint, no HLS/Stack)
+ENV GHCUP_INSTALL_BASE_PREFIX="/opt"
+ENV PATH="/opt/.ghcup/bin:${PATH}"
+RUN curl -sSf https://get-ghcup.haskell.org | \
+    BOOTSTRAP_HASKELL_NONINTERACTIVE=1 \
+    BOOTSTRAP_HASKELL_GHC_VERSION=9.8.4 \
+    BOOTSTRAP_HASKELL_CABAL_VERSION=latest \
+    BOOTSTRAP_HASKELL_INSTALL_HLS=0 \
+    BOOTSTRAP_HASKELL_INSTALL_STACK=0 \
+    sh \
+  && rm -rf /opt/.ghcup/cache /opt/.ghcup/tmp
+
+# Remove curl now that GHCup is installed
+RUN apt-get purge -y curl && apt-get autoremove -y && rm -rf /var/lib/apt/lists/*
+
+# Install Python ML packages (no cache, no .pyc)
+RUN pip3 install --no-cache-dir --no-compile numpy pandas scikit-learn polars \
+  && find /usr/lib/python3 -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 apt-get update && apt-get install -y --no-install-recommends curl \
+  && curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
+     | sh -s -- -y --default-toolchain leanprover/lean4:v4.29.0 \
+  && apt-get purge -y curl && apt-get autoremove -y && rm -rf /var/lib/apt/lists/*
+
+# Verify installations
+RUN python3 --version && lean --version && lake --version
+
 WORKDIR /opt/sabela
 
+# Copy compiled binary
 COPY --from=build /opt/bin/sabela /opt/bin/sabela
 
+# Copy pre-built cabal store and package index from build stage
+COPY --from=build /root/.cabal/store /root/.cabal/store
+COPY --from=build /root/.cabal/packages /root/.cabal/packages
+
+# Copy static assets
 COPY --from=build /opt/build/static/ /opt/sabela/static/
 COPY --from=build /opt/build/display/ /opt/sabela/display/
 
 COPY ./examples /opt/sabela/examples/
 
-RUN cabal update
-
-RUN cabal install dataframe
-
 ENTRYPOINT ["/usr/bin/tini", "--"]
 
-CMD ["timeout", "900", "/opt/bin/sabela", "3000", "examples", \
-     "/root/.sabela/global.md", "granite", "text"]
+CMD ["/opt/bin/sabela", "3000", "."]

app/Main.hs

@@ -1,20 +1,28 @@
 module Main (main) where
 
+import Control.Exception (finally)
+import Control.Monad (when)
+import Data.Maybe (fromMaybe)
 import qualified Data.Set as S
 import GHC.IO.Encoding (setLocaleEncoding, utf8)
 import Network.Wai.Handler.Warp (run)
 import Sabela.Handlers (initGlobalEnv, initPreinstalledPackages, setupReactive)
-import Sabela.Server (initState, mkApp)
+import Sabela.Server (mkApp, newApp)
+import Sabela.State (App (..))
+import Sabela.State.Environment (Environment (..))
 import System.Directory (
+    doesDirectoryExist,
     getCurrentDirectory,
     getHomeDirectory,
+    removeDirectoryRecursive,
  )
-import System.Environment (getArgs)
+import System.Environment (getArgs, lookupEnv, setEnv)
 import System.FilePath (takeDirectory, (</>))
 
 main :: IO ()
 main = do
     setLocaleEncoding utf8
+    addElanToPath
     homeDir <- getHomeDirectory
     let defaultGlobal = homeDir </> ".sabela" </> "global.md"
     args <- getArgs
@@ -33,7 +41,23 @@ start port workDir globalFile pkgs = do
     globalDeps <- initGlobalEnv globalFile
     preinstalledDeps <- initPreinstalledPackages (takeDirectory globalFile) pkgs
     let allGlobalDeps = globalDeps `S.union` preinstalledDeps
-    st <- initState workDir allGlobalDeps
-    rn <- setupReactive st
+    app <- newApp workDir allGlobalDeps
+    rn <- setupReactive app
     putStrLn $ "sabela running on http://localhost:" ++ show port ++ "/index.html"
-    run port (mkApp st rn)
+    run port (mkApp app rn) `finally` cleanupTmpDir app
+
+-- | Add elan's bin directory to PATH so lake/lean are found.
+addElanToPath :: IO ()
+addElanToPath = do
+    home <- getHomeDirectory
+    let elanBin = home </> ".elan" </> "bin"
+    exists <- doesDirectoryExist elanBin
+    when exists $ do
+        path <- fromMaybe "" <$> lookupEnv "PATH"
+        setEnv "PATH" (elanBin ++ ":" ++ path)
+
+cleanupTmpDir :: App -> IO ()
+cleanupTmpDir app = do
+    let tmpDir = envTmpDir (appEnv app)
+    putStrLn $ "Cleaning up temp directory: " ++ tmpDir
+    removeDirectoryRecursive tmpDir

build.sh

@@ -1,3 +1,5 @@
+aws login
+aws ecr get-login-password --region us-east-1 | docker login --username AWS --password-stdin 768860981221.dkr.ecr.us-east-1.amazonaws.com
 docker build --platform linux/amd64 -t datahaskell/sabela .
 docker tag datahaskell/sabela:latest 768860981221.dkr.ecr.us-east-1.amazonaws.com/datahaskell/sabela:latest
 docker push 768860981221.dkr.ecr.us-east-1.amazonaws.com/datahaskell/sabela:latest