From b64cf8a7beffdb5cb17b368467e958a9cb40055d Mon Sep 17 00:00:00 2001
From: "Achim D. Brucker" <adbrucker@0x5f.org>
Date: Thu, 3 Jan 2019 09:41:12 +0000
Subject: [PATCH] Initial commit isabelle.

---
 README.md           |  3 +++
 build.sh            | 49 ++++++++++++++++++++++++++++++++++++++
 isabelle/Dockerfile | 58 +++++++++++++++++++++++++++++++++++++++++++++
 3 files changed, 110 insertions(+)
 create mode 100644 isabelle/Dockerfile

diff --git a/README.md b/README.md
index e494c4d..7671b73 100644
--- a/README.md
+++ b/README.md
@@ -10,6 +10,9 @@ and projects based on [Isabelle](https://isabelle.in.tum.de).
   eagerly optimised for size, as it goal is to include all tools that are required for 
   running Isabelle and tools based on Isabelle (e.g., HOL-TestGen).
 
+* [isabelle](isabelle/Dockerfile) provides a parametrized Dockerfile to generate docker 
+  images for various Isabelle versions.
+
 ## Authors
 
 Main author: [Achim D. Brucker](http://www.brucker.ch/)
diff --git a/build.sh b/build.sh
index 115fd0a..eeb80a2 100755
--- a/build.sh
+++ b/build.sh
@@ -1,4 +1,53 @@
 #!/bin/bash
+# Copyright (c) 2019 Achim D. Brucker
+#
+# All rights reserved.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#
+# * Redistributions of source code must retain the above copyright notice, this
+#
+# * Redistributions in binary form must reproduce the above copyright notice,
+#   this list of conditions and the following disclaimer in the documentation
+#   and/or other materials provided with the distribution.
+#
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+# AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+# IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+# DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
+# FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+# DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+# SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+# CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+# OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+# OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+#
+# SPDX-License-Identifier: BSD-2-Clause
+
 set -e 
 
+VERSION=${1:-2018}
+SESSIONS=${2:-"HOL"}
+
+# Generate base image
 docker build -t logicalhacking:debian4isabelle debian4isabelle
+
+# Generate Isabelle image
+ISA_URL="http://isabelle.in.tum.de/website-Isabelle"$VERSION"/dist/Isabelle"$VERSION"_app.tar.gz"
+AFP_URL="https://sourceforge.net/projects/afp/files/afp-Isabelle$VERSION/"
+AFP_TAR=`w3m -dump  $AFP_URL | grep ^afp- | head -1 | awk -e '{print $1}'`
+
+for url in $ISA_URL $AFP_URL/$AFP_TAR; do
+  if curl --output /dev/null --silent --head --fail "$url"; then
+    echo "URL exists: $url"
+  else
+    echo "URL does not exist: $url"
+    exit 1
+  fi
+done
+
+docker build -t logicalhacking:isabelle2018 isabelle \
+             --build-arg sessions=$SESSIONS \
+             --build-arg isabelle=$ISA_URL \
+             --build-arg afp=$AFP_URL/$AFP_TAR
diff --git a/isabelle/Dockerfile b/isabelle/Dockerfile
new file mode 100644
index 0000000..867d914
--- /dev/null
+++ b/isabelle/Dockerfile
@@ -0,0 +1,58 @@
+# Copyright (c) 2019 Achim D. Brucker
+#
+# All rights reserved.
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions are met:
+#
+# * Redistributions of source code must retain the above copyright notice, this
+#
+# * Redistributions in binary form must reproduce the above copyright notice,
+#   this list of conditions and the following disclaimer in the documentation
+#   and/or other materials provided with the distribution.
+#
+# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+# AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+# IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+# DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
+# FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+# DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+# SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+# CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+# OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+# OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+#
+# SPDX-License-Identifier: BSD-2-Clause
+
+FROM logicalhacking:debian4isabelle
+
+ARG isabelle
+ARG afp
+ARG sessions
+
+LABEL isabelle.url="$isabelle"
+LABEL isabelle.afp.url="$afp"
+LABEL isabelle.sessions="$sessions"
+
+SHELL ["/bin/bash", "-c"]
+
+# Create default user (isabelle)
+RUN useradd -m isabelle && (echo isabelle:isabelle | chpasswd)
+USER isabelle
+
+# Install Isabelle and corresponding AFP
+WORKDIR /home/isabelle
+RUN curl -L -o "Isabelle.tar.gz" "$isabelle" && \
+  curl -L -o "afp.tar.gz" "$afp" && \
+  tar xzf "Isabelle.tar.gz" && \
+  tar xzf "afp.tar.gz" && \
+  rm *.tar.gz && \
+  mv Isabelle* Isabelle && \
+  mv afp* afp && \
+  mkdir .isabelle && \
+  echo `pwd`/afp/thys > .isabelle/ROOTS && \
+  perl -pi -e 's,ISABELLE_HOME_USER=.*,ISABELLE_HOME_USER="\$USER_HOME/.isabelle",g;' Isabelle/etc/settings && \
+  Isabelle/bin/isabelle build -s -b $sessions
+
+ENTRYPOINT ["Isabelle/bin/isabelle"]
+