Idris 2 DevContainer

0_README.md

How to use Idris 2 in devcontainer

Step 1: build executable and libraries

Use the Dockerfile below to build the Idris 2 executable and standard library:

docker build --tag=idris2 .

Step 2: describe devcontainer

In folder for your Idris 2 playground create a subdirectory .devcontainer. Copy devcontainer.json there, and create a new Dockerfile with the following content:

FROM idris2:latest

Step 3: open VSCode in devcontainer mode and use it!

Make sure to have Remote development extension pack installed. Click on the menu in the lower left corner, and select Reopen in container.

NB: Idris 2 executable is available as idris2 and as a symlink idris, so the extension should just work out of the box.

devcontainer.json

{
    "name": "Idris 2",
    "dockerFile": "Dockerfile",
    "settings": {
        "terminal.integrated.shell.linux": "/bin/bash"
    },
    "runArgs": [
        "--network=host"
    ],
    "extensions": [
        "zjhmale.idris"
    ]
}

Dockerfile

# Stage 0: get Idris 2 source and build it using Racket
FROM ubuntu:latest AS build

ENV IDRIS2_CG racket
ENV DEBIAN_FRONTEND noninteractive

WORKDIR /root

RUN apt-get update && \
    apt-get install -y racket git make gcc libc-dev
RUN git clone https://github.com/idris-lang/Idris2.git && \
    cd ./Idris2 && \
    make bootstrap-racket && \
    make install

# Stage 1: copy Idris 2 executable and libraries to the minimal Ubuntu image (with Racket)
FROM ubuntu:latest
WORKDIR /root
COPY --from=build /root/.idris2 /root/.idris2
# This ensures the extension works without additional configuration:
RUN ln -s /root/.idris2/bin/idris2 /bin/idris

ENV PATH="/root/.idris2/bin:${PATH}"
ENV LD_LIBRARY_PATH="/root/.idris2/lib:${LD_LIBRARY_PATH}"

RUN apt-get update && \
    apt-get install -y racket