src/Pure/Admin/build_docker.scala
changeset 66790 c0e68e6a1beb
parent 66789 feb36b73a7f0
child 66791 e51f789f7705
     1.1 --- a/src/Pure/Admin/build_docker.scala	Sun Oct 08 14:48:47 2017 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,163 +0,0 @@
     1.4 -/*  Title:      Pure/Admin/build_docker.scala
     1.5 -    Author:     Makarius
     1.6 -
     1.7 -Build docker image from Isabelle application bundle for Linux.
     1.8 -*/
     1.9 -
    1.10 -package isabelle
    1.11 -
    1.12 -
    1.13 -object Build_Docker
    1.14 -{
    1.15 -  private val default_base = "ubuntu"
    1.16 -  private lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC")
    1.17 -
    1.18 -  private val Isabelle_Name = """^.*?(Isabelle[^/\\:]+)_(?:app|linux)\.tar\.gz$""".r
    1.19 -
    1.20 -  val packages: List[String] =
    1.21 -    List("curl", "less", "lib32stdc++6", "libgomp1", "libwww-perl", "rlwrap", "unzip")
    1.22 -
    1.23 -  val package_collections: Map[String, List[String]] =
    1.24 -    Map("X11" -> List("libx11-6", "libxext6", "libxrender1", "libxtst6", "libxi6"),
    1.25 -      "latex" -> List("texlive-fonts-extra", "texlive-latex-extra", "texlive-math-extra"))
    1.26 -
    1.27 -  def build_docker(progress: Progress,
    1.28 -    app_archive: String,
    1.29 -    base: String = default_base,
    1.30 -    logic: String = default_logic,
    1.31 -    no_build: Boolean = false,
    1.32 -    entrypoint: Boolean = false,
    1.33 -    output: Option[Path] = None,
    1.34 -    more_packages: List[String] = Nil,
    1.35 -    tag: String = "",
    1.36 -    verbose: Boolean = false)
    1.37 -  {
    1.38 -    val isabelle_name =
    1.39 -      app_archive match {
    1.40 -        case Isabelle_Name(name) => name
    1.41 -        case _ => error("Cannot determine Isabelle distribution name from " + app_archive)
    1.42 -      }
    1.43 -    val is_remote = Url.is_wellformed(app_archive)
    1.44 -
    1.45 -    val dockerfile =
    1.46 -      """## Dockerfile for """ + isabelle_name + """
    1.47 -
    1.48 -FROM """ + base + """
    1.49 -SHELL ["/bin/bash", "-c"]
    1.50 -
    1.51 -# packages
    1.52 -RUN apt-get -y update && \
    1.53 -  apt-get install -y """ + Bash.strings(packages ::: more_packages) + """ && \
    1.54 -  apt-get clean
    1.55 -
    1.56 -# user
    1.57 -RUN useradd -m isabelle && (echo isabelle:isabelle | chpasswd)
    1.58 -USER isabelle
    1.59 -
    1.60 -# Isabelle
    1.61 -WORKDIR /home/isabelle
    1.62 -""" +
    1.63 - (if (is_remote)
    1.64 -   "RUN curl --fail --silent " + Bash.string(app_archive) + " > Isabelle.tar.gz"
    1.65 -  else "COPY Isabelle.tar.gz .") +
    1.66 -"""
    1.67 -RUN tar xzf Isabelle.tar.gz && \
    1.68 -  mv """ + isabelle_name + """ Isabelle && \
    1.69 -  rm -rf Isabelle.tar.gz Isabelle/contrib/jdk/x86-linux && \
    1.70 -  perl -pi -e 's,ISABELLE_HOME_USER=.*,ISABELLE_HOME_USER="\$USER_HOME/.isabelle",g;' Isabelle/etc/settings && \
    1.71 -  perl -pi -e 's,ISABELLE_LOGIC=.*,ISABELLE_LOGIC=""" + logic + """,g;' Isabelle/etc/settings && \
    1.72 -  Isabelle/bin/isabelle build -s -b """ + logic +
    1.73 - (if (entrypoint) """
    1.74 -
    1.75 -ENTRYPOINT ["Isabelle/bin/isabelle"]
    1.76 -"""
    1.77 -  else "")
    1.78 -
    1.79 -    output.foreach(File.write(_, dockerfile))
    1.80 -
    1.81 -    if (!no_build) {
    1.82 -      Isabelle_System.with_tmp_dir("docker")(tmp_dir =>
    1.83 -        {
    1.84 -          File.write(tmp_dir + Path.explode("Dockerfile"), dockerfile)
    1.85 -
    1.86 -          if (is_remote) {
    1.87 -            if (!Url.is_readable(app_archive))
    1.88 -              error("Cannot access remote archive " + app_archive)
    1.89 -          }
    1.90 -          else File.copy(Path.explode(app_archive), tmp_dir + Path.explode("Isabelle.tar.gz"))
    1.91 -
    1.92 -          val quiet_option = if (verbose) "" else " -q"
    1.93 -          val tag_option = if (tag == "") "" else " -t " + Bash.string(tag)
    1.94 -          progress.bash("docker build" + quiet_option + tag_option + " " + File.bash_path(tmp_dir),
    1.95 -            echo = true).check
    1.96 -        })
    1.97 -    }
    1.98 -  }
    1.99 -
   1.100 -
   1.101 -  /* Isabelle tool wrapper */
   1.102 -
   1.103 -  val isabelle_tool =
   1.104 -    Isabelle_Tool("build_docker", "build Isabelle docker image", args =>
   1.105 -    {
   1.106 -      var base = default_base
   1.107 -      var entrypoint = false
   1.108 -      var logic = default_logic
   1.109 -      var no_build = false
   1.110 -      var output: Option[Path] = None
   1.111 -      var more_packages: List[String] = Nil
   1.112 -      var verbose = false
   1.113 -      var tag = ""
   1.114 -
   1.115 -      val getopts =
   1.116 -        Getopts("""
   1.117 -Usage: isabelle build_docker [OPTIONS] APP_ARCHIVE
   1.118 -
   1.119 -  Options are:
   1.120 -    -B NAME      base image (default """ + quote(default_base) + """)
   1.121 -    -E           set bin/isabelle as entrypoint
   1.122 -    -P NAME      additional Ubuntu package collection (""" +
   1.123 -          package_collections.keySet.toList.sorted.map(quote(_)).mkString(", ") + """)
   1.124 -    -l NAME      default logic (default ISABELLE_LOGIC=""" + quote(default_logic) + """)
   1.125 -    -n           no docker build
   1.126 -    -o FILE      output generated Dockerfile
   1.127 -    -p NAME      additional Ubuntu package
   1.128 -    -t TAG       docker build tag
   1.129 -    -v           verbose
   1.130 -
   1.131 -  Build Isabelle docker image with default logic image, using a standard
   1.132 -  Isabelle application archive for Linux (local file or remote URL).
   1.133 -
   1.134 -  Examples:
   1.135 -
   1.136 -    isabelle build_docker -E -t test/isabelle:Isabelle2017 Isabelle2017_app.tar.gz
   1.137 -
   1.138 -    isabelle build_docker -E -n -o Dockerfile http://isabelle.in.tum.de/dist/Isabelle2017_app.tar.gz
   1.139 -
   1.140 -""",
   1.141 -          "B:" -> (arg => base = arg),
   1.142 -          "E" -> (_ => entrypoint = true),
   1.143 -          "P:" -> (arg =>
   1.144 -            package_collections.get(arg) match {
   1.145 -              case Some(ps) => more_packages :::= ps
   1.146 -              case None => error("Unknown package collection " + quote(arg))
   1.147 -            }),
   1.148 -          "l:" -> (arg => logic = arg),
   1.149 -          "n" -> (_ => no_build = true),
   1.150 -          "o:" -> (arg => output = Some(Path.explode(arg))),
   1.151 -          "p:" -> (arg => more_packages ::= arg),
   1.152 -          "t:" -> (arg => tag = arg),
   1.153 -          "v" -> (_ => verbose = true))
   1.154 -
   1.155 -      val more_args = getopts(args)
   1.156 -      val app_archive =
   1.157 -        more_args match {
   1.158 -          case List(arg) => arg
   1.159 -          case _ => getopts.usage()
   1.160 -        }
   1.161 -
   1.162 -      build_docker(new Console_Progress(), app_archive, base = base, logic = logic,
   1.163 -        no_build = no_build, entrypoint = entrypoint, output = output,
   1.164 -        more_packages = more_packages, tag = tag, verbose = verbose)
   1.165 -    }, admin = true)
   1.166 -}