build_docker is regular tool (non-admin);
authorwenzelm
Sun Oct 08 14:52:06 2017 +0200 (19 months ago)
changeset 66790c0e68e6a1beb
parent 66789 feb36b73a7f0
child 66791 e51f789f7705
build_docker is regular tool (non-admin);
src/Pure/Admin/build_docker.scala
src/Pure/Tools/build_docker.scala
src/Pure/build-jars
     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 -}
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/Tools/build_docker.scala	Sun Oct 08 14:52:06 2017 +0200
     2.3 @@ -0,0 +1,163 @@
     2.4 +/*  Title:      Pure/Tools/build_docker.scala
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +Build docker image from Isabelle application bundle for Linux.
     2.8 +*/
     2.9 +
    2.10 +package isabelle
    2.11 +
    2.12 +
    2.13 +object Build_Docker
    2.14 +{
    2.15 +  private val default_base = "ubuntu"
    2.16 +  private lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC")
    2.17 +
    2.18 +  private val Isabelle_Name = """^.*?(Isabelle[^/\\:]+)_(?:app|linux)\.tar\.gz$""".r
    2.19 +
    2.20 +  val packages: List[String] =
    2.21 +    List("curl", "less", "lib32stdc++6", "libgomp1", "libwww-perl", "rlwrap", "unzip")
    2.22 +
    2.23 +  val package_collections: Map[String, List[String]] =
    2.24 +    Map("X11" -> List("libx11-6", "libxext6", "libxrender1", "libxtst6", "libxi6"),
    2.25 +      "latex" -> List("texlive-fonts-extra", "texlive-latex-extra", "texlive-math-extra"))
    2.26 +
    2.27 +  def build_docker(progress: Progress,
    2.28 +    app_archive: String,
    2.29 +    base: String = default_base,
    2.30 +    logic: String = default_logic,
    2.31 +    no_build: Boolean = false,
    2.32 +    entrypoint: Boolean = false,
    2.33 +    output: Option[Path] = None,
    2.34 +    more_packages: List[String] = Nil,
    2.35 +    tag: String = "",
    2.36 +    verbose: Boolean = false)
    2.37 +  {
    2.38 +    val isabelle_name =
    2.39 +      app_archive match {
    2.40 +        case Isabelle_Name(name) => name
    2.41 +        case _ => error("Cannot determine Isabelle distribution name from " + app_archive)
    2.42 +      }
    2.43 +    val is_remote = Url.is_wellformed(app_archive)
    2.44 +
    2.45 +    val dockerfile =
    2.46 +      """## Dockerfile for """ + isabelle_name + """
    2.47 +
    2.48 +FROM """ + base + """
    2.49 +SHELL ["/bin/bash", "-c"]
    2.50 +
    2.51 +# packages
    2.52 +RUN apt-get -y update && \
    2.53 +  apt-get install -y """ + Bash.strings(packages ::: more_packages) + """ && \
    2.54 +  apt-get clean
    2.55 +
    2.56 +# user
    2.57 +RUN useradd -m isabelle && (echo isabelle:isabelle | chpasswd)
    2.58 +USER isabelle
    2.59 +
    2.60 +# Isabelle
    2.61 +WORKDIR /home/isabelle
    2.62 +""" +
    2.63 + (if (is_remote)
    2.64 +   "RUN curl --fail --silent " + Bash.string(app_archive) + " > Isabelle.tar.gz"
    2.65 +  else "COPY Isabelle.tar.gz .") +
    2.66 +"""
    2.67 +RUN tar xzf Isabelle.tar.gz && \
    2.68 +  mv """ + isabelle_name + """ Isabelle && \
    2.69 +  rm -rf Isabelle.tar.gz Isabelle/contrib/jdk/x86-linux && \
    2.70 +  perl -pi -e 's,ISABELLE_HOME_USER=.*,ISABELLE_HOME_USER="\$USER_HOME/.isabelle",g;' Isabelle/etc/settings && \
    2.71 +  perl -pi -e 's,ISABELLE_LOGIC=.*,ISABELLE_LOGIC=""" + logic + """,g;' Isabelle/etc/settings && \
    2.72 +  Isabelle/bin/isabelle build -s -b """ + logic +
    2.73 + (if (entrypoint) """
    2.74 +
    2.75 +ENTRYPOINT ["Isabelle/bin/isabelle"]
    2.76 +"""
    2.77 +  else "")
    2.78 +
    2.79 +    output.foreach(File.write(_, dockerfile))
    2.80 +
    2.81 +    if (!no_build) {
    2.82 +      Isabelle_System.with_tmp_dir("docker")(tmp_dir =>
    2.83 +        {
    2.84 +          File.write(tmp_dir + Path.explode("Dockerfile"), dockerfile)
    2.85 +
    2.86 +          if (is_remote) {
    2.87 +            if (!Url.is_readable(app_archive))
    2.88 +              error("Cannot access remote archive " + app_archive)
    2.89 +          }
    2.90 +          else File.copy(Path.explode(app_archive), tmp_dir + Path.explode("Isabelle.tar.gz"))
    2.91 +
    2.92 +          val quiet_option = if (verbose) "" else " -q"
    2.93 +          val tag_option = if (tag == "") "" else " -t " + Bash.string(tag)
    2.94 +          progress.bash("docker build" + quiet_option + tag_option + " " + File.bash_path(tmp_dir),
    2.95 +            echo = true).check
    2.96 +        })
    2.97 +    }
    2.98 +  }
    2.99 +
   2.100 +
   2.101 +  /* Isabelle tool wrapper */
   2.102 +
   2.103 +  val isabelle_tool =
   2.104 +    Isabelle_Tool("build_docker", "build Isabelle docker image", args =>
   2.105 +    {
   2.106 +      var base = default_base
   2.107 +      var entrypoint = false
   2.108 +      var logic = default_logic
   2.109 +      var no_build = false
   2.110 +      var output: Option[Path] = None
   2.111 +      var more_packages: List[String] = Nil
   2.112 +      var verbose = false
   2.113 +      var tag = ""
   2.114 +
   2.115 +      val getopts =
   2.116 +        Getopts("""
   2.117 +Usage: isabelle build_docker [OPTIONS] APP_ARCHIVE
   2.118 +
   2.119 +  Options are:
   2.120 +    -B NAME      base image (default """ + quote(default_base) + """)
   2.121 +    -E           set bin/isabelle as entrypoint
   2.122 +    -P NAME      additional Ubuntu package collection (""" +
   2.123 +          package_collections.keySet.toList.sorted.map(quote(_)).mkString(", ") + """)
   2.124 +    -l NAME      default logic (default ISABELLE_LOGIC=""" + quote(default_logic) + """)
   2.125 +    -n           no docker build
   2.126 +    -o FILE      output generated Dockerfile
   2.127 +    -p NAME      additional Ubuntu package
   2.128 +    -t TAG       docker build tag
   2.129 +    -v           verbose
   2.130 +
   2.131 +  Build Isabelle docker image with default logic image, using a standard
   2.132 +  Isabelle application archive for Linux (local file or remote URL).
   2.133 +
   2.134 +  Examples:
   2.135 +
   2.136 +    isabelle build_docker -E -t test/isabelle:Isabelle2017 Isabelle2017_app.tar.gz
   2.137 +
   2.138 +    isabelle build_docker -E -n -o Dockerfile http://isabelle.in.tum.de/dist/Isabelle2017_app.tar.gz
   2.139 +
   2.140 +""",
   2.141 +          "B:" -> (arg => base = arg),
   2.142 +          "E" -> (_ => entrypoint = true),
   2.143 +          "P:" -> (arg =>
   2.144 +            package_collections.get(arg) match {
   2.145 +              case Some(ps) => more_packages :::= ps
   2.146 +              case None => error("Unknown package collection " + quote(arg))
   2.147 +            }),
   2.148 +          "l:" -> (arg => logic = arg),
   2.149 +          "n" -> (_ => no_build = true),
   2.150 +          "o:" -> (arg => output = Some(Path.explode(arg))),
   2.151 +          "p:" -> (arg => more_packages ::= arg),
   2.152 +          "t:" -> (arg => tag = arg),
   2.153 +          "v" -> (_ => verbose = true))
   2.154 +
   2.155 +      val more_args = getopts(args)
   2.156 +      val app_archive =
   2.157 +        more_args match {
   2.158 +          case List(arg) => arg
   2.159 +          case _ => getopts.usage()
   2.160 +        }
   2.161 +
   2.162 +      build_docker(new Console_Progress(), app_archive, base = base, logic = logic,
   2.163 +        no_build = no_build, entrypoint = entrypoint, output = output,
   2.164 +        more_packages = more_packages, tag = tag, verbose = verbose)
   2.165 +    })
   2.166 +}
     3.1 --- a/src/Pure/build-jars	Sun Oct 08 14:48:47 2017 +0200
     3.2 +++ b/src/Pure/build-jars	Sun Oct 08 14:52:06 2017 +0200
     3.3 @@ -11,7 +11,6 @@
     3.4  declare -a SOURCES=(
     3.5    Admin/build_cygwin.scala
     3.6    Admin/build_doc.scala
     3.7 -  Admin/build_docker.scala
     3.8    Admin/build_history.scala
     3.9    Admin/build_jdk.scala
    3.10    Admin/build_log.scala
    3.11 @@ -133,6 +132,7 @@
    3.12    Thy/thy_syntax.scala
    3.13    Tools/bibtex.scala
    3.14    Tools/build.scala
    3.15 +  Tools/build_docker.scala
    3.16    Tools/check_keywords.scala
    3.17    Tools/debugger.scala
    3.18    Tools/doc.scala