# HG changeset patch
# User wenzelm
# Date 1663360394 -7200
# Node ID 1f95e94243412162a8a45626e2f5eab433536d5e
# Parent  b847a9983784b6826bfe477c4849cafae7743076
more robust: snap version of docker cannot access /tmp;

diff -r b847a9983784 -r 1f95e9424341 NEWS
--- a/NEWS	Fri Sep 16 20:54:56 2022 +0200
+++ b/NEWS	Fri Sep 16 22:33:14 2022 +0200
@@ -293,6 +293,9 @@
 to identity the original build process uniquely. Thus other tools may
 dependent symbolically on a particular build instance.
 
+* Command-line tool "isabelle build_docker" supports Docker within Snap
+more robustly; see also option -W.
+
 * Command-line tool "isabelle scala_project" supports Gradle as
 alternative to Maven: either option -G or -M needs to be specified
 explicitly. This increases the chances that the Java/Scala IDE project
diff -r b847a9983784 -r 1f95e9424341 src/Doc/System/Misc.thy
--- a/src/Doc/System/Misc.thy	Fri Sep 16 20:54:56 2022 +0200
+++ b/src/Doc/System/Misc.thy	Fri Sep 16 22:33:14 2022 +0200
@@ -41,6 +41,8 @@
     -B NAME      base image (default "ubuntu")
     -E           set Isabelle/bin/isabelle as entrypoint
     -P NAME      additional Ubuntu package collection ("X11", "latex")
+    -W DIR       working directory that is accessible to docker,
+                 potentially via snap (default: ".")
     -l NAME      default logic (default ISABELLE_LOGIC="HOL")
     -n           no docker build
     -o FILE      output generated Dockerfile
@@ -89,6 +91,12 @@
   tools.
 
   Option \<^verbatim>\<open>-v\<close> disables quiet-mode of the underlying \<^verbatim>\<open>docker build\<close> process.
+
+  \<^medskip>
+  Option \<^verbatim>\<open>-W\<close> specifies an alternative work directory: it needs to be
+  accessible to docker, even if this is run via Snap (e.g.\ on Ubuntu 22.04).
+  The default ``\<^verbatim>\<open>.\<close>'' usually works, if this is owned by the user: the tool
+  will create a fresh directory within it, and remove it afterwards.
 \<close>
 
 
diff -r b847a9983784 -r 1f95e9424341 src/Pure/Tools/build_docker.scala
--- a/src/Pure/Tools/build_docker.scala	Fri Sep 16 20:54:56 2022 +0200
+++ b/src/Pure/Tools/build_docker.scala	Fri Sep 16 22:33:14 2022 +0200
@@ -9,6 +9,7 @@
 
 object Build_Docker {
   private val default_base = "ubuntu"
+  private val default_work_dir = Path.current
   private lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC")
 
   private val Isabelle_Name = """^.*?(Isabelle[^/\\:]+)_linux(?:_arm)?\.tar\.gz$""".r
@@ -27,6 +28,7 @@
   def build_docker(progress: Progress,
     app_archive: String,
     base: String = default_base,
+    work_dir: Path = default_work_dir,
     logic: String = default_logic,
     no_build: Boolean = false,
     entrypoint: Boolean = false,
@@ -76,15 +78,19 @@
     output.foreach(File.write(_, dockerfile))
 
     if (!no_build) {
-      Isabelle_System.with_tmp_dir("docker") { tmp_dir =>
+      progress.echo("Docker working directory: " + work_dir.absolute)
+      Isabelle_System.make_directory(work_dir)
+      Isabelle_System.with_tmp_dir("docker_build", base_dir = work_dir.file) { tmp_dir =>
         File.write(tmp_dir + Path.explode("Dockerfile"), dockerfile)
 
         if (is_remote) {
           if (!Url.is_readable(app_archive))
             error("Cannot access remote archive " + app_archive)
         }
-        else Isabelle_System.copy_file(Path.explode(app_archive),
-          tmp_dir + Path.explode("Isabelle.tar.gz"))
+        else {
+          Isabelle_System.copy_file(Path.explode(app_archive),
+            tmp_dir + Path.explode("Isabelle.tar.gz"))
+        }
 
         val quiet_option = if (verbose) "" else " -q"
         val tag_option = if (tag == "") "" else " -t " + Bash.string(tag)
@@ -103,6 +109,7 @@
       { args =>
         var base = default_base
         var entrypoint = false
+        var work_dir = default_work_dir
         var logic = default_logic
         var no_build = false
         var output: Option[Path] = None
@@ -118,6 +125,8 @@
     -E           set Isabelle/bin/isabelle as entrypoint
     -P NAME      additional Ubuntu package collection (""" +
           package_collections.keySet.toList.sorted.map(quote(_)).mkString(", ") + """)
+    -W DIR       working directory that is accessible to docker,
+                 potentially via snap (default: """ + default_work_dir + """)
     -l NAME      default logic (default ISABELLE_LOGIC=""" + quote(default_logic) + """)
     -n           no docker build
     -o FILE      output generated Dockerfile
@@ -135,6 +144,7 @@
               case Some(ps) => more_packages :::= ps
               case None => error("Unknown package collection " + quote(arg))
             }),
+          "W:" -> (arg => work_dir = Path.explode(arg)),
           "l:" -> (arg => logic = arg),
           "n" -> (_ => no_build = true),
           "o:" -> (arg => output = Some(Path.explode(arg))),
@@ -149,8 +159,8 @@
             case _ => getopts.usage()
           }
 
-        build_docker(new Console_Progress(), app_archive, base = base, logic = logic,
-          no_build = no_build, entrypoint = entrypoint, output = output,
+        build_docker(new Console_Progress(), app_archive, base = base, work_dir = work_dir,
+          logic = logic, no_build = no_build, entrypoint = entrypoint, output = output,
           more_packages = more_packages, tag = tag, verbose = verbose)
       })
 }