chore: support AL2 development using build container

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

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

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
+```

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 "$@"

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 "$@"