70 |
70 |
71 \<^medskip> |
71 \<^medskip> |
72 Option \<^verbatim>\<open>-B\<close> specifies the Docker image taken as starting point for the |
72 Option \<^verbatim>\<open>-B\<close> specifies the Docker image taken as starting point for the |
73 Isabelle installation: it needs to be a suitable version of Ubuntu Linux, |
73 Isabelle installation: it needs to be a suitable version of Ubuntu Linux, |
74 see also \<^url>\<open>https://hub.docker.com/_/ubuntu\<close>. The default for Isabelle2024 |
74 see also \<^url>\<open>https://hub.docker.com/_/ubuntu\<close>. The default for Isabelle2024 |
75 is \<^verbatim>\<open>ubuntu:22.04\<close>, but other versions often work as well, after some |
75 is \<^verbatim>\<open>ubuntu:22.04\<close>, but \<^verbatim>\<open>ubuntu:20.04\<close> and \<^verbatim>\<open>ubuntu:24.04\<close> should work as |
76 experimentation with packages. |
76 well. Other versions might require experimentation with the package |
|
77 selection. |
77 |
78 |
78 Option \<^verbatim>\<open>-p\<close> includes additional Ubuntu packages, using the terminology |
79 Option \<^verbatim>\<open>-p\<close> includes additional Ubuntu packages, using the terminology |
79 of \<^verbatim>\<open>apt-get install\<close> within the underlying Linux distribution. |
80 of \<^verbatim>\<open>apt-get install\<close> within the underlying Linux distribution. |
80 |
81 |
81 Option \<^verbatim>\<open>-P\<close> refers to high-level package collections: \<^verbatim>\<open>X11\<close> or \<^verbatim>\<open>latex\<close> as |
82 Option \<^verbatim>\<open>-P\<close> refers to high-level package collections: \<^verbatim>\<open>X11\<close> or \<^verbatim>\<open>latex\<close> as |
82 provided by \<^verbatim>\<open>isabelle docker_build\<close> (assuming Ubuntu 22.04 LTS). This |
83 provided by \<^verbatim>\<open>isabelle docker_build\<close> (assuming Ubuntu 20.04/22.04/24.04 |
83 imposes extra weight on the resulting Docker images. Note that \<^verbatim>\<open>X11\<close> will |
84 LTS). This imposes extra weight on the resulting Docker images. Note that |
84 only provide remote X11 support according to the modest GUI quality |
85 \<^verbatim>\<open>X11\<close> will only provide remote X11 support according to the modest GUI |
85 standards of the late 1990-ies. |
86 quality standards of the late 1990-ies. |
86 |
87 |
87 \<^medskip> |
88 \<^medskip> |
88 Option \<^verbatim>\<open>-n\<close> suppresses the actual \<^verbatim>\<open>docker build\<close> process. Option \<^verbatim>\<open>-o\<close> |
89 Option \<^verbatim>\<open>-n\<close> suppresses the actual \<^verbatim>\<open>docker build\<close> process. Option \<^verbatim>\<open>-o\<close> |
89 outputs the generated \<^verbatim>\<open>Dockerfile\<close>. Both options together produce a |
90 outputs the generated \<^verbatim>\<open>Dockerfile\<close>. Both options together produce a |
90 Dockerfile only, which might be useful for informative purposes or other |
91 Dockerfile only, which might be useful for informative purposes or other |