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