Containerfile

# SPDX-License-Identifier: MPL-2.0
# SPDX-FileCopyrightText: 2026 hyperpolymath
#
# GQLdt Development Container
# Lean 4 + Zig + Build Tools

FROM ubuntu:24.04

LABEL org.opencontainers.image.title="GQLdt Development Environment"
LABEL org.opencontainers.image.description="Lean 4 + Zig for dependently-typed Lith queries"
LABEL org.opencontainers.image.authors="Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"
LABEL org.opencontainers.image.licenses="MPL-2.0"

# Install system dependencies
RUN apt-get update && apt-get install -y \
    curl \
    git \
    build-essential \
    cmake \
    wget \
    ca-certificates \
    && rm -rf /var/lib/apt/lists/*

# Install elan (Lean version manager)
RUN curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf \
    | sh -s -- -y --default-toolchain leanprover/lean4:v4.15.0

ENV PATH="/root/.elan/bin:${PATH}"

# Install Zig
RUN wget -q https://ziglang.org/download/0.13.0/zig-linux-x86_64-0.13.0.tar.xz \
    && tar -xf zig-linux-x86_64-0.13.0.tar.xz \
    && mv zig-linux-x86_64-0.13.0 /usr/local/zig \
    && ln -s /usr/local/zig/zig /usr/local/bin/zig \
    && rm zig-linux-x86_64-0.13.0.tar.xz

# Verify installations
RUN lean --version && lake --version && zig version

# Set working directory
WORKDIR /workspace

# Copy project files
COPY . /workspace/

# Build the Zig FFI bridge FIRST: lakefile.lean links against
# bridge/zig-out/lib/liblith_bridge.a, so the Lean build needs this artifact to
# already exist. (The previous order built Lean first and masked the inevitable
# failure with `|| echo`, which also meant a genuinely broken build still
# produced a "successful" image.)
WORKDIR /workspace/bridge
RUN zig build && test -f zig-out/lib/liblith_bridge.a

# Build Lean 4 project (fetches mathlib on first run)
WORKDIR /workspace
RUN lake build

# Default command: interactive shell
CMD ["/bin/bash"]