# HG changeset patch # User wenzelm # Date 1507467126 -7200 # Node ID c0e68e6a1bebd482ae73da9e5f353cecbea2252e # Parent feb36b73a7f0d68c833f7c67da5fdda31f4cf071 build_docker is regular tool (non-admin); diff -r feb36b73a7f0 -r c0e68e6a1beb src/Pure/Admin/build_docker.scala --- a/src/Pure/Admin/build_docker.scala Sun Oct 08 14:48:47 2017 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,163 +0,0 @@ -/* Title: Pure/Admin/build_docker.scala - Author: Makarius - -Build docker image from Isabelle application bundle for Linux. -*/ - -package isabelle - - -object Build_Docker -{ - private val default_base = "ubuntu" - private lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC") - - private val Isabelle_Name = """^.*?(Isabelle[^/\\:]+)_(?:app|linux)\.tar\.gz$""".r - - val packages: List[String] = - List("curl", "less", "lib32stdc++6", "libgomp1", "libwww-perl", "rlwrap", "unzip") - - val package_collections: Map[String, List[String]] = - Map("X11" -> List("libx11-6", "libxext6", "libxrender1", "libxtst6", "libxi6"), - "latex" -> List("texlive-fonts-extra", "texlive-latex-extra", "texlive-math-extra")) - - def build_docker(progress: Progress, - app_archive: String, - base: String = default_base, - logic: String = default_logic, - no_build: Boolean = false, - entrypoint: Boolean = false, - output: Option[Path] = None, - more_packages: List[String] = Nil, - tag: String = "", - verbose: Boolean = false) - { - val isabelle_name = - app_archive match { - case Isabelle_Name(name) => name - case _ => error("Cannot determine Isabelle distribution name from " + app_archive) - } - val is_remote = Url.is_wellformed(app_archive) - - val dockerfile = - """## Dockerfile for """ + isabelle_name + """ - -FROM """ + base + """ -SHELL ["/bin/bash", "-c"] - -# packages -RUN apt-get -y update && \ - apt-get install -y """ + Bash.strings(packages ::: more_packages) + """ && \ - apt-get clean - -# user -RUN useradd -m isabelle && (echo isabelle:isabelle | chpasswd) -USER isabelle - -# Isabelle -WORKDIR /home/isabelle -""" + - (if (is_remote) - "RUN curl --fail --silent " + Bash.string(app_archive) + " > Isabelle.tar.gz" - else "COPY Isabelle.tar.gz .") + -""" -RUN tar xzf Isabelle.tar.gz && \ - mv """ + isabelle_name + """ 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 + - (if (entrypoint) """ - -ENTRYPOINT ["Isabelle/bin/isabelle"] -""" - else "") - - output.foreach(File.write(_, dockerfile)) - - if (!no_build) { - Isabelle_System.with_tmp_dir("docker")(tmp_dir => - { - File.write(tmp_dir + Path.explode("Dockerfile"), dockerfile) - - if (is_remote) { - if (!Url.is_readable(app_archive)) - error("Cannot access remote archive " + app_archive) - } - else File.copy(Path.explode(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 base = default_base - var entrypoint = false - var logic = default_logic - var no_build = false - var output: Option[Path] = None - var more_packages: List[String] = Nil - var verbose = false - var tag = "" - - val getopts = - Getopts(""" -Usage: isabelle build_docker [OPTIONS] APP_ARCHIVE - - Options are: - -B NAME base image (default """ + quote(default_base) + """) - -E set bin/isabelle as entrypoint - -P NAME additional Ubuntu package collection (""" + - package_collections.keySet.toList.sorted.map(quote(_)).mkString(", ") + """) - -l NAME default logic (default ISABELLE_LOGIC=""" + quote(default_logic) + """) - -n no docker build - -o FILE output generated Dockerfile - -p NAME additional Ubuntu package - -t TAG docker build tag - -v verbose - - Build Isabelle docker image with default logic image, using a standard - Isabelle application archive for Linux (local file or remote URL). - - Examples: - - isabelle build_docker -E -t test/isabelle:Isabelle2017 Isabelle2017_app.tar.gz - - isabelle build_docker -E -n -o Dockerfile http://isabelle.in.tum.de/dist/Isabelle2017_app.tar.gz - -""", - "B:" -> (arg => base = arg), - "E" -> (_ => entrypoint = true), - "P:" -> (arg => - package_collections.get(arg) match { - case Some(ps) => more_packages :::= ps - case None => error("Unknown package collection " + quote(arg)) - }), - "l:" -> (arg => logic = arg), - "n" -> (_ => no_build = true), - "o:" -> (arg => output = Some(Path.explode(arg))), - "p:" -> (arg => more_packages ::= arg), - "t:" -> (arg => tag = arg), - "v" -> (_ => verbose = true)) - - val more_args = getopts(args) - val app_archive = - more_args match { - case List(arg) => arg - case _ => getopts.usage() - } - - build_docker(new Console_Progress(), app_archive, base = base, logic = logic, - no_build = no_build, entrypoint = entrypoint, output = output, - more_packages = more_packages, tag = tag, verbose = verbose) - }, admin = true) -} diff -r feb36b73a7f0 -r c0e68e6a1beb src/Pure/Tools/build_docker.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Tools/build_docker.scala Sun Oct 08 14:52:06 2017 +0200 @@ -0,0 +1,163 @@ +/* Title: Pure/Tools/build_docker.scala + Author: Makarius + +Build docker image from Isabelle application bundle for Linux. +*/ + +package isabelle + + +object Build_Docker +{ + private val default_base = "ubuntu" + private lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC") + + private val Isabelle_Name = """^.*?(Isabelle[^/\\:]+)_(?:app|linux)\.tar\.gz$""".r + + val packages: List[String] = + List("curl", "less", "lib32stdc++6", "libgomp1", "libwww-perl", "rlwrap", "unzip") + + val package_collections: Map[String, List[String]] = + Map("X11" -> List("libx11-6", "libxext6", "libxrender1", "libxtst6", "libxi6"), + "latex" -> List("texlive-fonts-extra", "texlive-latex-extra", "texlive-math-extra")) + + def build_docker(progress: Progress, + app_archive: String, + base: String = default_base, + logic: String = default_logic, + no_build: Boolean = false, + entrypoint: Boolean = false, + output: Option[Path] = None, + more_packages: List[String] = Nil, + tag: String = "", + verbose: Boolean = false) + { + val isabelle_name = + app_archive match { + case Isabelle_Name(name) => name + case _ => error("Cannot determine Isabelle distribution name from " + app_archive) + } + val is_remote = Url.is_wellformed(app_archive) + + val dockerfile = + """## Dockerfile for """ + isabelle_name + """ + +FROM """ + base + """ +SHELL ["/bin/bash", "-c"] + +# packages +RUN apt-get -y update && \ + apt-get install -y """ + Bash.strings(packages ::: more_packages) + """ && \ + apt-get clean + +# user +RUN useradd -m isabelle && (echo isabelle:isabelle | chpasswd) +USER isabelle + +# Isabelle +WORKDIR /home/isabelle +""" + + (if (is_remote) + "RUN curl --fail --silent " + Bash.string(app_archive) + " > Isabelle.tar.gz" + else "COPY Isabelle.tar.gz .") + +""" +RUN tar xzf Isabelle.tar.gz && \ + mv """ + isabelle_name + """ 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 + + (if (entrypoint) """ + +ENTRYPOINT ["Isabelle/bin/isabelle"] +""" + else "") + + output.foreach(File.write(_, dockerfile)) + + if (!no_build) { + Isabelle_System.with_tmp_dir("docker")(tmp_dir => + { + File.write(tmp_dir + Path.explode("Dockerfile"), dockerfile) + + if (is_remote) { + if (!Url.is_readable(app_archive)) + error("Cannot access remote archive " + app_archive) + } + else File.copy(Path.explode(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 base = default_base + var entrypoint = false + var logic = default_logic + var no_build = false + var output: Option[Path] = None + var more_packages: List[String] = Nil + var verbose = false + var tag = "" + + val getopts = + Getopts(""" +Usage: isabelle build_docker [OPTIONS] APP_ARCHIVE + + Options are: + -B NAME base image (default """ + quote(default_base) + """) + -E set bin/isabelle as entrypoint + -P NAME additional Ubuntu package collection (""" + + package_collections.keySet.toList.sorted.map(quote(_)).mkString(", ") + """) + -l NAME default logic (default ISABELLE_LOGIC=""" + quote(default_logic) + """) + -n no docker build + -o FILE output generated Dockerfile + -p NAME additional Ubuntu package + -t TAG docker build tag + -v verbose + + Build Isabelle docker image with default logic image, using a standard + Isabelle application archive for Linux (local file or remote URL). + + Examples: + + isabelle build_docker -E -t test/isabelle:Isabelle2017 Isabelle2017_app.tar.gz + + isabelle build_docker -E -n -o Dockerfile http://isabelle.in.tum.de/dist/Isabelle2017_app.tar.gz + +""", + "B:" -> (arg => base = arg), + "E" -> (_ => entrypoint = true), + "P:" -> (arg => + package_collections.get(arg) match { + case Some(ps) => more_packages :::= ps + case None => error("Unknown package collection " + quote(arg)) + }), + "l:" -> (arg => logic = arg), + "n" -> (_ => no_build = true), + "o:" -> (arg => output = Some(Path.explode(arg))), + "p:" -> (arg => more_packages ::= arg), + "t:" -> (arg => tag = arg), + "v" -> (_ => verbose = true)) + + val more_args = getopts(args) + val app_archive = + more_args match { + case List(arg) => arg + case _ => getopts.usage() + } + + build_docker(new Console_Progress(), app_archive, base = base, logic = logic, + no_build = no_build, entrypoint = entrypoint, output = output, + more_packages = more_packages, tag = tag, verbose = verbose) + }) +} diff -r feb36b73a7f0 -r c0e68e6a1beb src/Pure/build-jars --- a/src/Pure/build-jars Sun Oct 08 14:48:47 2017 +0200 +++ b/src/Pure/build-jars Sun Oct 08 14:52:06 2017 +0200 @@ -11,7 +11,6 @@ declare -a SOURCES=( Admin/build_cygwin.scala Admin/build_doc.scala - Admin/build_docker.scala Admin/build_history.scala Admin/build_jdk.scala Admin/build_log.scala @@ -133,6 +132,7 @@ Thy/thy_syntax.scala Tools/bibtex.scala Tools/build.scala + Tools/build_docker.scala Tools/check_keywords.scala Tools/debugger.scala Tools/doc.scala