From 586c7e324e707fc99bfc3ef1e411689448ff5dd8 Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Fri, 10 May 2024 13:37:39 -0400
Subject: [PATCH] Add Dockerfile

This adds a basic `Dockerfile` that installs `copilot` and `copilot-verifier`,
along with bundling its dependencies (e.g., `z3`).
---
 .dockerignore | 25 +++++++++++++++++++++++++
 Dockerfile    | 29 +++++++++++++++++++++++++++++
 README.md     | 11 +++++++++++
 3 files changed, 65 insertions(+)
 create mode 100644 .dockerignore
 create mode 100644 Dockerfile

diff --git a/.dockerignore b/.dockerignore
new file mode 100644
index 0000000..7d1d60a
--- /dev/null
+++ b/.dockerignore
@@ -0,0 +1,25 @@
+/build/
+.cabal-sandbox
+.stack-work
+**/cabal.config
+cabal.sandbox.config
+dist
+TAGS
+unitTest.tix
+hpc_report
+stack.yaml
+**/dist-newstyle
+.*.swp
+cabal.project.local
+*.tix
+.ghc.environment.*
+*~
+_darcs
+.boring
+
+# Where copilot-verifier puts its autogenerated code
+results/
+
+Dockerfile
+.git
+.gitignore
diff --git a/Dockerfile b/Dockerfile
new file mode 100644
index 0000000..e46cdbe
--- /dev/null
+++ b/Dockerfile
@@ -0,0 +1,29 @@
+FROM ubuntu:focal
+
+ENV DEBIAN_FRONTEND=noninteractive
+RUN apt-get update && \
+    apt-get install --yes curl gcc g++ git libgmp3-dev libtinfo-dev libz-dev make wget z3
+
+ENV GHCUP_VER=0.1.22.0
+RUN mkdir -p /root/.ghcup/bin
+RUN wget https://downloads.haskell.org/~ghcup/$GHCUP_VER/x86_64-linux-ghcup-$GHCUP_VER -O /root/.ghcup/bin/ghcup && \
+    chmod a+x /root/.ghcup/bin/ghcup
+
+ENV PATH=/root/bsc/bin:/root/.cabal/bin:/root/.ghcup/bin:$PATH
+
+ENV GHC_VER=9.2.8
+ENV CABAL_VER=3.8.1.0
+RUN ghcup install ghc $GHC_VER && \
+    ghcup set ghc $GHC_VER && \
+    ghcup install cabal $CABAL_VER && \
+    ghcup set cabal $CABAL_VER && \
+    cabal update
+
+COPY . /copilot-verifier
+WORKDIR /copilot-verifier
+
+RUN cabal configure --enable-tests && \
+    cabal build lib:copilot-verifier --write-ghc-environment-files=always && \
+    cabal test copilot-verifier
+
+ENTRYPOINT ["/usr/bin/bash"]
diff --git a/README.md b/README.md
index 4a90648..22c142a 100644
--- a/README.md
+++ b/README.md
@@ -49,6 +49,17 @@ This will clone the repository, build the verifier, and run the associated test
 suite. If you have performed all of the steps above correctly, the test suite
 should pass.
 
+We also provide a [Dockerfile](Dockerfile) which automates the process of
+installing Copilot and the verifier. The Dockerfile can be built and run using
+the following commands:
+
+```
+$ docker build -t <tag> .
+$ docker run -it <tag>
+```
+
+Where `<tag>` is a unique name for the Docker image.
+
 ## Using the Copilot Verifier
 
 The main interface to the verifier is the `Copilot.Verifier.verify`