From e66dc483691320ebb5238ee77fa9c0720922a1b6 Mon Sep 17 00:00:00 2001
From: Ken Sakayori <kensakayori+research@gmail.com>
Date: Mon, 23 Dec 2024 14:31:28 +0900
Subject: [PATCH] add a a Dockerfile

---
 .dockerignore     |  2 ++
 README.md         |  2 ++
 docker/Dockerfile | 62 +++++++++++++++++++++++++++++++++++++++++++++++
 3 files changed, 66 insertions(+)
 create mode 100644 .dockerignore
 create mode 100644 docker/Dockerfile

diff --git a/.dockerignore b/.dockerignore
new file mode 100644
index 0000000..4463c8f
--- /dev/null
+++ b/.dockerignore
@@ -0,0 +1,2 @@
+_build/
+dockerfile/
diff --git a/README.md b/README.md
index c8d26ad..0fabc11 100644
--- a/README.md
+++ b/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.
diff --git a/docker/Dockerfile b/docker/Dockerfile
new file mode 100644
index 0000000..1dd2228
--- /dev/null
+++ b/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"]