From 18895bdb552952b956115ee9673f2ef5d373ff9e Mon Sep 17 00:00:00 2001
From: "Achim D. Brucker" <adbrucker@0x5f.org>
Date: Thu, 27 Apr 2023 13:36:47 +0100
Subject: [PATCH] Initial upload: Dockerfile for Isabelle nightly builds.

---
 build.sh                    | 10 +++++--
 isabelle_nightly/Dockerfile | 55 +++++++++++++++++++++++++++++++++++++
 2 files changed, 62 insertions(+), 3 deletions(-)
 create mode 100644 isabelle_nightly/Dockerfile

diff --git a/build.sh b/build.sh
index e914128..4689cab 100755
--- a/build.sh
+++ b/build.sh
@@ -34,9 +34,13 @@ export VERSION SESSIONS CONTAINER DOCKERUID LATEST
 # Generate base image
 $CONTAINER build -t logicalhacking/debian4isabelle debian4isabelle
 
-# Generate Isabelle image(s)
-export IMAGE_NAME=logicalhacking/isabelle$VERSION
-( cd isabelle && source hooks/build)
+if [[ "$VERSION" == "nightly" ]]; then 
+  $CONTAINER build --build-arg uid="$DOCKERUID" --build-arg sessions="$SESSIONS" -t logicalhacking/isabelle_nightly isabelle_nightly
+else 
+  # Generate Isabelle image(s)
+  export IMAGE_NAME=logicalhacking/isabelle$VERSION
+  ( cd isabelle && source hooks/build)
+fi
 
 # Generate Isabelle/DOF image
 #ISADOF_VERSION=1.0.0
diff --git a/isabelle_nightly/Dockerfile b/isabelle_nightly/Dockerfile
new file mode 100644
index 0000000..bca174d
--- /dev/null
+++ b/isabelle_nightly/Dockerfile
@@ -0,0 +1,55 @@
+# 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
+ARG uid
+
+LABEL isabelle.url="https://isabelle.sketis.net/repos/isabelle/"
+LABEL isabelle.afp.url="https://foss.heptapod.net/isa-afp/afp-devel/"
+LABEL isabelle.sessions="$sessions"
+
+
+# Create default user (isabelle)
+RUN useradd -o -u $uid -m isabelle && (echo isabelle:isabelle | chpasswd)
+USER isabelle
+
+# Install Isabelle and corresponding AFP
+WORKDIR /home/isabelle
+RUN hg clone https://isabelle.sketis.net/repos/isabelle/ && \
+    hg clone https://foss.heptapod.net/isa-afp/afp-devel/ && \
+    isabelle/Admin/init && \
+    /home/isabelle/isabelle/bin/isabelle components -u afp-devel/thys && \
+    isabelle/Admin/init && \
+    perl -pi -e 's,ISABELLE_HOME_USER=.*,ISABELLE_HOME_USER="/home/isabelle/.isabelle",g;' isabelle/etc/settings && \
+    isabelle/bin/isabelle build -j 1 -b $sessions 
+
+ENV PATH="/home/isabelle/isabelle/bin:${PATH}"
+ENV HOME="/home/isabelle"
+USER root