add dockerfiles

Author: yongweiy

README.md

@@ -10,4 +10,18 @@ This repo includes artifacts for "Live Pattern Matching with Typed Holes". Speci
 
 - Assuming `opam` is installed, run `$ ./build` under `incon-sat` will build the project and check the tests.
 
+### Docker
+  Alternatively, you may use [Docker](https://docs.docker.com/get-docker/). Note: building dockers may take a while.
+
+- Build and run Agda mechanization
+  ```
+  $ docker build -t pattern-agda agda-mechanization
+  $ docker run pattern-agda # will check proof
+  ```
+- Build and run Exhaustiveness and Redundancy Checker
+  ```
+  $ docker build -t pattern-incon agda-mechanization
+  $ docker run -it pattern-incon # will invoke OCaml toplevel
+  ``` 
+
 Please see the README in each folder for detailed instructions.

agda-mechanization/Dockerfile

@@ -0,0 +1,6 @@
+from haskell:8.4.3
+run cabal update
+run cabal install alex happy
+run cabal install Agda-2.6.2
+copy . .
+cmd ["agda" , "-v", "2" , "all.agda"]

incon-sat/.dockerignore

@@ -0,0 +1,2 @@
+_build/
+.merlin

incon-sat/Dockerfile

@@ -0,0 +1,9 @@
+from ocaml/opam:debian-10-ocaml-4.12
+run sudo apt install -y python3 libgmp-dev
+run opam install --yes dune utop ocamlformat z3 ppx_inline_test
+copy . .
+env PATH=/home/opam/.opam/4.12/bin:$PATH
+run dune build @runtest
+cmd dune utop src
+
+

incon-sat/build

@@ -1,3 +1,4 @@
+#!/bin/sh
 OCAML_VERSION=4.12.0
 if ! command -v opam &> /dev/null
 then