1/* Title: Pure/Tools/build_docker.scala 2 Author: Makarius 3 4Build docker image from Isabelle application bundle for Linux. 5*/ 6 7package isabelle 8 9 10object Build_Docker 11{ 12 private val default_base = "ubuntu" 13 private lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC") 14 15 private val Isabelle_Name = """^.*?(Isabelle[^/\\:]+)_(?:app|linux)\.tar\.gz$""".r 16 17 val packages: List[String] = 18 List("curl", "less", "lib32stdc++6", "libgomp1", "libwww-perl", "rlwrap", "unzip") 19 20 val package_collections: Map[String, List[String]] = 21 Map("X11" -> List("libx11-6", "libxext6", "libxrender1", "libxtst6", "libxi6"), 22 "latex" -> List("texlive-fonts-extra", "texlive-latex-extra", "texlive-math-extra")) 23 24 def build_docker(progress: Progress, 25 app_archive: String, 26 base: String = default_base, 27 logic: String = default_logic, 28 no_build: Boolean = false, 29 entrypoint: Boolean = false, 30 output: Option[Path] = None, 31 more_packages: List[String] = Nil, 32 tag: String = "", 33 verbose: Boolean = false) 34 { 35 val isabelle_name = 36 app_archive match { 37 case Isabelle_Name(name) => name 38 case _ => error("Cannot determine Isabelle distribution name from " + app_archive) 39 } 40 val is_remote = Url.is_wellformed(app_archive) 41 42 val dockerfile = 43 """## Dockerfile for """ + isabelle_name + """ 44 45FROM """ + base + """ 46SHELL ["/bin/bash", "-c"] 47 48# packages 49RUN apt-get -y update && \ 50 apt-get install -y """ + Bash.strings(packages ::: more_packages) + """ && \ 51 apt-get clean 52 53# user 54RUN useradd -m isabelle && (echo isabelle:isabelle | chpasswd) 55USER isabelle 56 57# Isabelle 58WORKDIR /home/isabelle 59""" + 60 (if (is_remote) 61 "RUN curl --fail --silent " + Bash.string(app_archive) + " > Isabelle.tar.gz" 62 else "COPY Isabelle.tar.gz .") + 63""" 64RUN tar xzf Isabelle.tar.gz && \ 65 mv """ + isabelle_name + """ Isabelle && \ 66 perl -pi -e 's,ISABELLE_HOME_USER=.*,ISABELLE_HOME_USER="\$USER_HOME/.isabelle",g;' Isabelle/etc/settings && \ 67 perl -pi -e 's,ISABELLE_LOGIC=.*,ISABELLE_LOGIC=""" + logic + """,g;' Isabelle/etc/settings && \ 68 Isabelle/bin/isabelle build -s -b """ + logic + 69 (if (entrypoint) """ 70 71ENTRYPOINT ["Isabelle/bin/isabelle"] 72""" 73 else "") 74 75 output.foreach(File.write(_, dockerfile)) 76 77 if (!no_build) { 78 Isabelle_System.with_tmp_dir("docker")(tmp_dir => 79 { 80 File.write(tmp_dir + Path.explode("Dockerfile"), dockerfile) 81 82 if (is_remote) { 83 if (!Url.is_readable(app_archive)) 84 error("Cannot access remote archive " + app_archive) 85 } 86 else File.copy(Path.explode(app_archive), tmp_dir + Path.explode("Isabelle.tar.gz")) 87 88 val quiet_option = if (verbose) "" else " -q" 89 val tag_option = if (tag == "") "" else " -t " + Bash.string(tag) 90 progress.bash("docker build" + quiet_option + tag_option + " " + File.bash_path(tmp_dir), 91 echo = true).check 92 }) 93 } 94 } 95 96 97 /* Isabelle tool wrapper */ 98 99 val isabelle_tool = 100 Isabelle_Tool("build_docker", "build Isabelle docker image", args => 101 { 102 var base = default_base 103 var entrypoint = false 104 var logic = default_logic 105 var no_build = false 106 var output: Option[Path] = None 107 var more_packages: List[String] = Nil 108 var verbose = false 109 var tag = "" 110 111 val getopts = 112 Getopts(""" 113Usage: isabelle build_docker [OPTIONS] APP_ARCHIVE 114 115 Options are: 116 -B NAME base image (default """ + quote(default_base) + """) 117 -E set bin/isabelle as entrypoint 118 -P NAME additional Ubuntu package collection (""" + 119 package_collections.keySet.toList.sorted.map(quote(_)).mkString(", ") + """) 120 -l NAME default logic (default ISABELLE_LOGIC=""" + quote(default_logic) + """) 121 -n no docker build 122 -o FILE output generated Dockerfile 123 -p NAME additional Ubuntu package 124 -t TAG docker build tag 125 -v verbose 126 127 Build Isabelle docker image with default logic image, using a standard 128 Isabelle application archive for Linux (local file or remote URL). 129 130 Examples: 131 132 isabelle build_docker -E -t test/isabelle:Isabelle2018 Isabelle2018_app.tar.gz 133 134 isabelle build_docker -E -n -o Dockerfile http://isabelle.in.tum.de/dist/Isabelle2018_app.tar.gz 135 136""", 137 "B:" -> (arg => base = arg), 138 "E" -> (_ => entrypoint = true), 139 "P:" -> (arg => 140 package_collections.get(arg) match { 141 case Some(ps) => more_packages :::= ps 142 case None => error("Unknown package collection " + quote(arg)) 143 }), 144 "l:" -> (arg => logic = arg), 145 "n" -> (_ => no_build = true), 146 "o:" -> (arg => output = Some(Path.explode(arg))), 147 "p:" -> (arg => more_packages ::= arg), 148 "t:" -> (arg => tag = arg), 149 "v" -> (_ => verbose = true)) 150 151 val more_args = getopts(args) 152 val app_archive = 153 more_args match { 154 case List(arg) => arg 155 case _ => getopts.usage() 156 } 157 158 build_docker(new Console_Progress(), app_archive, base = base, logic = logic, 159 no_build = no_build, entrypoint = entrypoint, output = output, 160 more_packages = more_packages, tag = tag, verbose = verbose) 161 }) 162} 163