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