Sign inSign up

ltchentw/agda

By ltchentw

•Updated over 1 year ago

Agda is a dependently typed programming language / interactive theorem prover.

Image
Languages & frameworks
0

2.3K

ltchentw/agda repository overview

⁠An unofficial Docker image for Agda

⁠Content

This Docker image includes

  1. Agda (/opt/agda)
  2. The standard library (/opt/agda/lib/agda-stdlib-*/)
  3. (Optional) Emacs with the Agda mode installed

⁠Tags

The tag name indicates the version of Agda and if Emacs is included in the image.

[Agda-ver]
[Agda-ver]-no-emacs

The latest refers to the last commit on the master branch of the Dockerfile repo, not the Agda’s official repo.

⁠Usage

  • It can be used directly to check and play with an Agda project in the current working directory:
docker run -it --mount type=bind,source"=${PWD}",destination=/root -w /root ltchentw/agda:latest
  • It can be used as a base image
FROM ltchen/agda:latest 

without having to compile Agda first.

⁠Build configuration

It is based on the latest Docker image of Alpine Linux⁠ and built in two stages.

  1. The first stage builds a statically linked Agda using GHC and Cabal.
  2. The second stage copies the executables and required data from the first stage and set up the environment.
⁠Dockerfile

The Dckerfiles are maintained at https://github.com/L-TChen/docker-agda/⁠. Images are built by GitHub workflows.

Tag summary

Content type

Image

Digest

sha256:c4b967b29…

Size

74.6 MB

Last updated

over 1 year ago

docker pull ltchentw/agda