author | wenzelm |
Sun, 15 Jan 2017 12:19:48 +0100 | |
changeset 64895 | ad3b66e7a028 |
parent 64894 | 6c6bb62702d4 |
child 64896 | 6d709a78e269 |
permissions | -rw-r--r-- |
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 |
|
64894 | 14 |
private val standard_packages = |
15 |
List("less", "lib32stdc++6", "libwww-perl", "rlwrap", "unzip") |
|
16 |
||
17 |
private val package_collections = |
|
64895 | 18 |
Map("X11" -> List("libx11-6", "libxext6", "libxrender1", "libxtst6", "libxi6"), |
19 |
"latex" -> List("texlive-fonts-extra", "texlive-latex-extra", "texlive-math-extra")) |
|
64894 | 20 |
|
64890
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
21 |
def build_docker(progress: Progress, |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
22 |
app_archive: Path, |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
23 |
logic: String = default_logic, |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
24 |
output: Option[Path] = None, |
64893 | 25 |
packages: List[String] = Nil, |
64890
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
26 |
tag: String = "", |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
27 |
verbose: Boolean = false) |
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 |
val distname = |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
30 |
{ |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
31 |
val Name = "^(Isabelle[^/]*)/?.*$".r |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
32 |
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
|
33 |
case Name(name) :: _ => name |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
34 |
case _ => error("Cannot determine Isabelle distribution name from " + app_archive) |
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 |
} |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
37 |
|
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
38 |
val dockerfile = |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
39 |
"""## Dockerfile for """ + distname + """ |
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 |
FROM ubuntu |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
42 |
SHELL ["/bin/bash", "-c"] |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
43 |
|
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
44 |
# packages |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
45 |
RUN apt-get -y update && \ |
64894 | 46 |
apt-get install -y """ + (standard_packages ::: packages).map(Bash.string(_)).mkString(" ") + """ && \ |
64890
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
47 |
apt-get clean |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
48 |
|
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
49 |
# user |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
50 |
RUN useradd -m isabelle && (echo isabelle:isabelle | chpasswd) |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
51 |
USER isabelle |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
52 |
|
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
53 |
# Isabelle |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
54 |
WORKDIR /home/isabelle |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
55 |
COPY Isabelle.tar.gz . |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
56 |
RUN tar xzf Isabelle.tar.gz && \ |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
57 |
mv """ + distname + """ Isabelle && \ |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
58 |
rm -rf Isabelle.tar.gz Isabelle/contrib/jdk/x86-linux && \ |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
59 |
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
|
60 |
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
|
61 |
Isabelle/bin/isabelle build -s -b """ + logic + """ |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
62 |
|
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
63 |
ENTRYPOINT ["Isabelle/bin/isabelle"] |
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 |
|
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
66 |
output.foreach(File.write(_, dockerfile)) |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
67 |
|
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
68 |
Isabelle_System.with_tmp_dir("docker")(tmp_dir => |
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 |
File.write(tmp_dir + Path.explode("Dockerfile"), dockerfile) |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
71 |
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
|
72 |
|
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
73 |
val quiet_option = if (verbose) "" else " -q" |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
74 |
val tag_option = if (tag == "") "" else " -t " + Bash.string(tag) |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
75 |
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
|
76 |
echo = true).check |
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 |
} |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
79 |
|
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
80 |
|
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
81 |
/* Isabelle tool wrapper */ |
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 isabelle_tool = |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
84 |
Isabelle_Tool("build_docker", "build Isabelle docker image", args => |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
85 |
{ |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
86 |
var logic = default_logic |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
87 |
var output: Option[Path] = None |
64893 | 88 |
var packages: List[String] = Nil |
64890
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
89 |
var verbose = false |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
90 |
var tag = "" |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
91 |
|
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
92 |
val getopts = |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
93 |
Getopts(""" |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
94 |
Usage: isabelle build_docker [OPTIONS] APP_ARCHIVE |
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 |
Options are: |
64894 | 97 |
-P NAME additional Ubuntu package collection (""" + |
64895 | 98 |
package_collections.keySet.toList.sorted.map(quote(_)).mkString(", ") + """) |
64890
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
99 |
-l NAME default logic (default ISABELLE_LOGIC=""" + quote(default_logic) + """) |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
100 |
-o FILE output generated Dockerfile |
64894 | 101 |
-p NAME additional Ubuntu package |
64890
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
102 |
-t TAG docker build tag |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
103 |
-v verbose |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
104 |
|
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
105 |
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
|
106 |
Isabelle application archive for Linux. |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
107 |
|
64895 | 108 |
Example: |
109 |
||
110 |
isabelle build_docker -t isabelle/Isabelle2016-1 Isabelle2016-1_app.tar.gz |
|
64890
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
111 |
""", |
64894 | 112 |
"P:" -> (arg => |
113 |
package_collections.get(arg) match { |
|
114 |
case Some(ps) => packages :::= ps |
|
115 |
case None => error("Unknown package collection " + quote(arg)) |
|
116 |
}), |
|
64890
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
117 |
"l:" -> (arg => logic = arg), |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
118 |
"o:" -> (arg => output = Some(Path.explode(arg))), |
64893 | 119 |
"p:" -> (arg => packages ::= arg), |
64890
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
120 |
"t:" -> (arg => tag = arg), |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
121 |
"v" -> (_ => verbose = true)) |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
122 |
|
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
123 |
val more_args = getopts(args) |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
124 |
val app_archive = |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
125 |
more_args match { |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
126 |
case List(arg) => Path.explode(arg) |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
127 |
case _ => getopts.usage() |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
128 |
} |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
129 |
|
64893 | 130 |
build_docker(new Console_Progress(), app_archive, logic = logic, output = output, |
131 |
packages = packages, tag = tag, verbose = verbose) |
|
64890
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
132 |
}, admin = true) |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
133 |
} |