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