From 4ba518e2582c7a3d8692255c50f3a575c7f48608 Mon Sep 17 00:00:00 2001 From: keyboardDrummer-bot Date: Fri, 1 May 2026 10:52:18 +0000 Subject: [PATCH 1/2] Add devcontainer with Lean, Claude Code, Kiro CLI, and GitHub MCP - Dockerfile installs elan, Node.js, Claude Code CLI, Kiro CLI, and uv - postCreate.sh installs the Lean toolchain and runs lake build/test to populate build caches - GitHub CLI added via devcontainer feature - GitHub MCP server configured for both Kiro and Claude Code - Lean4 VS Code extension included Closes #32 --- .claude/settings.json | 11 +++++++++++ .devcontainer/Dockerfile | 29 +++++++++++++++++++++++++++++ .devcontainer/devcontainer.json | 17 +++++++++++++++++ .devcontainer/postCreate.sh | 9 +++++++++ .kiro/settings/mcp.json | 10 +++++++++- 5 files changed, 75 insertions(+), 1 deletion(-) create mode 100644 .claude/settings.json create mode 100644 .devcontainer/Dockerfile create mode 100644 .devcontainer/devcontainer.json create mode 100755 .devcontainer/postCreate.sh diff --git a/.claude/settings.json b/.claude/settings.json new file mode 100644 index 0000000000..b7067fce0f --- /dev/null +++ b/.claude/settings.json @@ -0,0 +1,11 @@ +{ + "mcpServers": { + "github": { + "command": "npx", + "args": [ + "-y", + "@modelcontextprotocol/server-github" + ] + } + } +} diff --git a/.devcontainer/Dockerfile b/.devcontainer/Dockerfile new file mode 100644 index 0000000000..db22f1cae0 --- /dev/null +++ b/.devcontainer/Dockerfile @@ -0,0 +1,29 @@ +FROM ubuntu:24.04 + +ARG DEBIAN_FRONTEND=noninteractive + +# Install base dependencies +RUN apt-get update && apt-get install -y --no-install-recommends \ + curl wget git ca-certificates unzip python3 python3-pip pipx \ + && rm -rf /var/lib/apt/lists/* + +# Install Node.js (needed for Claude Code and Kiro CLI) +RUN curl -fsSL https://deb.nodesource.com/setup_22.x | bash - \ + && apt-get install -y nodejs \ + && rm -rf /var/lib/apt/lists/* + +# Install elan (Lean version manager) and the toolchain specified in lean-toolchain +RUN curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | bash -s -- -y --default-toolchain none +ENV PATH="/root/.elan/bin:${PATH}" + +# Install Claude Code CLI +RUN npm install -g @anthropic-ai/claude-code + +# Install Kiro CLI +RUN npm install -g kiro + +# Install uv (needed for lean-lsp-mcp via uvx) +RUN pipx install uv +ENV PATH="/root/.local/bin:${PATH}" + +WORKDIR /workspaces/Strata diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json new file mode 100644 index 0000000000..057f6c4340 --- /dev/null +++ b/.devcontainer/devcontainer.json @@ -0,0 +1,17 @@ +{ + "name": "Strata", + "build": { + "dockerfile": "Dockerfile" + }, + "features": { + "ghcr.io/devcontainers/features/github-cli:1": {} + }, + "postCreateCommand": ".devcontainer/postCreate.sh", + "customizations": { + "vscode": { + "extensions": [ + "leanprover.lean4" + ] + } + } +} diff --git a/.devcontainer/postCreate.sh b/.devcontainer/postCreate.sh new file mode 100755 index 0000000000..2304460da6 --- /dev/null +++ b/.devcontainer/postCreate.sh @@ -0,0 +1,9 @@ +#!/bin/bash +set -euo pipefail + +# Install the Lean toolchain specified in lean-toolchain +elan install "$(cat lean-toolchain)" + +# Build and test to populate the Lake cache +lake build +lake test diff --git a/.kiro/settings/mcp.json b/.kiro/settings/mcp.json index 29a35b076b..fedfc81326 100644 --- a/.kiro/settings/mcp.json +++ b/.kiro/settings/mcp.json @@ -27,6 +27,14 @@ "lean_local_search", "lean_verify" ] + }, + "github": { + "command": "npx", + "args": [ + "-y", + "@modelcontextprotocol/server-github" + ], + "disabled": false } } -} \ No newline at end of file +} From cd563f14190c9a978ab8fc6bb6f4ba7d80f83066 Mon Sep 17 00:00:00 2001 From: keyboardDrummer-bot Date: Fri, 1 May 2026 11:45:21 +0000 Subject: [PATCH 2/2] Install cvc5 and z3 in devcontainer, exclude Python tests Add cvc5 v1.2.1 and z3 v4.15.2 to the Dockerfile (matching CI versions) so that lake test can find the SMT solvers it needs. Exclude Languages.Python from lake test in postCreate.sh since those tests require a separate Python toolchain setup (matching CI behavior). --- .devcontainer/Dockerfile | 24 ++++++++++++++++++++++++ .devcontainer/postCreate.sh | 2 +- 2 files changed, 25 insertions(+), 1 deletion(-) diff --git a/.devcontainer/Dockerfile b/.devcontainer/Dockerfile index db22f1cae0..df90fe1a05 100644 --- a/.devcontainer/Dockerfile +++ b/.devcontainer/Dockerfile @@ -16,6 +16,30 @@ RUN curl -fsSL https://deb.nodesource.com/setup_22.x | bash - \ RUN curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | bash -s -- -y --default-toolchain none ENV PATH="/root/.elan/bin:${PATH}" +# Install cvc5 (required by Strata tests) +RUN ARCH=$(uname -m) \ + && if [ "$ARCH" = "x86_64" ]; then ARCH_NAME="x86_64"; \ + elif [ "$ARCH" = "aarch64" ] || [ "$ARCH" = "arm64" ]; then ARCH_NAME="arm64"; \ + else echo "Unsupported architecture: $ARCH" && exit 1; fi \ + && wget -q https://github.com/cvc5/cvc5/releases/download/cvc5-1.2.1/cvc5-Linux-${ARCH_NAME}-static.zip \ + && unzip -q cvc5-Linux-${ARCH_NAME}-static.zip \ + && mv cvc5-Linux-${ARCH_NAME}-static/bin/cvc5 /usr/local/bin/ \ + && rm -rf cvc5-Linux-${ARCH_NAME}-static* + +# Install z3 (required by Strata tests) +RUN ARCH=$(uname -m) \ + && if [ "$ARCH" = "x86_64" ]; then \ + wget -q https://github.com/Z3Prover/z3/releases/download/z3-4.15.2/z3-4.15.2-x64-glibc-2.39.zip \ + && unzip -q z3-4.15.2-x64-glibc-2.39.zip \ + && mv z3-4.15.2-x64-glibc-2.39/bin/z3 /usr/local/bin/ \ + && rm -rf z3-4.15.2-x64-glibc-2.39*; \ + elif [ "$ARCH" = "aarch64" ] || [ "$ARCH" = "arm64" ]; then \ + wget -q https://github.com/Z3Prover/z3/releases/download/z3-4.15.2/z3-4.15.2-arm64-glibc-2.34.zip \ + && unzip -q z3-4.15.2-arm64-glibc-2.34.zip \ + && mv z3-4.15.2-arm64-glibc-2.34/bin/z3 /usr/local/bin/ \ + && rm -rf z3-4.15.2-arm64-glibc-2.34*; \ + else echo "Unsupported architecture: $ARCH" && exit 1; fi + # Install Claude Code CLI RUN npm install -g @anthropic-ai/claude-code diff --git a/.devcontainer/postCreate.sh b/.devcontainer/postCreate.sh index 2304460da6..eb770d1d18 100755 --- a/.devcontainer/postCreate.sh +++ b/.devcontainer/postCreate.sh @@ -6,4 +6,4 @@ elan install "$(cat lean-toolchain)" # Build and test to populate the Lake cache lake build -lake test +lake test -- --exclude Languages.Python