src/Pure/Tools/build_docker.scala
changeset 66790 c0e68e6a1beb
parent 66785 6fbd7fc824a9
child 66906 03a96b8c7c06
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Tools/build_docker.scala	Sun Oct 08 14:52:06 2017 +0200
     1.3 @@ -0,0 +1,163 @@
     1.4 +/*  Title:      Pure/Tools/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 +    })
   1.166 +}