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