diff --git a/.dockerignore b/.dockerignore new file mode 100644 index 00000000..ffe629c4 --- /dev/null +++ b/.dockerignore @@ -0,0 +1,7 @@ +.dockerignore +.git +docker-compose.yml +Dockerfile +Dockerfile.c +Dockerfile.coq +Dockerfile.haskell diff --git a/.gitignore b/.gitignore index e448abb6..da239319 100644 --- a/.gitignore +++ b/.gitignore @@ -33,5 +33,6 @@ alectryon-doc # Gen /*.rs /*.c +!/Dockerfile.c /*.h /*.inc diff --git a/Dockerfile.c b/Dockerfile.c new file mode 100644 index 00000000..3c4bd4b5 --- /dev/null +++ b/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"] \ No newline at end of file diff --git a/Dockerfile.coq b/Dockerfile.coq new file mode 100644 index 00000000..02aa824c --- /dev/null +++ b/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"] \ No newline at end of file diff --git a/Dockerfile.haskell b/Dockerfile.haskell new file mode 100644 index 00000000..e655f736 --- /dev/null +++ b/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"] + + diff --git a/README.md b/README.md index b87e7a4f..934dddac 100644 --- a/README.md +++ b/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/).