add a Dockerfile

.dockerignore

@@ -0,0 +1,2 @@
+_build/
+dockerfile/

README.md

@@ -4,6 +4,8 @@
 A nuHFL(Z) (aka higher-order CHC) solver based on refinement types.
 
 ## Install and Build
+The easiest way to test ReTHFL is to use Docker (see the [README](docker/README.md) for Docker).
+Here we explain how to install ReTHFL without relying on Docker.
 
 ### Creating an opam switch
 We use [opam](https://opam.ocaml.org/) for install and build.

docker/Dockerfile

@@ -0,0 +1,62 @@
+FROM ubuntu:24.04 AS base
+
+ARG TARGETARCH
+ENV Z3_VERSION=4.13.4
+ENV ELDARICA_VERSION=2.1
+
+RUN apt update && apt install -y curl wget unzip build-essential git
+# opam
+WORKDIR /tmp
+RUN curl -fsSL https://opam.ocaml.org/install.sh > opam.sh && \
+    yes "" | bash opam.sh && \
+    opam init --disable-sandboxing
+
+# rustup (for hoice)
+WORKDIR /tmp
+RUN curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs > rustup.sh && \
+    chmod +x rustup.sh && \
+    ./rustup.sh -y
+ENV PATH="/root/.cargo/bin:${PATH}"
+
+# Z3 for (hoice)
+RUN echo ${TARGETARCH} && \
+    case ${TARGETARCH} in \
+        amd64) \
+            BASE="z3-${Z3_VERSION}-x64-glibc-2.35"; \
+            URL="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/${BASE}.zip";; \
+        arm64) \
+            # The glibc version is different from that of x64
+            BASE="z3-${Z3_VERSION}-arm64-glibc-2.34"; \
+            URL="https://github.com/Z3Prover/z3/releases/download/z3-${Z3_VERSION}/${BASE}.zip";; \
+        *) \
+            echo "Unsupported architecture: ${TARGETARCH}"; \
+            exit 1;; \
+     esac && \
+    wget ${URL} && \
+    unzip ${BASE}.zip && \
+    cp ${BASE}/bin/z3 /usr/local/bin
+
+# Hoice
+WORKDIR /tmp
+RUN . $HOME/.cargo/env && \
+    cargo install --git https://github.com/hopv/hoice
+
+# Eldarica
+WORKDIR /tmp
+RUN wget https://github.com/uuverifiers/eldarica/releases/download/v${ELDARICA_VERSION}/eldarica-bin-${ELDARICA_VERSION}.zip && \
+    unzip eldarica-bin-2.1.zip && \
+    mv eldarica /usr/local/bin && \
+    ln -s /usr/local/bin/eldarica/eld /usr/local/bin/eld && \
+    apt install -y default-jre
+
+FROM base AS builder
+COPY ./ /root/rethfl
+WORKDIR /root/rethfl
+RUN opam switch create . --deps-only --locked --yes && \
+    eval $(opam env) && \
+    dune build @install && \
+    dune install
+
+ENV OPAMSWITCH="/root/rethfl"
+ENTRYPOINT ["opam", "exec", "--"]
+CMD ["rethfl"]

docker/README.md

@@ -0,0 +1,25 @@
+# Docker
+
+## Building an Image
+Run
+
+``` sh
+docker buildx build . -t rethfl -f docker/Dockerfile
+```
+at the root directory of this repository.
+Note that we use `buildx` for multiplatform support.
+
+## Running Rethfl
+Just prepend `docker run <image name>` in front of `rethfl`, its options and the input file.
+For example,
+``` sh
+docker run rethfl:latest rethfl input/ok/valid/sum.in --show-refinement
+```
+
+## Developing inside a continer
+
+``` sh
+docker run -it [--rm] rethfl:latest /bin/bash
+```
+will let you get into the container.
+You will find this repository at `/root/rethfl`.