From fc1f8a2c0ae9881c38042c1b60728895b50148b4 Mon Sep 17 00:00:00 2001 From: Simon Tennant Date: Thu, 21 Aug 2025 15:59:13 +0200 Subject: [PATCH 1/2] Add Dockerfiles for building and running C,Coq and Haskell projects --- .dockerignore | 7 +++++++ .gitignore | 1 + Dockerfile.c | 19 +++++++++++++++++++ Dockerfile.coq | 45 +++++++++++++++++++++++++++++++++++++++++++++ Dockerfile.haskell | 17 +++++++++++++++++ README.md | 20 ++++++++++++++++++++ 6 files changed, 109 insertions(+) create mode 100644 .dockerignore create mode 100644 Dockerfile.c create mode 100644 Dockerfile.coq create mode 100644 Dockerfile.haskell diff --git a/.dockerignore b/.dockerignore new file mode 100644 index 000000000..ffe629c4f --- /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 e448abb61..da239319d 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 000000000..3c4bd4b50 --- /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 000000000..02aa824cd --- /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 000000000..35ccd528a --- /dev/null +++ b/Dockerfile.haskell @@ -0,0 +1,17 @@ +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 && cabal build --jobs=$(nproc) + +CMD ["cabal", "repl", "Simplicity"] \ No newline at end of file diff --git a/README.md b/README.md index b87e7a4f8..934dddac0 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/). From 6892b08658a9ddfca7a47f11372ce0e00c7d9a1b Mon Sep 17 00:00:00 2001 From: Simon Tennant Date: Sun, 24 Aug 2025 15:03:43 +0200 Subject: [PATCH 2/2] Ensure Simplicity modules are loaded at the GHCi prompt. --- Dockerfile.haskell | 32 ++++++++++++++++++++++++++++++-- 1 file changed, 30 insertions(+), 2 deletions(-) diff --git a/Dockerfile.haskell b/Dockerfile.haskell index 35ccd528a..e655f7365 100644 --- a/Dockerfile.haskell +++ b/Dockerfile.haskell @@ -12,6 +12,34 @@ COPY Haskell-Examples/ Haskell-Examples/ COPY Haskell-Generate/ Haskell-Generate/ COPY C/ C/ -RUN cabal update && cabal build --jobs=$(nproc) +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"] + -CMD ["cabal", "repl", "Simplicity"] \ No newline at end of file