Add devcontainer configuration

[keyboardDrummer-bot]

Adds a devcontainer configuration for the Strata project.

Changes

.devcontainer/Dockerfile — Custom image based on Ubuntu 24.04 with:

• elan (Lean version manager)
• Node.js 22 (for Claude Code and Kiro CLIs)
• Claude Code CLI (@anthropic-ai/claude-code)
• Kiro CLI (kiro)
• uv (for uvx used by the lean-lsp MCP server)

.devcontainer/devcontainer.json — Container config with:

• GitHub CLI via devcontainer feature
• postCreateCommand that runs lake build and lake test to populate build caches
• Lean4 VS Code extension

.devcontainer/postCreate.sh — Installs the Lean toolchain from lean-toolchain and runs lake build + lake test to create build caches in the prebuilt snapshot.

.claude/settings.json — GitHub MCP server configuration for Claude Code.

.kiro/settings/mcp.json — Added GitHub MCP server to existing Kiro MCP configuration (alongside the existing lean-lsp server).

Closes #32

[keyboardDrummer-bot]

The failing CI check "Run internal benchmarks of Strata" is a pre-existing failure unrelated to this PR.

The strata-benchmarks job in .github/workflows/ci.yml requires AWS credentials (secrets.AWS_BENCHMARK_ACCOUNT) to assume an IAM role and trigger a CodeBuild project against strata-org/Strata.git. This infrastructure is configured for the upstream strata-org/Strata repository — the secrets are not available in this fork (keyboardDrummer/Strata), so the job fails at the "Configure AWS credentials" step.

This PR only adds devcontainer configuration files (.devcontainer/, .claude/settings.json, .kiro/settings/mcp.json) and does not modify any CI workflows or source code. The same benchmark job would fail on any PR in this fork.

[keyboardDrummer]

Could you use the github-mcp-server CLI ?

"github": {
  "type": "stdio",
  "command": "github-mcp-server",
  "args": ["stdio", "--exclude-tools", "push_files,create_or_update_file,delete_file"],
  "autoApprove": ["*"]
}

[keyboardDrummer]

@keyboardDrummer-bot can you test whether lake build and lake test pass with this devcontainer file? You might have to use the devcontainer CLI tool

[keyboardDrummer-bot]

I built the devcontainer image and ran lake build and lake test inside it. Here are the results:

lake build — ✅ passes (571/571 jobs completed successfully)

lake test — ❌ fails due to two categories of missing dependencies:

1. Missing cvc5 SMT solver — The majority of test failures are because cvc5 is not installed in the container. Many tests use #guard_msgs that expect SMT solver results, but get could not execute external process 'cvc5' errors instead. Affected test files include:

   • StrataTest/Languages/Core/Tests/VCGPathTests.lean
   • StrataTest/Languages/Core/Tests/LambdaHigherOrderTests.lean
   • StrataTest/Languages/Core/Tests/ExprEvalTest.lean
   • StrataTest/DL/Imperative/Examples.lean
   • StrataTest/Languages/Boole/find_max_verus.lean
   • And ~120+ other test files across Core, Boole, Laurel, C_Simp, and Python language tests

2. Missing B3 verifier dependency — The B3 verifier tests fail with resource vanished (error code: 32, broken pipe), suggesting a missing external process (likely the B3/Z3 solver).

The Dockerfile needs to install cvc5 (and possibly z3) to make lake test pass. For example, adding something like:

# Install cvc5
RUN wget -q https://github.com/cvc5/cvc5/releases/download/cvc5-1.2.0/cvc5-Linux-x86_64-static.zip \
    && unzip cvc5-Linux-x86_64-static.zip \
    && mv cvc5-Linux-x86_64-static/bin/cvc5 /usr/local/bin/ \
    && rm -rf cvc5-Linux-x86_64-static*

[keyboardDrummer]

@keyboardDrummer-bot please update the PR until the devcontainers file produces something that enables lake build and lake test to pass

[keyboardDrummer-bot]

The failing check "Run internal benchmarks of Strata" is a pre-existing issue unrelated to this PR. The strata-benchmarks CI job uses aws-actions/configure-aws-credentials with secrets.AWS_BENCHMARK_ACCOUNT and an OIDC role scoped to strata-org/Strata. Since this is the keyboardDrummer/Strata fork, the AWS credential step fails because the secret is unavailable or the OIDC trust policy doesn't cover this repository.

This same failure also occurs on PR #31 (and presumably all PRs in this fork). The CI workflow file is unchanged by this PR — the job definition on main and on this branch are identical.

This is not fixable from within this PR. The fix would need to happen in the AWS account's OIDC trust policy or by making the benchmark job conditional (e.g., only running on strata-org/Strata).