From d8750f8049cc722b884a7ffaea2e91fae13b6bb7 Mon Sep 17 00:00:00 2001
From: Gustavo Varo <gustavo.varo@microsoft.com>
Date: Fri, 14 Sep 2018 12:14:49 -0400
Subject: [PATCH] Adding windows docker files for FStar docs and Fstar binaries

---
 .docker/build/build_helper.sh                |  5 ++-
 .docker/build/windows-nt/binaries/Dockerfile | 35 ++++++++++++++++++++
 .docker/build/windows-nt/docs/Dockerfile     | 35 ++++++++++++++++++++
 3 files changed, 74 insertions(+), 1 deletion(-)
 create mode 100755 .docker/build/windows-nt/binaries/Dockerfile
 create mode 100755 .docker/build/windows-nt/docs/Dockerfile

diff --git a/.docker/build/build_helper.sh b/.docker/build/build_helper.sh
index 38989effeab..43edce919c7 100644
--- a/.docker/build/build_helper.sh
+++ b/.docker/build/build_helper.sh
@@ -30,4 +30,7 @@ ssh-add -D
 FStar/.scripts/query-stats.py -f $out_file -F html -o log_no_replay.html -n all '--filter=fstar_usedhints=+' '--filter=fstar_tag=-' -g
 
 # Worst offenders (longest times)
-FStar/.scripts/query-stats.py -f $out_file -F html -o log_worst.html -c -g -n 10
\ No newline at end of file
+FStar/.scripts/query-stats.py -f $out_file -F html -o log_worst.html -c -g -n 10
+
+# Generate the container timestamp for debug purposes
+echo $(date -u "+%Y-%m-%d %H:%M:%S") >> "timestamp.txt"
\ No newline at end of file
diff --git a/.docker/build/windows-nt/binaries/Dockerfile b/.docker/build/windows-nt/binaries/Dockerfile
new file mode 100755
index 00000000000..88e370af08b
--- /dev/null
+++ b/.docker/build/windows-nt/binaries/Dockerfile
@@ -0,0 +1,35 @@
+# Fstar binaries container used to build fstar binaries.
+# Binaries should always use the latest fstar image available.
+FROM fstar-windows-nt:latest
+
+ARG BUILDLOGFILE
+ARG MAXTHREADS
+ARG TARGET
+ARG BRANCHNAME
+ARG FSTARSOURCEVERSION
+
+# Add ssh key
+# We cannot copy directly to the .ssh folder, instead we copy to a temp folder
+WORKDIR "everestsshkey"
+COPY id_rsa .
+WORKDIR ".."
+
+# Now, using bash we copy the file, set the correct security and remove the previous folder
+RUN Invoke-BashCmd '"cd .ssh && cp ../everestsshkey/id_rsa . && chmod 600 id_rsa && rm -rf ../everestsshkey"'
+
+# Remove extra files.
+RUN Invoke-BashCmd rm -f $Env:BUILDLOGFILE
+RUN Invoke-BashCmd rm -f log_no_replay.html
+RUN Invoke-BashCmd rm -f log_worst.html
+RUN Invoke-BashCmd rm -f orange_status.txt
+RUN Invoke-BashCmd rm -f result.txt
+RUN Invoke-BashCmd rm -f status.txt
+RUN Invoke-BashCmd rm -f commitinfofilename.json
+
+COPY build.sh build.sh
+COPY build_helper.sh build_helper.sh
+
+RUN Invoke-BashCmd ./build_helper.sh $Env:TARGET $Env:BUILDLOGFILE $Env:MAXTHREADS $Env:BRANCHNAME $Env:FSTARSOURCEVERSION '||' true
+
+# Remove ssh key.
+RUN Invoke-BashCmd rm .ssh/id_rsa
\ No newline at end of file
diff --git a/.docker/build/windows-nt/docs/Dockerfile b/.docker/build/windows-nt/docs/Dockerfile
new file mode 100755
index 00000000000..201d085b089
--- /dev/null
+++ b/.docker/build/windows-nt/docs/Dockerfile
@@ -0,0 +1,35 @@
+# Fstar docs container used to build fstar documentation.
+# Docs should always use the latest fstar image available.
+FROM fstar-windows-nt:latest
+
+ARG BUILDLOGFILE
+ARG MAXTHREADS
+ARG TARGET
+ARG BRANCHNAME
+ARG FSTARSOURCEVERSION
+
+# Add ssh key
+# We cannot copy directly to the .ssh folder, instead we copy to a temp folder
+WORKDIR "everestsshkey"
+COPY id_rsa .
+WORKDIR ".."
+
+# Now, using bash we copy the file, set the correct security and remove the previous folder
+RUN Invoke-BashCmd '"cd .ssh && cp ../everestsshkey/id_rsa . && chmod 600 id_rsa && rm -rf ../everestsshkey"'
+
+# Remove extra files.
+RUN Invoke-BashCmd rm -f $Env:BUILDLOGFILE
+RUN Invoke-BashCmd rm -f log_no_replay.html
+RUN Invoke-BashCmd rm -f log_worst.html
+RUN Invoke-BashCmd rm -f orange_status.txt
+RUN Invoke-BashCmd rm -f result.txt
+RUN Invoke-BashCmd rm -f status.txt
+RUN Invoke-BashCmd rm -f commitinfofilename.json
+
+COPY build.sh build.sh
+COPY build_helper.sh build_helper.sh
+
+RUN Invoke-BashCmd ./build_helper.sh $Env:TARGET $Env:BUILDLOGFILE $Env:MAXTHREADS $Env:BRANCHNAME $Env:FSTARSOURCEVERSION '||' true
+
+# Remove ssh key.
+RUN Invoke-BashCmd rm .ssh/id_rsa
\ No newline at end of file