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