src/Pure/Admin/build_docker.scala
author wenzelm
Sat Jan 14 22:28:51 2017 +0100 (2017-01-14)
changeset 64894 6c6bb62702d4
parent 64893 07a93485d22b
child 64895 ad3b66e7a028
permissions -rw-r--r--
clarified packages;
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@64890
    12
  private lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC")
wenzelm@64890
    13
wenzelm@64894
    14
  private val standard_packages =
wenzelm@64894
    15
    List("less", "lib32stdc++6", "libwww-perl", "rlwrap", "unzip")
wenzelm@64894
    16
wenzelm@64894
    17
  private val package_collections =
wenzelm@64894
    18
    Map("X11" -> List("libx11-6", "libxext6", "libxrender1", "libxtst6", "libxi6"))
wenzelm@64894
    19
wenzelm@64890
    20
  def build_docker(progress: Progress,
wenzelm@64890
    21
    app_archive: Path,
wenzelm@64890
    22
    logic: String = default_logic,
wenzelm@64890
    23
    output: Option[Path] = None,
wenzelm@64893
    24
    packages: List[String] = Nil,
wenzelm@64890
    25
    tag: String = "",
wenzelm@64890
    26
    verbose: Boolean = false)
wenzelm@64890
    27
  {
wenzelm@64890
    28
    val distname =
wenzelm@64890
    29
    {
wenzelm@64890
    30
      val Name = "^(Isabelle[^/]*)/?.*$".r
wenzelm@64890
    31
      Isabelle_System.bash("tar tzf " + File.bash_path(app_archive)).check.out_lines match {
wenzelm@64890
    32
        case Name(name) :: _ => name
wenzelm@64890
    33
        case _ => error("Cannot determine Isabelle distribution name from " + app_archive)
wenzelm@64890
    34
      }
wenzelm@64890
    35
    }
wenzelm@64890
    36
wenzelm@64890
    37
    val dockerfile =
wenzelm@64890
    38
      """## Dockerfile for """ + distname + """
wenzelm@64890
    39
wenzelm@64890
    40
FROM ubuntu
wenzelm@64890
    41
SHELL ["/bin/bash", "-c"]
wenzelm@64890
    42
wenzelm@64890
    43
# packages
wenzelm@64890
    44
RUN apt-get -y update && \
wenzelm@64894
    45
  apt-get install -y  """ + (standard_packages ::: packages).map(Bash.string(_)).mkString(" ") + """ && \
wenzelm@64890
    46
  apt-get clean
wenzelm@64890
    47
wenzelm@64890
    48
# user
wenzelm@64890
    49
RUN useradd -m isabelle && (echo isabelle:isabelle | chpasswd)
wenzelm@64890
    50
USER isabelle
wenzelm@64890
    51
wenzelm@64890
    52
# Isabelle
wenzelm@64890
    53
WORKDIR /home/isabelle
wenzelm@64890
    54
COPY Isabelle.tar.gz .
wenzelm@64890
    55
RUN tar xzf Isabelle.tar.gz && \
wenzelm@64890
    56
  mv """ + distname + """ Isabelle && \
wenzelm@64890
    57
  rm -rf Isabelle.tar.gz Isabelle/contrib/jdk/x86-linux && \
wenzelm@64890
    58
  perl -pi -e 's,ISABELLE_HOME_USER=.*,ISABELLE_HOME_USER="\$USER_HOME/.isabelle",g;' Isabelle/etc/settings && \
wenzelm@64890
    59
  perl -pi -e 's,ISABELLE_LOGIC=.*,ISABELLE_LOGIC=""" + logic + """,g;' Isabelle/etc/settings && \
wenzelm@64890
    60
  Isabelle/bin/isabelle build -s -b """ + logic + """
wenzelm@64890
    61
wenzelm@64890
    62
ENTRYPOINT ["Isabelle/bin/isabelle"]
wenzelm@64890
    63
"""
wenzelm@64890
    64
wenzelm@64890
    65
    output.foreach(File.write(_, dockerfile))
wenzelm@64890
    66
wenzelm@64890
    67
    Isabelle_System.with_tmp_dir("docker")(tmp_dir =>
wenzelm@64890
    68
      {
wenzelm@64890
    69
        File.write(tmp_dir + Path.explode("Dockerfile"), dockerfile)
wenzelm@64890
    70
        File.copy(app_archive, tmp_dir + Path.explode("Isabelle.tar.gz"))
wenzelm@64890
    71
wenzelm@64890
    72
        val quiet_option = if (verbose) "" else " -q"
wenzelm@64890
    73
        val tag_option = if (tag == "") "" else " -t " + Bash.string(tag)
wenzelm@64890
    74
        progress.bash("docker build" + quiet_option + tag_option + " " + File.bash_path(tmp_dir),
wenzelm@64890
    75
          echo = true).check
wenzelm@64890
    76
      })
wenzelm@64890
    77
  }
wenzelm@64890
    78
wenzelm@64890
    79
wenzelm@64890
    80
  /* Isabelle tool wrapper */
wenzelm@64890
    81
wenzelm@64890
    82
  val isabelle_tool =
wenzelm@64890
    83
    Isabelle_Tool("build_docker", "build Isabelle docker image", args =>
wenzelm@64890
    84
    {
wenzelm@64890
    85
      var logic = default_logic
wenzelm@64890
    86
      var output: Option[Path] = None
wenzelm@64893
    87
      var packages: List[String] = Nil
wenzelm@64890
    88
      var verbose = false
wenzelm@64890
    89
      var tag = ""
wenzelm@64890
    90
wenzelm@64890
    91
      val getopts =
wenzelm@64890
    92
        Getopts("""
wenzelm@64890
    93
Usage: isabelle build_docker [OPTIONS] APP_ARCHIVE
wenzelm@64890
    94
wenzelm@64890
    95
  Options are:
wenzelm@64894
    96
    -P NAME      additional Ubuntu package collection (""" +
wenzelm@64894
    97
          package_collections.keySet.toList.sorted.mkString(", ") + """)
wenzelm@64890
    98
    -l NAME      default logic (default ISABELLE_LOGIC=""" + quote(default_logic) + """)
wenzelm@64890
    99
    -o FILE      output generated Dockerfile
wenzelm@64894
   100
    -p NAME      additional Ubuntu package
wenzelm@64890
   101
    -t TAG       docker build tag
wenzelm@64890
   102
    -v           verbose
wenzelm@64890
   103
wenzelm@64890
   104
  Build Isabelle docker image with default logic image, using a standard
wenzelm@64890
   105
  Isabelle application archive for Linux.
wenzelm@64890
   106
wenzelm@64890
   107
  The remaining DOCKER_ARGS are passed directly to "docker build".
wenzelm@64890
   108
""",
wenzelm@64894
   109
          "P:" -> (arg =>
wenzelm@64894
   110
            package_collections.get(arg) match {
wenzelm@64894
   111
              case Some(ps) => packages :::= ps
wenzelm@64894
   112
              case None => error("Unknown package collection " + quote(arg))
wenzelm@64894
   113
            }),
wenzelm@64890
   114
          "l:" -> (arg => logic = arg),
wenzelm@64890
   115
          "o:" -> (arg => output = Some(Path.explode(arg))),
wenzelm@64893
   116
          "p:" -> (arg => packages ::= arg),
wenzelm@64890
   117
          "t:" -> (arg => tag = arg),
wenzelm@64890
   118
          "v" -> (_ => verbose = true))
wenzelm@64890
   119
wenzelm@64890
   120
      val more_args = getopts(args)
wenzelm@64890
   121
      val app_archive =
wenzelm@64890
   122
        more_args match {
wenzelm@64890
   123
          case List(arg) => Path.explode(arg)
wenzelm@64890
   124
          case _ => getopts.usage()
wenzelm@64890
   125
        }
wenzelm@64890
   126
wenzelm@64893
   127
      build_docker(new Console_Progress(), app_archive, logic = logic, output = output,
wenzelm@64893
   128
        packages = packages, tag = tag, verbose = verbose)
wenzelm@64890
   129
    }, admin = true)
wenzelm@64890
   130
}