Add Dockerfiles for building and running C,Coq and Haskell projects

.dockerignore

@@ -0,0 +1,7 @@
+.dockerignore
+.git
+docker-compose.yml
+Dockerfile
+Dockerfile.c
+Dockerfile.coq
+Dockerfile.haskell

.gitignore

@@ -33,5 +33,6 @@ alectryon-doc
 # Gen
 /*.rs
 /*.c
+!/Dockerfile.c
 /*.h
 /*.inc

Dockerfile.c

@@ -0,0 +1,19 @@
+FROM debian:stable-slim
+
+RUN apt-get update && apt-get install -y --no-install-recommends \
+    build-essential \
+    && rm -rf /var/lib/apt/lists/*
+
+WORKDIR /simplicity
+
+COPY C/ .
+
+RUN make -j$(nproc) X86_SHANI_CXXFLAGS="-msse4.1 -msha"
+
+RUN make install out=/usr/local
+
+RUN make check
+
+# The library is at /usr/local/lib/libElementsSimplicity.a
+# The headers are in /usr/local/include/
+CMD ["/bin/bash"]

Dockerfile.coq

@@ -0,0 +1,45 @@
+FROM coqorg/coq:8.17.1
+USER root
+RUN DEBIAN_FRONTEND=noninteractive TZ=Etc/UTC \
+    apt-get update && apt-get install -y --no-install-recommends \
+        make \
+        wget
+
+USER coq
+
+RUN opam update
+RUN opam install --yes -j$(nproc) coq-compcert=3.13.1
+
+ENV PATH="/home/coq/.opam/4.13.1+flambda/bin:${PATH}"
+
+RUN set -ex && \
+    wget https://github.com/sipa/safegcd-bounds/archive/06abb7f7aba9b00eb4ead96bdd7dbcc04ec45c4f.tar.gz -O safegcd-bounds.tar.gz && \
+    tar -xvzf safegcd-bounds.tar.gz && \
+    cd safegcd-bounds-06abb7f7aba9b00eb4ead96bdd7dbcc04ec45c4f/coq/divsteps && \
+    sed -i 's/Time Qed./Admitted./g' divsteps724.v && \
+    coq_makefile -f _CoqProject -o Makefile && \
+    make -j$(nproc) && \
+    make install
+
+    # unfortunately the following opam install for coq-vst doesn't work and so we have a long workaround
+# RUN opam install --yes -j$(nproc) coq-vst=2.14
+RUN set -ex && \
+    wget https://github.com/PrincetonUniversity/VST/archive/refs/tags/v2.14.tar.gz -O vst.tar.gz && \
+    tar -xvzf vst.tar.gz && \
+    cd VST-2.14 && \
+    COMPCERT_DIR=$(coqc -where)/user-contrib/compcert && \
+    make -j$(nproc) default_target sha COMPCERT=inst_dir COMPCERT_INST_DIR="$COMPCERT_DIR" && \
+    gcc -c sha/sha.c -o sha/sha.o && \
+    make install && \
+    install -d $(coqc -where)/user-contrib/sha && \
+    install -m 0644 -t $(coqc -where)/user-contrib/sha sha/*.v sha/*.vo
+
+WORKDIR /home/coq/simplicity
+COPY --chown=coq:coq . .
+WORKDIR /home/coq/simplicity/Coq
+RUN coq_makefile -f _CoqProject -o CoqMakefile -docroot /tmp
+RUN make -f CoqMakefile clean && make -f CoqMakefile -j$(nproc)
+RUN make -f CoqMakefile install
+
+RUN echo "Require Import Simplicity.Semantics." > /home/coq/coq-init.v
+CMD ["coqtop", "-q", "-init-file", "/home/coq/coq-init.v"]

Dockerfile.haskell

@@ -0,0 +1,45 @@
+FROM haskell:9.8
+
+RUN apt-get update && apt-get install -y --no-install-recommends \
+    valgrind \
+    && apt-get clean && rm -rf /var/lib/apt/lists/*
+
+WORKDIR /simplicity
+
+COPY Simplicity.cabal ./
+COPY Haskell/ Haskell/
+COPY Haskell-Examples/ Haskell-Examples/
+COPY Haskell-Generate/ Haskell-Generate/
+COPY C/ C/
+
+RUN cabal update
+RUN cabal configure --jobs=$(nproc)
+RUN cabal build --jobs=$(nproc)
+
+RUN echo ":m + Simplicity.Bitcoin.Term" > /simplicity/.ghci && \
+    echo ":m + Simplicity.Bitcoin.Semantics" >> /simplicity/.ghci && \
+    echo ":m + Simplicity.Bitcoin.Primitive" >> /simplicity/.ghci && \
+    echo ":m + Simplicity.Bitcoin.DataTypes" >> /simplicity/.ghci && \
+    echo ":m + Simplicity.Elements.Term" >> /simplicity/.ghci && \
+    echo ":m + Simplicity.Elements.Semantics" >> /simplicity/.ghci && \
+    echo ":m + Simplicity.Elements.Primitive" >> /simplicity/.ghci && \
+    echo ":m + Simplicity.Elements.DataTypes" >> /simplicity/.ghci && \
+    echo ":m + Simplicity.Programs.Generic" >> /simplicity/.ghci && \
+    echo ":m + Simplicity.Programs.Word" >> /simplicity/.ghci && \
+    echo ":m + Simplicity.Programs.Bit" >> /simplicity/.ghci && \
+    echo ":m + Simplicity.Programs.Arith" >> /simplicity/.ghci && \
+    echo ":m + Simplicity.Programs.Sha256" >> /simplicity/.ghci && \
+    echo ":m + Simplicity.Programs.LibSecp256k1" >> /simplicity/.ghci && \
+    echo ":m + Simplicity.Ty.Word" >> /simplicity/.ghci && \
+    echo ":m + Simplicity.Ty.Bit" >> /simplicity/.ghci && \
+    echo ":m + Simplicity.Weight" >> /simplicity/.ghci && \
+    echo ":m + Simplicity.MerkleRoot" >> /simplicity/.ghci && \
+    echo ":m + Simplicity.Tags" >> /simplicity/.ghci && \
+    echo ":set prompt \"Simplicity> \"" >> /simplicity/.ghci && \
+    echo ":set +t" >> /simplicity/.ghci && \
+    echo "import qualified Simplicity.Ty.Word as Ty" >> /simplicity/.ghci
+
+#CMD ["/bin/bash"]
+CMD ["cabal", "repl", "Simplicity", "--enable-multi-repl"]
+
+

README.md

@@ -37,6 +37,12 @@ nix-shell --arg coq false --arg haskell false
 
 Use arguments to enable / disable the other projects.
 
+#### Docker
+```
+docker build -f Dockerfile.c -t simplicity-c  .
+docker run -it  simplicity-c
+```
+
 #### Manual
 
 Change into the C directory of this repository.
@@ -79,6 +85,13 @@ nix-shell --arg c false --arg coq false
 
 Use arguments to enable / disable the other projects.
 
+#### Docker
+
+```
+docker build -f Dockerfile.haskell -t simplicity-haskell  .
+docker run -it  simplicity-haskell
+```
+
 #### Manual
 
 Install the [Glasgow Haskell Compiler](https://www.haskell.org/ghc/) and [Cabal](https://www.haskell.org/cabal/).
@@ -125,6 +138,13 @@ nix-shell --arg c false --arg haskell false
 
 Use arguments to enable / disable the other projects.
 
+#### Docker
+
+```
+docker build -f Dockerfile.coq -t simplicity-coq  .
+docker run -it  simplicity-coq
+```
+
 #### Manual
 
 Install the [opam package manager](https://opam.ocaml.org/).