Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
29 changes: 29 additions & 0 deletions .devcontainer/devcontainer-lock.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,29 @@
{
"features": {
"ghcr.io/devcontainers/features/common-utils:2": {
"version": "2.5.3",
"resolved": "ghcr.io/devcontainers/features/common-utils@sha256:3cf7ca93154faf9bdb128f3009cf1d1a91750ec97cc52082cf5d4edef5451f85",
"integrity": "sha256:3cf7ca93154faf9bdb128f3009cf1d1a91750ec97cc52082cf5d4edef5451f85"
},
"ghcr.io/devcontainers/features/docker-in-docker:2": {
"version": "2.12.2",
"resolved": "ghcr.io/devcontainers/features/docker-in-docker@sha256:842d2ed40827dc91b95ef727771e170b0e52272404f00dba063cee94eafac4bb",
"integrity": "sha256:842d2ed40827dc91b95ef727771e170b0e52272404f00dba063cee94eafac4bb"
},
"ghcr.io/devcontainers/features/github-cli:1": {
"version": "1.0.14",
"resolved": "ghcr.io/devcontainers/features/github-cli@sha256:ca677566507c4118e4368cd76a4800807e911e5e350cc3525fb67ebc9132dfa1",
"integrity": "sha256:ca677566507c4118e4368cd76a4800807e911e5e350cc3525fb67ebc9132dfa1"
},
"ghcr.io/edouard-lopez/devcontainer-features/bats:0": {
"version": "0.0.1",
"resolved": "ghcr.io/edouard-lopez/devcontainer-features/bats@sha256:8acd020fc45ebacdd399a29977c4d22cad56b5c95c43cdf2ae061f0e755aea7a",
"integrity": "sha256:8acd020fc45ebacdd399a29977c4d22cad56b5c95c43cdf2ae061f0e755aea7a"
},
"ghcr.io/joshuanianji/devcontainer-features/github-cli-persistence:1": {
"version": "1.0.3",
"resolved": "ghcr.io/joshuanianji/devcontainer-features/github-cli-persistence@sha256:757843d75915f140ec22bc16ccb5e657a910d9b1d1f445d15350a78e584d130f",
"integrity": "sha256:757843d75915f140ec22bc16ccb5e657a910d9b1d1f445d15350a78e584d130f"
}
}
}
File renamed without changes.
70 changes: 0 additions & 70 deletions .github/workflows/version-base-build-test.yml
Original file line number Diff line number Diff line change
Expand Up @@ -104,73 +104,3 @@ jobs:
run: |
docker run ${{ env.TAG }} /bin/bash -c "make test"

# "consumer" images just "consume" the base image and do nothing else
# basic tests for these
consumer-build-test:
name: Build Consumer
runs-on: ubuntu-latest
needs: [base-test-1, base-test-2]
strategy:
matrix:
dockerfile: [debian, ubuntu]
# use a local registry
services:
registry:
image: registry:2
ports:
- 5000:5000
env:
# use local registry so we can reference the base image in another dockerfile
# https://github.com/docker/build-push-action/issues/738
BASE_TAG: localhost:5000/base-${{ inputs.idris-version }}:latest
TAG: idris-consumer-${{ matrix.dockerfile }}-${{ inputs.idris-version }}:test
steps:
- name: Checkout Repo
uses: actions/checkout@v4

- name: Setup Buildx (no ARM)
uses: docker/setup-buildx-action@v3
with:
# since we're using a local registry
driver-opts: network=host

- name: Build Base Image
uses: ./.github/actions/build-base-img
with:
idris-version: ${{ inputs.idris-version }}
push: true
tags: ${{ env.BASE_TAG }}

- name: Run `docker image ls`
run: docker image ls

- name: Build ${{ matrix.dockerfile}}
uses: docker/build-push-action@v6
with:
context: .
file: ${{ matrix.dockerfile }}.Dockerfile
build-args: |
IDRIS_VERSION=${{ inputs.idris-version }}
BASE_IMG=${{ env.BASE_TAG }}
tags: ${{ env.TAG }}
load: true

- name: Setup Bats and Bats libs
uses: bats-core/[email protected]
with:
bats-version: 1.10.0
support-version: 0.3.0
support-path: ${{ github.workspace }}/.bats/bats-support
assert-version: 2.1.0
assert-path: ${{ github.workspace }}/.bats/bats-assert
file-install: false
detik-install: false

# LIB_PATH is a env var I use in the setup() function of my bats tests
# it points to the folder containing bats-assert and bats-support
- name: Run Test
env:
LIB_PATH: ${{ github.workspace }}/.bats
DOCKER_IMAGE: ${{ env.TAG }}
IDRIS_VERSION: ${{ inputs.idris-version }}
run: bats tests/consumer-idris.bats
43 changes: 0 additions & 43 deletions .github/workflows/version-base-deploy.yml
Original file line number Diff line number Diff line change
Expand Up @@ -54,46 +54,3 @@ jobs:
labels: ${{ steps.create-meta.outputs.labels }}
platforms: linux/amd64,linux/arm64

deploy-consumers:
name: Deploy Consumer
runs-on: ubuntu-latest
strategy:
matrix:
dockerfile: [ubuntu, debian]
needs: deploy-base
steps:
- name: Checkout Repo
uses: actions/checkout@v4

# instead of native builds, we'll just use QEMU for consumers
# consumer builds don't really do much intensive stuff anyway
- name: Set up QEMU
uses: docker/setup-qemu-action@v3

- name: Setup Buildx
uses: docker/setup-buildx-action@v3

- name: Login to GHCR
uses: docker/login-action@v3
with:
registry: ghcr.io
username: ${{ github.actor }}
password: ${{ secrets.GITHUB_TOKEN }}

- name: Docker meta
id: create-meta
uses: docker/metadata-action@v5
with:
images: ${{ github.repository }}/${{ matrix.dockerfile }}

- name: Build ${{ matrix.dockerfile}}
uses: docker/build-push-action@v6
with:
context: .
platforms: linux/amd64,linux/arm64
file: ${{ matrix.dockerfile }}.Dockerfile
build-args: |
IDRIS_VERSION=${{ inputs.idris-version }}
BASE_IMG=ghcr.io/${{ github.repository }}/base:${{ inputs.idris-version }}
tags: ghcr.io/${{ github.repository }}/${{ matrix.dockerfile }}:${{ inputs.idris-version }}
push: true
35 changes: 29 additions & 6 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@ Idris Versions: `v0.5.1`, `v0.6.0`, `v0.7.0`, `latest` (Up to date with [Idris2/
- [Running Locally](#running-locally)
- [Build Latest](#build-latest)
- [Build From a Tagged Release/SHA commit](#build-from-a-tagged-releasesha-commit)
- [Running tests](#running-tests)
- [Credit](#credit)

## Motivation
Expand All @@ -28,10 +29,8 @@ Installing Idris2 is [quite time consuming](https://idris2.readthedocs.io/en/lat

## Images

* [idris-2-docker/base](https://github.com/joshuanianji/idris-2-docker/pkgs/container/idris-2-docker%2Fbase) - Base image with Idris2 installed from source.
* [idris-2-docker/base](https://github.com/joshuanianji/idris-2-docker/pkgs/container/idris-2-docker%2Fbase) - Base image with Idris2 installed from source (debian-based)
* [idris-2-docker/devcontainer](https://github.com/joshuanianji/idris-2-docker/pkgs/container/idris-2-docker%2Fdevcontainer) - Includes [Idris2 LSP](https://github.com/idris-community/idris2-lsp)
* [idris-2-docker/ubuntu](https://github.com/joshuanianji/idris-2-docker/pkgs/container/idris-2-docker%2Fubuntu) - Ubuntu 20.04
* [idris-2-docker/debian](https://github.com/joshuanianji/idris-2-docker/pkgs/container/idris-2-docker%2Fdebian) - Debian bullseye

## Example Project

Expand Down Expand Up @@ -86,17 +85,41 @@ To run the images locally, I recommend opening the workspace in the Devcontainer
This is the default behaviour when running the script.

```bash
# this is the only module we need, so i chose not to create a requirements.txt file
pip install -U requests

# builds base from latest commit on the Idris repo. Tag is base-latest
python scripts/build-image.py --image base
python scripts/build-image.py --image devcontainer --tag devcontainer-latest-test
python scripts/build-image.py --image ubuntu
python scripts/build-image.py --image devcontainer --tag devcontainer-latest
```

### Build From a Tagged Release/SHA commit

```bash
python scripts/build-image.py --image base --version v0.6.0
python scripts/build-image.py --image base --version v0.7.0
python scripts/build-image.py --image base --sha 58e5d156621cfdd4c54df26abf7ac9620cfebdd8
python scripts/build-image.py --image devcontainer --version v0.6.0
python scripts/build-image.py --image devcontainer --version v0.7.0
```

### Running tests

We have some tests to ensure the docker images are working as expected, using [bats](https://github.com/bats-core/bats-core). The bats CLI tool should already be installed in the devcontainer.

You'll need to install the `bats-support` and `bats-assert` libraries. I found the easiest way to do this was to clone via git:

```bash
git clone https://github.com/bats-core/bats-support test/test_helper/bats-support
git clone https://github.com/bats-core/bats-assert test/test_helper/bats-assert
```

To run a test on a specific image, set the required variables, and run the bats command. The following is an example for the base image

```bash
export LIB_PATH=$(pwd)/tests/test_helper
export DOCKER_IMAGE=
export IDRIS_VERSION=latest
bats tests/base.bats
```

## Credit
Expand Down
6 changes: 3 additions & 3 deletions base-sha.Dockerfile
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
# separating this into a separate file so we can get better caching
# there is a lot of redundancy between this and base.Dockerfile, but I don't think it's worth it to try to abstract it out

FROM debian:bullseye as scheme-builder
FROM debian:bullseye AS scheme-builder

WORKDIR /root

Expand All @@ -22,12 +22,12 @@
# this makes it a bit easier for us to move the csv folder to other build steps, since it is necessary for scheme to run
RUN mkdir scheme-lib && cp -r /usr/lib/csv* /root/scheme-lib

FROM debian:bullseye as idris-builder
FROM debian:bullseye AS idris-builder

RUN apt-get update && \
apt-get install -y git make gcc libgmp-dev curl

ENV DEBIAN_FRONTEND noninteractive
ENV DEBIAN_FRONTEND=noninteractive
# SHA of the latest commit on the idris-lang/idris2 repo
ARG IDRIS_SHA

Expand All @@ -44,7 +44,7 @@
# add idris2 to path
ENV PATH="/root/.idris2/bin:${PATH}"
# add idris lib to LD_LIBRARY_PATH
ENV LD_LIBRARY_PATH="/root/.idris2/lib:${LD_LIBRARY_PATH}"

Check warning on line 47 in base-sha.Dockerfile

View workflow job for this annotation

GitHub Actions / Base Build & Test - latest / Build Base

Variables should be defined before their use

UndefinedVar: Usage of undefined variable '$LD_LIBRARY_PATH' More info: https://docs.docker.com/go/dockerfile/rule/undefined-var/

Check warning on line 47 in base-sha.Dockerfile

View workflow job for this annotation

GitHub Actions / Base Build & Test - latest / Test 1 Base

Variables should be defined before their use

UndefinedVar: Usage of undefined variable '$LD_LIBRARY_PATH' More info: https://docs.docker.com/go/dockerfile/rule/undefined-var/

Check warning on line 47 in base-sha.Dockerfile

View workflow job for this annotation

GitHub Actions / Base Build & Test - latest / Test 2 Base

Variables should be defined before their use

UndefinedVar: Usage of undefined variable '$LD_LIBRARY_PATH' More info: https://docs.docker.com/go/dockerfile/rule/undefined-var/

Check warning on line 47 in base-sha.Dockerfile

View workflow job for this annotation

GitHub Actions / Devcontainer Build & Test - latest / Build & Test

Variables should be defined before their use

UndefinedVar: Usage of undefined variable '$LD_LIBRARY_PATH' More info: https://docs.docker.com/go/dockerfile/rule/undefined-var/

# self-hosting (needed for Idris2 API)
# in my experience, the Idris2 API seems to still work without the self-hosting step
Expand Down
8 changes: 4 additions & 4 deletions base.Dockerfile
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
# Expects IDRIS_VERSION to NOT be `latest`
# uBut a tag of the form `v0.7.0`
# But a tag of the form `v0.7.0`

FROM debian:bullseye as scheme-builder
FROM debian:bullseye AS scheme-builder

WORKDIR /root

Expand All @@ -20,12 +20,12 @@
# this makes it a bit easier for us to move the csv folder to other build steps, since it is necessary for scheme to run
RUN mkdir scheme-lib && cp -r /usr/lib/csv* /root/scheme-lib

FROM debian:bullseye as idris-builder
FROM debian:bullseye AS idris-builder

RUN apt-get update && \
apt-get install -y git make gcc libgmp-dev curl

ENV DEBIAN_FRONTEND noninteractive
ENV DEBIAN_FRONTEND=noninteractive
ARG IDRIS_VERSION

COPY --from=scheme-builder /usr/bin/scheme /usr/bin/scheme
Expand All @@ -41,7 +41,7 @@
# add idris2 to path
ENV PATH="/root/.idris2/bin:${PATH}"
# add idris lib to LD_LIBRARY_PATH
ENV LD_LIBRARY_PATH="/root/.idris2/lib:${LD_LIBRARY_PATH}"

Check warning on line 44 in base.Dockerfile

View workflow job for this annotation

GitHub Actions / Base Build & Test - v0.5.1 / Build Base

Variables should be defined before their use

UndefinedVar: Usage of undefined variable '$LD_LIBRARY_PATH' More info: https://docs.docker.com/go/dockerfile/rule/undefined-var/

Check warning on line 44 in base.Dockerfile

View workflow job for this annotation

GitHub Actions / Base Build & Test - v0.6.0 / Build Base

Variables should be defined before their use

UndefinedVar: Usage of undefined variable '$LD_LIBRARY_PATH' More info: https://docs.docker.com/go/dockerfile/rule/undefined-var/

Check warning on line 44 in base.Dockerfile

View workflow job for this annotation

GitHub Actions / Base Build & Test - v0.7.0 / Build Base

Variables should be defined before their use

UndefinedVar: Usage of undefined variable '$LD_LIBRARY_PATH' More info: https://docs.docker.com/go/dockerfile/rule/undefined-var/

Check warning on line 44 in base.Dockerfile

View workflow job for this annotation

GitHub Actions / Base Build & Test - v0.7.0 / Test 2 Base

Variables should be defined before their use

UndefinedVar: Usage of undefined variable '$LD_LIBRARY_PATH' More info: https://docs.docker.com/go/dockerfile/rule/undefined-var/

Check warning on line 44 in base.Dockerfile

View workflow job for this annotation

GitHub Actions / Base Build & Test - v0.7.0 / Test 1 Base

Variables should be defined before their use

UndefinedVar: Usage of undefined variable '$LD_LIBRARY_PATH' More info: https://docs.docker.com/go/dockerfile/rule/undefined-var/

Check warning on line 44 in base.Dockerfile

View workflow job for this annotation

GitHub Actions / Base Build & Test - v0.6.0 / Test 1 Base

Variables should be defined before their use

UndefinedVar: Usage of undefined variable '$LD_LIBRARY_PATH' More info: https://docs.docker.com/go/dockerfile/rule/undefined-var/

Check warning on line 44 in base.Dockerfile

View workflow job for this annotation

GitHub Actions / Base Build & Test - v0.6.0 / Test 2 Base

Variables should be defined before their use

UndefinedVar: Usage of undefined variable '$LD_LIBRARY_PATH' More info: https://docs.docker.com/go/dockerfile/rule/undefined-var/

Check warning on line 44 in base.Dockerfile

View workflow job for this annotation

GitHub Actions / Base Build & Test - v0.5.1 / Test 2 Base

Variables should be defined before their use

UndefinedVar: Usage of undefined variable '$LD_LIBRARY_PATH' More info: https://docs.docker.com/go/dockerfile/rule/undefined-var/

Check warning on line 44 in base.Dockerfile

View workflow job for this annotation

GitHub Actions / Base Build & Test - v0.5.1 / Test 1 Base

Variables should be defined before their use

UndefinedVar: Usage of undefined variable '$LD_LIBRARY_PATH' More info: https://docs.docker.com/go/dockerfile/rule/undefined-var/

Check warning on line 44 in base.Dockerfile

View workflow job for this annotation

GitHub Actions / Devcontainer Build & Test - idris2-0.7.0 / Build & Test

Variables should be defined before their use

UndefinedVar: Usage of undefined variable '$LD_LIBRARY_PATH' More info: https://docs.docker.com/go/dockerfile/rule/undefined-var/

Check warning on line 44 in base.Dockerfile

View workflow job for this annotation

GitHub Actions / Devcontainer Build & Test - idris2-0.6.0 / Build & Test

Variables should be defined before their use

UndefinedVar: Usage of undefined variable '$LD_LIBRARY_PATH' More info: https://docs.docker.com/go/dockerfile/rule/undefined-var/

# self-hosting (needed for Idris2 API)
# in my experience, the Idris2 API seems to still work without the self-hosting step
Expand Down
17 changes: 0 additions & 17 deletions debian.Dockerfile

This file was deleted.

2 changes: 1 addition & 1 deletion devcontainer-sha.Dockerfile
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@
# =====
# Idris Builder
# Rebuild with correct prefix. Somehow, building from scratch with a different prefix fails
FROM $BASE_IMG as idris-builder
FROM $BASE_IMG AS idris-builder
ARG IDRIS_VERSION
ARG IDRIS_SHA

Expand All @@ -19,7 +19,7 @@

# =====
# LSP Builder
FROM debian:bullseye as lsp-builder

Check warning on line 22 in devcontainer-sha.Dockerfile

View workflow job for this annotation

GitHub Actions / Devcontainer Build & Test - latest / Build & Test

The 'as' keyword should match the case of the 'from' keyword

FromAsCasing: 'as' and 'FROM' keywords' casing do not match More info: https://docs.docker.com/go/dockerfile/rule/from-as-casing/

RUN apt-get update && \
apt-get install -y git make gcc libgmp-dev curl
Expand All @@ -31,7 +31,7 @@

# necessary environment variables for building Idris and the LSP
ENV PATH="/usr/local/lib/idris2/bin:${PATH}"
ENV LD_LIBRARY_PATH="/usr/local/lib/idris2/lib:${LD_LIBRARY_PATH}"

Check warning on line 34 in devcontainer-sha.Dockerfile

View workflow job for this annotation

GitHub Actions / Devcontainer Build & Test - latest / Build & Test

Variables should be defined before their use

UndefinedVar: Usage of undefined variable '$LD_LIBRARY_PATH' More info: https://docs.docker.com/go/dockerfile/rule/undefined-var/
ENV IDRIS2_PREFIX="/usr/local/lib/idris2"

# LSP_VERSION is in the form "idris2-0.5.1", or "latest"
Expand Down Expand Up @@ -65,7 +65,7 @@
# set required environment variables
ENV PATH="/usr/local/lib/idris2/bin:${PATH}"
# LD_LIBRARY_PATH is only required for v0.5.1 and earlier
ENV LD_LIBRARY_PATH="/usr/local/lib/idris2/lib:${LD_LIBRARY_PATH}"

Check warning on line 68 in devcontainer-sha.Dockerfile

View workflow job for this annotation

GitHub Actions / Devcontainer Build & Test - latest / Build & Test

Variables should be defined before their use

UndefinedVar: Usage of undefined variable '$LD_LIBRARY_PATH' More info: https://docs.docker.com/go/dockerfile/rule/undefined-var/
ENV SCHEME=scheme

# re-expose version information
Expand Down
2 changes: 1 addition & 1 deletion devcontainer.Dockerfile
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@
# =====
# Idris Builder
# Rebuild with correct prefix. Somehow, building from scratch with a different prefix fails
FROM $BASE_IMG as idris-builder
FROM $BASE_IMG AS idris-builder
ARG IDRIS_VERSION

WORKDIR /build
Expand All @@ -17,7 +17,7 @@

# =====
# LSP Builder
FROM debian:bullseye as lsp-builder

Check warning on line 20 in devcontainer.Dockerfile

View workflow job for this annotation

GitHub Actions / Devcontainer Build & Test - idris2-0.7.0 / Build & Test

The 'as' keyword should match the case of the 'from' keyword

FromAsCasing: 'as' and 'FROM' keywords' casing do not match More info: https://docs.docker.com/go/dockerfile/rule/from-as-casing/

Check warning on line 20 in devcontainer.Dockerfile

View workflow job for this annotation

GitHub Actions / Devcontainer Build & Test - idris2-0.6.0 / Build & Test

The 'as' keyword should match the case of the 'from' keyword

FromAsCasing: 'as' and 'FROM' keywords' casing do not match More info: https://docs.docker.com/go/dockerfile/rule/from-as-casing/

RUN apt-get update && \
apt-get install -y git make gcc libgmp-dev curl
Expand All @@ -29,7 +29,7 @@

# necessary environment variables for building Idris and the LSP
ENV PATH="/usr/local/lib/idris2/bin:${PATH}"
ENV LD_LIBRARY_PATH="/usr/local/lib/idris2/lib:${LD_LIBRARY_PATH}"

Check warning on line 32 in devcontainer.Dockerfile

View workflow job for this annotation

GitHub Actions / Devcontainer Build & Test - idris2-0.7.0 / Build & Test

Variables should be defined before their use

UndefinedVar: Usage of undefined variable '$LD_LIBRARY_PATH' More info: https://docs.docker.com/go/dockerfile/rule/undefined-var/

Check warning on line 32 in devcontainer.Dockerfile

View workflow job for this annotation

GitHub Actions / Devcontainer Build & Test - idris2-0.6.0 / Build & Test

Variables should be defined before their use

UndefinedVar: Usage of undefined variable '$LD_LIBRARY_PATH' More info: https://docs.docker.com/go/dockerfile/rule/undefined-var/
ENV IDRIS2_PREFIX="/usr/local/lib/idris2"

# LSP_VERSION is in the form "idris2-0.5.1", or "latest"
Expand Down Expand Up @@ -62,7 +62,7 @@
# set required environment variables
ENV PATH="/usr/local/lib/idris2/bin:${PATH}"
# LD_LIBRARY_PATH is only required for v0.5.1 and earlier
ENV LD_LIBRARY_PATH="/usr/local/lib/idris2/lib:${LD_LIBRARY_PATH}"

Check warning on line 65 in devcontainer.Dockerfile

View workflow job for this annotation

GitHub Actions / Devcontainer Build & Test - idris2-0.7.0 / Build & Test

Variables should be defined before their use

UndefinedVar: Usage of undefined variable '$LD_LIBRARY_PATH' More info: https://docs.docker.com/go/dockerfile/rule/undefined-var/

Check warning on line 65 in devcontainer.Dockerfile

View workflow job for this annotation

GitHub Actions / Devcontainer Build & Test - idris2-0.6.0 / Build & Test

Variables should be defined before their use

UndefinedVar: Usage of undefined variable '$LD_LIBRARY_PATH' More info: https://docs.docker.com/go/dockerfile/rule/undefined-var/
ENV SCHEME=scheme

# re-expose version information
Expand Down
Loading