Add Dockerfile

This adds a basic `Dockerfile` that installs `copilot` and `copilot-verifier`,
along with bundling its dependencies (e.g., `z3`).

.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

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"]

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`