From d39b3920a448f4bc7bcb6855bc5d57c3e292bfe1 Mon Sep 17 00:00:00 2001
From: Joe Kerrigan <kerrijoe@amazon.com>
Date: Wed, 3 Dec 2025 18:10:37 +0000
Subject: [PATCH] chore: support AL2 development using build container

You can't develop KLR on AL2 because its version of glibc is too old.
Set up a Docker container to enable development on AL2 and other
unsupported platforms.
---
 README.md                            | 15 ++++++++++++++
 build_container/Dockerfile           |  8 +++++++
 build_container/README.md            | 31 ++++++++++++++++++++++++++++
 build_container/build_container_exec | 19 +++++++++++++++++
 lakew                                |  8 +++++++
 5 files changed, 81 insertions(+)
 create mode 100644 build_container/Dockerfile
 create mode 100644 build_container/README.md
 create mode 100755 build_container/build_container_exec
 create mode 100755 lakew

diff --git a/README.md b/README.md
index 82b8ed1c..c3f23602 100644
--- a/README.md
+++ b/README.md
@@ -29,6 +29,21 @@ using `pip`:
 
 For more information see the [Getting Started Guide](docs/getting_started.md)
 
+## Development commands
+
+```
+# Build the project
+lake build
+
+# Re-generate files under interop/KLR
+lake build Extract
+
+# Run KLR executable
+lake exe klr
+```
+
+**Note**: if you are building using Amazon Linux 2, you will probably want to use the [build container](build_container/README.md).
+
 # Interop with Python
 
 The KLR compiler starts with Python code (e.g. NKI kernels), and converts this
diff --git a/build_container/Dockerfile b/build_container/Dockerfile
new file mode 100644
index 00000000..bd2cda72
--- /dev/null
+++ b/build_container/Dockerfile
@@ -0,0 +1,8 @@
+FROM ubuntu:latest
+
+RUN apt-get update && apt-get install -y curl git && rm -rf /var/lib/apt/lists/*
+
+RUN curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
+ENV PATH="/root/.elan/bin:${PATH}"
+
+WORKDIR /workspace
\ No newline at end of file
diff --git a/build_container/README.md b/build_container/README.md
new file mode 100644
index 00000000..8a4639b7
--- /dev/null
+++ b/build_container/README.md
@@ -0,0 +1,31 @@
+# KLR build container
+
+Amazon Linux 2 (AL2) currently uses an old GLIBC version that is not supported by our Lean toolchain.
+We provide a Docker image that can be used for development on AL2 and other unsupported platforms.
+
+## Usage
+
+The project root contains a simple wrapper script, `lakew`. Use `lakew` in place of `lake`:
+
+```
+$ ./lakew build
+<...>
+Build completed successfully (575 jobs).
+$ ./lakew exe klr
+klr [0.0.12]
+KLR is an IR for NKI and other tensor-like languages in Lean.
+
+USAGE:
+    klr [SUBCOMMAND] [FLAGS]
+
+FLAGS:
+    -h, --help  Prints this message.
+    --version   Prints the version.
+
+SUBCOMMANDS:
+    compile  Compile a NKI kernel
+    gather   Gather Python sources into an AST file
+    info     Display information about a KLR file
+    trace    Trace Python to KLR
+    list     List builtin functions and constants
+```
\ No newline at end of file
diff --git a/build_container/build_container_exec b/build_container/build_container_exec
new file mode 100755
index 00000000..017dc499
--- /dev/null
+++ b/build_container/build_container_exec
@@ -0,0 +1,19 @@
+#!/bin/bash
+# build_container_exec: run a command inside build container
+
+cd "$(dirname "$0")/.." || exit 1
+
+if ! docker image inspect klr-build &>/dev/null; then
+    echo "Error: klr-build image not found."
+    read -p "Build it now? (y/n) " -n 1 -r
+    echo
+    if [[ $REPLY =~ ^[Yy]$ ]]; then
+        docker build -t klr-build build_container/ || exit 1
+    else
+        exit 1
+    fi
+fi
+
+# Mount project directory at /workspace so generated sources end up in the right place.
+# Override ELAN_HOME and mount it as a volume so we cache Lean toolchains in between invocations.
+docker run -it --rm -v "$(pwd):/workspace" -v /tmp/klr-elan:/elan -e ELAN_HOME=/elan -w /workspace klr-build "$@"
\ No newline at end of file
diff --git a/lakew b/lakew
new file mode 100755
index 00000000..2e7cd87d
--- /dev/null
+++ b/lakew
@@ -0,0 +1,8 @@
+#!/bin/bash
+# lakew: lake wrapper
+# runs lake inside build container
+# see build_container/README.md for additional details
+
+cd "$(dirname "$0")" || exit 1
+
+./build_container/build_container_exec lake "$@"
\ No newline at end of file