src/Pure/Admin/build_docker.scala
author wenzelm
Sat, 14 Jan 2017 20:33:55 +0100
changeset 64890 d8ccbd5305bf
child 64893 07a93485d22b
permissions -rw-r--r--
build docker image from Isabelle application bundle for Linux;
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
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    14
  def build_docker(progress: Progress,
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    15
    app_archive: Path,
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    16
    logic: String = default_logic,
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    17
    output: Option[Path] = None,
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    18
    tag: String = "",
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    19
    verbose: Boolean = false)
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    20
  {
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    21
    val distname =
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    22
    {
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    23
      val Name = "^(Isabelle[^/]*)/?.*$".r
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    24
      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
    25
        case Name(name) :: _ => name
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    26
        case _ => error("Cannot determine Isabelle distribution name from " + app_archive)
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    27
      }
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
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    30
    val dockerfile =
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    31
      """## Dockerfile for """ + distname + """
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    32
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    33
FROM ubuntu
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    34
SHELL ["/bin/bash", "-c"]
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
# packages
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    37
RUN apt-get -y update && \
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    38
  apt-get install -y less lib32stdc++6 libwww-perl rlwrap unzip && \
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    39
  apt-get clean
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
# user
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    42
RUN useradd -m isabelle && (echo isabelle:isabelle | chpasswd)
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    43
USER isabelle
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    44
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    45
# Isabelle
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    46
WORKDIR /home/isabelle
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    47
COPY Isabelle.tar.gz .
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    48
RUN tar xzf Isabelle.tar.gz && \
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    49
  mv """ + distname + """ Isabelle && \
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    50
  rm -rf Isabelle.tar.gz Isabelle/contrib/jdk/x86-linux && \
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    51
  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
    52
  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
    53
  Isabelle/bin/isabelle build -s -b """ + logic + """
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    54
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    55
ENTRYPOINT ["Isabelle/bin/isabelle"]
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    56
"""
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    57
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    58
    output.foreach(File.write(_, dockerfile))
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    59
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    60
    Isabelle_System.with_tmp_dir("docker")(tmp_dir =>
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    61
      {
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    62
        File.write(tmp_dir + Path.explode("Dockerfile"), dockerfile)
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    63
        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
    64
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    65
        val quiet_option = if (verbose) "" else " -q"
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    66
        val tag_option = if (tag == "") "" else " -t " + Bash.string(tag)
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    67
        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
    68
          echo = true).check
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
  }
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    71
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
  /* Isabelle tool wrapper */
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    74
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    75
  val isabelle_tool =
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    76
    Isabelle_Tool("build_docker", "build Isabelle docker image", args =>
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
      var logic = default_logic
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    79
      var output: Option[Path] = None
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    80
      var verbose = false
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    81
      var tag = ""
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 getopts =
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    84
        Getopts("""
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    85
Usage: isabelle build_docker [OPTIONS] APP_ARCHIVE
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    86
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    87
  Options are:
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    88
    -l NAME      default logic (default ISABELLE_LOGIC=""" + quote(default_logic) + """)
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    89
    -o FILE      output generated Dockerfile
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    90
    -t TAG       docker build tag
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    91
    -v           verbose
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    92
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    93
  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
    94
  Isabelle application archive for Linux.
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
  The remaining DOCKER_ARGS are passed directly to "docker build".
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    97
""",
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    98
          "l:" -> (arg => logic = arg),
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
    99
          "o:" -> (arg => output = Some(Path.explode(arg))),
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
   100
          "t:" -> (arg => tag = arg),
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
   101
          "v" -> (_ => verbose = true))
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
   102
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
   103
      val more_args = getopts(args)
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
   104
      val app_archive =
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
   105
        more_args match {
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
   106
          case List(arg) => Path.explode(arg)
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
   107
          case _ => getopts.usage()
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
   108
        }
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
   109
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
   110
      build_docker(new Console_Progress(), app_archive, logic, output, tag, verbose)
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
   111
    }, admin = true)
d8ccbd5305bf build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff changeset
   112
}