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