docker-agda-mini

Small Docker images containing Agda.

See also: https://hub.docker.com/r/sourcedennis/agda-mini

The main purpose of these images is to provide easily reproducible Agda executions. Existing images were often humongous, at roughly ~2 GB (uncompressed). While mine are much smaller (~150MB uncompressed - 50MB compressed).

Tagging convention:

• There are images without the standard library, tagged with the Agda version number X.Y.Z.W.
• There are also images with the standard library, tagged as X.Y.Z.W-A.B.C, where X.Y.Z.W is the Agda version and A.B.C is the standard library version.

Example

If you have a local directory with Agda proofs called proofs/, you can create a Dockerfile like:

FROM sourcedennis/agda-mini:2.6.2.1-1.7.1

WORKDIR /proofs
COPY --chown=proof:proof proofs .

Note that proof is the user, which avoids issues with root.

Which you then build into a Docker image with:

docker build . --tag=my-proofs

You can execute your proofs with (assuming your proofs/ directory contains a file Proof.agda):

docker run -it --rm my-proofs agda Proof.agda

As Agda can render proofs to HTML, you can also run:

docker run -it --rm -v "$PWD/html:/proofs/html" my-proofs agda --html --html-dir=html Proof.agda

This creates a local html/ directory. You can open html/Proof.html in any browser.

Building the images

To build the Docker images with the Dockerfiles here, run these commands:

• Without the standard library (modify the version):

  docker build . --tag agda-mini:2.6.2.1 --build-arg AGDA_VERSION=2.6.2.1 --file Dockerfile

• With the standard library (modify the versions):

  docker build . --tag agda-mini:2.6.2.1-1.7.1 --build-arg AGDA_VERSION=2.6.2.1 --build-arg STDLIB_VERSION=1.7.1 --file stdlib.Dockerfile

Nightly

Theres also a nightly.Dockerfile for Agda's nightly release. It requires setting AGDA_VERSION to the version of next release (currently 2.6.3). Build it with:

docker build . --tag agda-mini:nightly --build-arg AGDA_VERSION=2.6.3 --file nightly.Dockerfile

I don't push the nightly version to DockerHub, because I don't think it should be used for reproducible builds.

Build History

The images on Dockerhub were built with build.sh. I rebuild them whenever a Dockerfile changes.

License

Public Domain - See the LICENSE file