author | wenzelm |
Tue, 07 Mar 2023 23:26:02 +0100 | |
changeset 77571 | 643146163fd1 |
parent 77567 | src/Pure/Tools/build_docker.scala@b975f5aaf6b8 |
child 77794 | 89e4971df810 |
permissions | -rw-r--r-- |
77567
b975f5aaf6b8
renamed "isabelle build_docker" to "isabelle docker_build" (unrelated to "isabelle build");
wenzelm
parents:
77510
diff
changeset
|
1 |
/* Title: Pure/Tools/docker_build.scala |
64890
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 |
|
77567
b975f5aaf6b8
renamed "isabelle build_docker" to "isabelle docker_build" (unrelated to "isabelle build");
wenzelm
parents:
77510
diff
changeset
|
10 |
object Docker_Build { |
76184 | 11 |
private val default_base = "ubuntu:22.04" |
76178
1f95e9424341
more robust: snap version of docker cannot access /tmp;
wenzelm
parents:
76103
diff
changeset
|
12 |
private val default_work_dir = Path.current |
64890
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
13 |
private lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC") |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
14 |
|
74654
b67d1d72516b
support linux_arm as well, e.g. native Docker on Apple Silicon;
wenzelm
parents:
74492
diff
changeset
|
15 |
private val Isabelle_Name = """^.*?(Isabelle[^/\\:]+)_linux(?:_arm)?\.tar\.gz$""".r |
64905
5e2eb9b14bbe
support for remote APP_ARCHIVE, with self-contained Dockerfile (e.g. for Docker Hub);
wenzelm
parents:
64903
diff
changeset
|
16 |
|
64899
749d3a86c6a3
clarified signature: packages may be accessed in Isabelle/Scala;
wenzelm
parents:
64897
diff
changeset
|
17 |
val packages: List[String] = |
76553
120f79cdb492
discontinued "unzip" executable (see also eb96243a25c5 and 662de910a96b);
wenzelm
parents:
76395
diff
changeset
|
18 |
List("curl", "less", "libfontconfig1", "libgomp1", "openssh-client", "pwgen", "rsync") |
64894 | 19 |
|
64899
749d3a86c6a3
clarified signature: packages may be accessed in Isabelle/Scala;
wenzelm
parents:
64897
diff
changeset
|
20 |
val package_collections: Map[String, List[String]] = |
64895 | 21 |
Map("X11" -> List("libx11-6", "libxext6", "libxrender1", "libxtst6", "libxi6"), |
69958 | 22 |
"latex" -> |
76395
fac28b6c37e8
support for Dagstuhl LIPIcs style with demo document;
wenzelm
parents:
76184
diff
changeset
|
23 |
List( |
fac28b6c37e8
support for Dagstuhl LIPIcs style with demo document;
wenzelm
parents:
76184
diff
changeset
|
24 |
"texlive-bibtex-extra", |
fac28b6c37e8
support for Dagstuhl LIPIcs style with demo document;
wenzelm
parents:
76184
diff
changeset
|
25 |
"texlive-fonts-extra", |
fac28b6c37e8
support for Dagstuhl LIPIcs style with demo document;
wenzelm
parents:
76184
diff
changeset
|
26 |
"texlive-font-utils", |
fac28b6c37e8
support for Dagstuhl LIPIcs style with demo document;
wenzelm
parents:
76184
diff
changeset
|
27 |
"texlive-latex-extra", |
fac28b6c37e8
support for Dagstuhl LIPIcs style with demo document;
wenzelm
parents:
76184
diff
changeset
|
28 |
"texlive-science")) |
64894 | 29 |
|
76103 | 30 |
def all_packages: List[String] = |
31 |
packages ::: package_collections.valuesIterator.flatten.toList |
|
32 |
||
77567
b975f5aaf6b8
renamed "isabelle build_docker" to "isabelle docker_build" (unrelated to "isabelle build");
wenzelm
parents:
77510
diff
changeset
|
33 |
def docker_build(progress: Progress, |
64905
5e2eb9b14bbe
support for remote APP_ARCHIVE, with self-contained Dockerfile (e.g. for Docker Hub);
wenzelm
parents:
64903
diff
changeset
|
34 |
app_archive: String, |
64942 | 35 |
base: String = default_base, |
76178
1f95e9424341
more robust: snap version of docker cannot access /tmp;
wenzelm
parents:
76103
diff
changeset
|
36 |
work_dir: Path = default_work_dir, |
64890
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
37 |
logic: String = default_logic, |
64906
49549acbf025
added option -n, e.g. useful to generate Dockerfile only;
wenzelm
parents:
64905
diff
changeset
|
38 |
no_build: Boolean = false, |
64942 | 39 |
entrypoint: Boolean = false, |
64890
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
40 |
output: Option[Path] = None, |
64899
749d3a86c6a3
clarified signature: packages may be accessed in Isabelle/Scala;
wenzelm
parents:
64897
diff
changeset
|
41 |
more_packages: List[String] = Nil, |
77510
f5d6cd98b16a
clarified signature: manage "verbose" flag via "progress";
wenzelm
parents:
77504
diff
changeset
|
42 |
tag: String = "" |
75393 | 43 |
): Unit = { |
64905
5e2eb9b14bbe
support for remote APP_ARCHIVE, with self-contained Dockerfile (e.g. for Docker Hub);
wenzelm
parents:
64903
diff
changeset
|
44 |
val isabelle_name = |
5e2eb9b14bbe
support for remote APP_ARCHIVE, with self-contained Dockerfile (e.g. for Docker Hub);
wenzelm
parents:
64903
diff
changeset
|
45 |
app_archive match { |
5e2eb9b14bbe
support for remote APP_ARCHIVE, with self-contained Dockerfile (e.g. for Docker Hub);
wenzelm
parents:
64903
diff
changeset
|
46 |
case Isabelle_Name(name) => name |
64890
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
47 |
case _ => error("Cannot determine Isabelle distribution name from " + app_archive) |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
48 |
} |
64905
5e2eb9b14bbe
support for remote APP_ARCHIVE, with self-contained Dockerfile (e.g. for Docker Hub);
wenzelm
parents:
64903
diff
changeset
|
49 |
val is_remote = Url.is_wellformed(app_archive) |
64890
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
50 |
|
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
51 |
val dockerfile = |
64905
5e2eb9b14bbe
support for remote APP_ARCHIVE, with self-contained Dockerfile (e.g. for Docker Hub);
wenzelm
parents:
64903
diff
changeset
|
52 |
"""## Dockerfile for """ + isabelle_name + """ |
64890
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
53 |
|
64942 | 54 |
FROM """ + base + """ |
64890
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
55 |
SHELL ["/bin/bash", "-c"] |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
56 |
|
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
57 |
# packages |
69958 | 58 |
ENV DEBIAN_FRONTEND=noninteractive |
64890
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
59 |
RUN apt-get -y update && \ |
64941 | 60 |
apt-get install -y """ + Bash.strings(packages ::: more_packages) + """ && \ |
64890
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
61 |
apt-get clean |
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 |
# user |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
64 |
RUN useradd -m isabelle && (echo isabelle:isabelle | chpasswd) |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
65 |
USER isabelle |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
66 |
|
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
67 |
# Isabelle |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
68 |
WORKDIR /home/isabelle |
75659
9bd92ac9328f
more robust Scala 3 indentation, for the sake of IntelliJ IDEA;
wenzelm
parents:
75394
diff
changeset
|
69 |
""" + (if (is_remote) |
77052
86ace3c45837
more uniform options for "curl", following lib/Tools/components;
wenzelm
parents:
76553
diff
changeset
|
70 |
"RUN curl --fail --silent --location " + Bash.string(app_archive) + " > Isabelle.tar.gz" |
75659
9bd92ac9328f
more robust Scala 3 indentation, for the sake of IntelliJ IDEA;
wenzelm
parents:
75394
diff
changeset
|
71 |
else "COPY Isabelle.tar.gz .") + """ |
64890
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
72 |
RUN tar xzf Isabelle.tar.gz && \ |
64905
5e2eb9b14bbe
support for remote APP_ARCHIVE, with self-contained Dockerfile (e.g. for Docker Hub);
wenzelm
parents:
64903
diff
changeset
|
73 |
mv """ + isabelle_name + """ Isabelle && \ |
74727 | 74 |
sed -i -e 's,ISABELLE_HOME_USER=.*,ISABELLE_HOME_USER="\$USER_HOME/.isabelle",g;' Isabelle/etc/settings && \ |
75 |
sed -i -e 's,ISABELLE_LOGIC=.*,ISABELLE_LOGIC=""" + logic + """,g;' Isabelle/etc/settings && \ |
|
71580 | 76 |
Isabelle/bin/isabelle build -o system_heaps -b """ + logic + """ && \ |
75659
9bd92ac9328f
more robust Scala 3 indentation, for the sake of IntelliJ IDEA;
wenzelm
parents:
75394
diff
changeset
|
77 |
rm Isabelle.tar.gz""" + (if (entrypoint) """ |
64890
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 |
ENTRYPOINT ["Isabelle/bin/isabelle"] |
75659
9bd92ac9328f
more robust Scala 3 indentation, for the sake of IntelliJ IDEA;
wenzelm
parents:
75394
diff
changeset
|
80 |
""" else "") |
64890
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
81 |
|
76182 | 82 |
for (path <- output) { |
83 |
progress.echo("Dockerfile: " + path.absolute) |
|
84 |
File.write(path, dockerfile) |
|
85 |
} |
|
64890
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
86 |
|
64906
49549acbf025
added option -n, e.g. useful to generate Dockerfile only;
wenzelm
parents:
64905
diff
changeset
|
87 |
if (!no_build) { |
76182 | 88 |
Isabelle_System.make_directory(work_dir) |
76178
1f95e9424341
more robust: snap version of docker cannot access /tmp;
wenzelm
parents:
76103
diff
changeset
|
89 |
progress.echo("Docker working directory: " + work_dir.absolute) |
76182 | 90 |
|
76178
1f95e9424341
more robust: snap version of docker cannot access /tmp;
wenzelm
parents:
76103
diff
changeset
|
91 |
Isabelle_System.with_tmp_dir("docker_build", base_dir = work_dir.file) { tmp_dir => |
76182 | 92 |
progress.echo("Docker temporary directory: " + tmp_dir.absolute) |
93 |
||
75394 | 94 |
File.write(tmp_dir + Path.explode("Dockerfile"), dockerfile) |
64905
5e2eb9b14bbe
support for remote APP_ARCHIVE, with self-contained Dockerfile (e.g. for Docker Hub);
wenzelm
parents:
64903
diff
changeset
|
95 |
|
75394 | 96 |
if (is_remote) { |
97 |
if (!Url.is_readable(app_archive)) |
|
98 |
error("Cannot access remote archive " + app_archive) |
|
99 |
} |
|
76178
1f95e9424341
more robust: snap version of docker cannot access /tmp;
wenzelm
parents:
76103
diff
changeset
|
100 |
else { |
1f95e9424341
more robust: snap version of docker cannot access /tmp;
wenzelm
parents:
76103
diff
changeset
|
101 |
Isabelle_System.copy_file(Path.explode(app_archive), |
1f95e9424341
more robust: snap version of docker cannot access /tmp;
wenzelm
parents:
76103
diff
changeset
|
102 |
tmp_dir + Path.explode("Isabelle.tar.gz")) |
1f95e9424341
more robust: snap version of docker cannot access /tmp;
wenzelm
parents:
76103
diff
changeset
|
103 |
} |
64890
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
104 |
|
77510
f5d6cd98b16a
clarified signature: manage "verbose" flag via "progress";
wenzelm
parents:
77504
diff
changeset
|
105 |
val quiet_option = if (progress.verbose) "" else " -q" |
77504 | 106 |
val tag_option = if_proper(tag, " -t " + Bash.string(tag)) |
75394 | 107 |
progress.bash("docker build" + quiet_option + tag_option + " " + File.bash_path(tmp_dir), |
108 |
echo = true).check |
|
109 |
} |
|
64906
49549acbf025
added option -n, e.g. useful to generate Dockerfile only;
wenzelm
parents:
64905
diff
changeset
|
110 |
} |
64890
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
111 |
} |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
112 |
|
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
113 |
|
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
114 |
/* Isabelle tool wrapper */ |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
115 |
|
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
116 |
val isabelle_tool = |
77567
b975f5aaf6b8
renamed "isabelle build_docker" to "isabelle docker_build" (unrelated to "isabelle build");
wenzelm
parents:
77510
diff
changeset
|
117 |
Isabelle_Tool("docker_build", "build Isabelle docker image", |
75394 | 118 |
Scala_Project.here, |
119 |
{ args => |
|
120 |
var base = default_base |
|
121 |
var entrypoint = false |
|
76178
1f95e9424341
more robust: snap version of docker cannot access /tmp;
wenzelm
parents:
76103
diff
changeset
|
122 |
var work_dir = default_work_dir |
75394 | 123 |
var logic = default_logic |
124 |
var no_build = false |
|
125 |
var output: Option[Path] = None |
|
126 |
var more_packages: List[String] = Nil |
|
127 |
var verbose = false |
|
128 |
var tag = "" |
|
64890
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
129 |
|
75394 | 130 |
val getopts = Getopts(""" |
77567
b975f5aaf6b8
renamed "isabelle build_docker" to "isabelle docker_build" (unrelated to "isabelle build");
wenzelm
parents:
77510
diff
changeset
|
131 |
Usage: isabelle docker_build [OPTIONS] APP_ARCHIVE |
64890
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
132 |
|
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
133 |
Options are: |
64942 | 134 |
-B NAME base image (default """ + quote(default_base) + """) |
72525 | 135 |
-E set Isabelle/bin/isabelle as entrypoint |
64894 | 136 |
-P NAME additional Ubuntu package collection (""" + |
64895 | 137 |
package_collections.keySet.toList.sorted.map(quote(_)).mkString(", ") + """) |
76178
1f95e9424341
more robust: snap version of docker cannot access /tmp;
wenzelm
parents:
76103
diff
changeset
|
138 |
-W DIR working directory that is accessible to docker, |
1f95e9424341
more robust: snap version of docker cannot access /tmp;
wenzelm
parents:
76103
diff
changeset
|
139 |
potentially via snap (default: """ + default_work_dir + """) |
64890
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
140 |
-l NAME default logic (default ISABELLE_LOGIC=""" + quote(default_logic) + """) |
64906
49549acbf025
added option -n, e.g. useful to generate Dockerfile only;
wenzelm
parents:
64905
diff
changeset
|
141 |
-n no docker build |
64890
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
142 |
-o FILE output generated Dockerfile |
64894 | 143 |
-p NAME additional Ubuntu package |
64890
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
144 |
-t TAG docker build tag |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
145 |
-v verbose |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
146 |
|
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
147 |
Build Isabelle docker image with default logic image, using a standard |
64905
5e2eb9b14bbe
support for remote APP_ARCHIVE, with self-contained Dockerfile (e.g. for Docker Hub);
wenzelm
parents:
64903
diff
changeset
|
148 |
Isabelle application archive for Linux (local file or remote URL). |
64890
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
149 |
""", |
64942 | 150 |
"B:" -> (arg => base = arg), |
151 |
"E" -> (_ => entrypoint = true), |
|
64894 | 152 |
"P:" -> (arg => |
153 |
package_collections.get(arg) match { |
|
64899
749d3a86c6a3
clarified signature: packages may be accessed in Isabelle/Scala;
wenzelm
parents:
64897
diff
changeset
|
154 |
case Some(ps) => more_packages :::= ps |
64894 | 155 |
case None => error("Unknown package collection " + quote(arg)) |
156 |
}), |
|
76178
1f95e9424341
more robust: snap version of docker cannot access /tmp;
wenzelm
parents:
76103
diff
changeset
|
157 |
"W:" -> (arg => work_dir = Path.explode(arg)), |
64890
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
158 |
"l:" -> (arg => logic = arg), |
64906
49549acbf025
added option -n, e.g. useful to generate Dockerfile only;
wenzelm
parents:
64905
diff
changeset
|
159 |
"n" -> (_ => no_build = true), |
64890
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
160 |
"o:" -> (arg => output = Some(Path.explode(arg))), |
64899
749d3a86c6a3
clarified signature: packages may be accessed in Isabelle/Scala;
wenzelm
parents:
64897
diff
changeset
|
161 |
"p:" -> (arg => more_packages ::= arg), |
64890
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
162 |
"t:" -> (arg => tag = arg), |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
163 |
"v" -> (_ => verbose = true)) |
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
164 |
|
75394 | 165 |
val more_args = getopts(args) |
166 |
val app_archive = |
|
167 |
more_args match { |
|
168 |
case List(arg) => arg |
|
169 |
case _ => getopts.usage() |
|
170 |
} |
|
64890
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
171 |
|
77510
f5d6cd98b16a
clarified signature: manage "verbose" flag via "progress";
wenzelm
parents:
77504
diff
changeset
|
172 |
val progress = new Console_Progress(verbose = verbose) |
f5d6cd98b16a
clarified signature: manage "verbose" flag via "progress";
wenzelm
parents:
77504
diff
changeset
|
173 |
|
77567
b975f5aaf6b8
renamed "isabelle build_docker" to "isabelle docker_build" (unrelated to "isabelle build");
wenzelm
parents:
77510
diff
changeset
|
174 |
docker_build(progress, app_archive, base = base, work_dir = work_dir, |
76178
1f95e9424341
more robust: snap version of docker cannot access /tmp;
wenzelm
parents:
76103
diff
changeset
|
175 |
logic = logic, no_build = no_build, entrypoint = entrypoint, output = output, |
77510
f5d6cd98b16a
clarified signature: manage "verbose" flag via "progress";
wenzelm
parents:
77504
diff
changeset
|
176 |
more_packages = more_packages, tag = tag) |
75394 | 177 |
}) |
64890
d8ccbd5305bf
build docker image from Isabelle application bundle for Linux;
wenzelm
parents:
diff
changeset
|
178 |
} |