Home
April 28, 2025

Running the Rocq and Lean Provers in Testcontainers

Curiously neither Rocq (formerly Coq) nor Lean has any official write-up (that I could find) on how to invoke these provers from within a container. I’m using Docker and Java’s Testcontainers here, but most of this should generalize to other contexts.

Rocq

The Dockerfile is simple enough that you can provide the image coordinates to Testcontainers directly instead, but I chose to create one for future customization:

FROM rocq/rocq-prover:9.0@sha256:853108e7c0bf2a04e2ecd970e0b22dc97d5ebbc99f7252942972f3eb670bcbf2

Assuming this Dockerfile is placed in src/{main,test,testFixtures}/resources, creation of the container via Testcontainers looks like this:

GenericContainer<?> container = new GenericContainer<>(
        new ImageFromDockerfile()
                .withFileFromClasspath("Dockerfile", "com/yourpackage/Dockerfile"))
    .withCommand("sleep", "infinity")
    .waitingFor(Wait.forSuccessfulCommand("eval $(opam env) && rocq -v"));

The rocq binary is managed by opam, hence the need to bring in opam-defined environment variables. There’s probably a way to push the eval $(opam env) into the Dockerfile (by applying it to e.g., the default login shell) but I didn’t bother myself.

Once the container is started, either by you calling container.start() or by annotating the definition with @Container in a @Testcontainers-annotated test class, you can run the prover like so:

String command = String.format(
      """
      INFILE="/tmp/in.v" \
      && echo -e "%s" > ${INFILE} \
      && eval $(opam env) \
      && rocq c ${INFILE} \
      """,
      input.replaceAll("\"", "\\\""));
Container.ExecResult execResult = execInContainer("bash", "-c", command);

I’m using rocq c (“c” for “compile”) rather than rocq repl:

  • rocq repl always returns an exit code of 0, even after encountering an error (understandable, it’s a REPL)
  • rocq repl emits substantial whitespace and formatting (also understandable)
  • the downside of using rocq c is that there appears to be no way to pipe input via stdin, hence the provision of an input file here, but that downside is outweighed (for my use case) by the return of a proper exit code and non-extraneous output formatting.

Also note that for some reason Rocq requires all input files to be suffixed with a .v extension.

Lean

I was unable to find an official container image for the Lean prover; this is the one I came up with:

FROM debian:stable-slim@sha256:00a24d7c50ebe46934e31f6154c0434e2ab51259a65e028be42413c636385f7f

USER root
RUN apt-get update
RUN apt-get install curl -y
RUN apt-get clean

# create a non-root user
RUN useradd -m lean
USER lean
WORKDIR /home/lean

SHELL ["/bin/bash", "-c"]

# make sure binaries are available even in non-login shells
ENV PATH="/home/lean/.elan/bin:/home/lean/.local/bin:$PATH"

RUN curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
RUN elan --version

# Use a stable release of Lean.
RUN elan default leanprover/lean4:v4.18.0

# Invoke lake (Lean's pkg manager) to trigger elan to install it.
RUN lake --version

# Invoke lean to trigger elan to install it.
RUN lean --version

Notes:

  • I would have used alpine, but Lean doesn’t work with musl, it requires glibc.
  • lean appears to only be installed at time of first invocation; in other words, omitting the lean --version here (or any use of the lean binary, regardless of provided flags) will defer installation of lean to its first invocation when the container is running, rather than pre-installing it at build-time into the image.

Assuming this Dockerfile is placed in src/{main,test,testFixtures}/resources, creation of the container via Testcontainers looks like this:

GenericContainer<?> container = new GenericContainer<>(
        new ImageFromDockerfile()
                .withFileFromClasspath("Dockerfile", "com/yourpackage/Dockerfile"))
    .withCommand("sleep", "infinity")
    .waitingFor(Wait.forSuccessfulCommand("lean --version"));

Once the container is started, either by you calling container.start() or by annotating the definition with @Container in a @Testcontainers-annotated test class, you can run the prover like so:

String command = String.format("echo -e \"%s\" | lean --stdin --json",
        code.replaceAll("\"", "\\\""));
Container.ExecResult execResult = execInContainer("bash", "-c", command);

Thankfully, the Lean prover allows input from stdin, and optionally formats output in JSON when the --json flag is provided.

← return home