build docker image from Isabelle application bundle for Linux;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Admin/build_docker.scala	Sat Jan 14 20:33:55 2017 +0100
@@ -0,0 +1,112 @@
+/*  Title:      Pure/Admin/build_docker.scala
+    Author:     Makarius
+
+Build docker image from Isabelle application bundle for Linux.
+*/
+
+package isabelle
+
+
+object Build_Docker
+{
+  private lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC")
+
+  def build_docker(progress: Progress,
+    app_archive: Path,
+    logic: String = default_logic,
+    output: Option[Path] = None,
+    tag: String = "",
+    verbose: Boolean = false)
+  {
+    val distname =
+    {
+      val Name = "^(Isabelle[^/]*)/?.*$".r
+      Isabelle_System.bash("tar tzf " + File.bash_path(app_archive)).check.out_lines match {
+        case Name(name) :: _ => name
+        case _ => error("Cannot determine Isabelle distribution name from " + app_archive)
+      }
+    }
+
+    val dockerfile =
+      """## Dockerfile for """ + distname + """
+
+FROM ubuntu
+SHELL ["/bin/bash", "-c"]
+
+# packages
+RUN apt-get -y update && \
+  apt-get install -y less lib32stdc++6 libwww-perl rlwrap unzip && \
+  apt-get clean
+
+# user
+RUN useradd -m isabelle && (echo isabelle:isabelle | chpasswd)
+USER isabelle
+
+# Isabelle
+WORKDIR /home/isabelle
+COPY Isabelle.tar.gz .
+RUN tar xzf Isabelle.tar.gz && \
+  mv """ + distname + """ Isabelle && \
+  rm -rf Isabelle.tar.gz Isabelle/contrib/jdk/x86-linux && \
+  perl -pi -e 's,ISABELLE_HOME_USER=.*,ISABELLE_HOME_USER="\$USER_HOME/.isabelle",g;' Isabelle/etc/settings && \
+  perl -pi -e 's,ISABELLE_LOGIC=.*,ISABELLE_LOGIC=""" + logic + """,g;' Isabelle/etc/settings && \
+  Isabelle/bin/isabelle build -s -b """ + logic + """
+
+ENTRYPOINT ["Isabelle/bin/isabelle"]
+"""
+
+    output.foreach(File.write(_, dockerfile))
+
+    Isabelle_System.with_tmp_dir("docker")(tmp_dir =>
+      {
+        File.write(tmp_dir + Path.explode("Dockerfile"), dockerfile)
+        File.copy(app_archive, tmp_dir + Path.explode("Isabelle.tar.gz"))
+
+        val quiet_option = if (verbose) "" else " -q"
+        val tag_option = if (tag == "") "" else " -t " + Bash.string(tag)
+        progress.bash("docker build" + quiet_option + tag_option + " " + File.bash_path(tmp_dir),
+          echo = true).check
+      })
+  }
+
+
+  /* Isabelle tool wrapper */
+
+  val isabelle_tool =
+    Isabelle_Tool("build_docker", "build Isabelle docker image", args =>
+    {
+      var logic = default_logic
+      var output: Option[Path] = None
+      var verbose = false
+      var tag = ""
+
+      val getopts =
+        Getopts("""
+Usage: isabelle build_docker [OPTIONS] APP_ARCHIVE
+
+  Options are:
+    -l NAME      default logic (default ISABELLE_LOGIC=""" + quote(default_logic) + """)
+    -o FILE      output generated Dockerfile
+    -t TAG       docker build tag
+    -v           verbose
+
+  Build Isabelle docker image with default logic image, using a standard
+  Isabelle application archive for Linux.
+
+  The remaining DOCKER_ARGS are passed directly to "docker build".
+""",
+          "l:" -> (arg => logic = arg),
+          "o:" -> (arg => output = Some(Path.explode(arg))),
+          "t:" -> (arg => tag = arg),
+          "v" -> (_ => verbose = true))
+
+      val more_args = getopts(args)
+      val app_archive =
+        more_args match {
+          case List(arg) => Path.explode(arg)
+          case _ => getopts.usage()
+        }
+
+      build_docker(new Console_Progress(), app_archive, logic, output, tag, verbose)
+    }, admin = true)
+}

--- a/src/Pure/System/isabelle_tool.scala	Sat Jan 14 20:22:15 2017 +0100
+++ b/src/Pure/System/isabelle_tool.scala	Sat Jan 14 20:33:55 2017 +0100
@@ -101,6 +101,7 @@
     List(
       Build.isabelle_tool,
       Build_Doc.isabelle_tool,
+      Build_Docker.isabelle_tool,
       Build_PolyML.isabelle_tool,
       Build_Stats.isabelle_tool,
       Check_Sources.isabelle_tool,

--- a/src/Pure/build-jars	Sat Jan 14 20:22:15 2017 +0100
+++ b/src/Pure/build-jars	Sat Jan 14 20:33:55 2017 +0100
@@ -10,6 +10,7 @@
 
 declare -a SOURCES=(
   Admin/build_doc.scala
+  Admin/build_docker.scala
   Admin/build_history.scala
   Admin/build_log.scala
   Admin/build_polyml.scala