diff --git a/src/Doc/System/Misc.thy b/src/Doc/System/Misc.thy --- a/src/Doc/System/Misc.thy +++ b/src/Doc/System/Misc.thy @@ -1,474 +1,474 @@ (*:maxLineLen=78:*) theory Misc imports Base begin chapter \Miscellaneous tools \label{ch:tools}\ text \ Subsequently we describe various Isabelle related utilities, given in alphabetical order. \ section \Building Isabelle docker images\ text \ Docker\<^footnote>\\<^url>\https://docs.docker.com\\ provides a self-contained environment for complex applications called \<^emph>\container\, although it does not fully contain the program in a strict sense of the word. This includes basic operating system services (usually based on Linux), shared libraries and other required packages. Thus Docker is a light-weight alternative to regular virtual machines, or a heavy-weight alternative to conventional self-contained applications. Although Isabelle can be easily run on a variety of OS environments without extra containment, Docker images may occasionally be useful when a standardized Linux environment is required, even on Windows\<^footnote>\\<^url>\https://docs.docker.com/docker-for-windows\\ and macOS\<^footnote>\\<^url>\https://docs.docker.com/docker-for-mac\\. Further uses are in common cloud computing environments, where applications need to be submitted as Docker images in the first place. \<^medskip> The @{tool_def build_docker} tool builds docker images from a standard Isabelle application archive for Linux: @{verbatim [display] \Usage: isabelle build_docker [OPTIONS] APP_ARCHIVE Options are: - -B NAME base image (default "ubuntu") + -B NAME base image (default "ubuntu:22.04") -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 -p NAME additional Ubuntu package -t TAG docker build tag -v verbose Build Isabelle docker image with default logic image, using a standard Isabelle application archive for Linux (local file or remote URL).\} Option \<^verbatim>\-E\ sets \<^verbatim>\bin/isabelle\ of the contained Isabelle distribution as the standard entry point of the Docker image. Thus \<^verbatim>\docker run\ will imitate the \<^verbatim>\isabelle\ command-line tool (\secref{sec:isabelle-tool}) of a regular local installation, but it lacks proper GUI support: \<^verbatim>\isabelle jedit\ will not work without further provisions. Note that the default entrypoint may be changed later via \<^verbatim>\docker run --entrypoint="..."\. Option \<^verbatim>\-t\ specifies the Docker image tag: this a symbolic name within the local Docker name space, but also relevant for Docker Hub\<^footnote>\\<^url>\https://hub.docker.com\\. Option \<^verbatim>\-l\ specifies the default logic image of the Isabelle distribution contained in the Docker environment: it will be produced by \<^verbatim>\isabelle build -b\ as usual (\secref{sec:tool-build}) and stored within the image. \<^medskip> Option \<^verbatim>\-B\ specifies the Docker image taken as starting point for the - Isabelle installation: it needs to be a suitable version of Ubuntu Linux. - The default \<^verbatim>\ubuntu\ refers to the latest LTS version provided by Canonical - as the official Ubuntu vendor\<^footnote>\\<^url>\https://hub.docker.com/_/ubuntu\\. For - Isabelle2022 this is normally Ubuntu 22.04 LTS. + Isabelle installation: it needs to be a suitable version of Ubuntu Linux, + see also \<^url>\https://hub.docker.com/_/ubuntu\. The default for Isabelle2022 + is \<^verbatim>\ubuntu:22.04\, but other versions often work as well, after some + experimentation with packages. Option \<^verbatim>\-p\ includes additional Ubuntu packages, using the terminology of \<^verbatim>\apt-get install\ within the underlying Linux distribution. Option \<^verbatim>\-P\ refers to high-level package collections: \<^verbatim>\X11\ or \<^verbatim>\latex\ as provided by \<^verbatim>\isabelle build_docker\ (assuming Ubuntu 20.04 LTS). This imposes extra weight on the resulting Docker images. Note that \<^verbatim>\X11\ will only provide remote X11 support according to the modest GUI quality standards of the late 1990-ies. \<^medskip> Option \<^verbatim>\-n\ suppresses the actual \<^verbatim>\docker build\ process. Option \<^verbatim>\-o\ outputs the generated \<^verbatim>\Dockerfile\. Both options together produce a Dockerfile only, which might be useful for informative purposes or other tools. Option \<^verbatim>\-v\ disables quiet-mode of the underlying \<^verbatim>\docker build\ process. \<^medskip> Option \<^verbatim>\-W\ 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>\.\'' usually works, if this is owned by the user: the tool will create a fresh directory within it, and remove it afterwards. \ subsubsection \Examples\ text \ Produce a Dockerfile (without image) from a remote Isabelle distribution: @{verbatim [display] \ isabelle build_docker -E -n -o Dockerfile https://isabelle.in.tum.de/website-Isabelle2022/dist/Isabelle2022_linux.tar.gz\} Build a standard Isabelle Docker image from a local Isabelle distribution, with \<^verbatim>\bin/isabelle\ as executable entry point: @{verbatim [display] \ isabelle build_docker -E -t test/isabelle:Isabelle2022 Isabelle2022_linux.tar.gz\} Invoke the raw Isabelle/ML process within that image: @{verbatim [display] \ docker run test/isabelle:Isabelle2022 process -e "Session.welcome ()"\} Invoke a Linux command-line tool within the contained Isabelle system environment: @{verbatim [display] \ docker run test/isabelle:Isabelle2022 env uname -a\} The latter should always report a Linux operating system, even when running on Windows or macOS. \ section \Managing Isabelle components \label{sec:tool-components}\ text \ The @{tool_def components} tool manages Isabelle components: @{verbatim [display] \Usage: isabelle components [OPTIONS] [COMPONENTS ...] Options are: -I init user settings -R URL component repository (default $ISABELLE_COMPONENT_REPOSITORY) -a resolve all missing components -l list status -u DIR update $ISABELLE_HOME_USER/components: add directory -x DIR update $ISABELLE_HOME_USER/components: remove directory Resolve Isabelle components via download and installation: given COMPONENTS are identified via base name. Further operations manage etc/settings and etc/components in $ISABELLE_HOME_USER. ISABELLE_COMPONENT_REPOSITORY="..." ISABELLE_HOME_USER="..." \} Components are initialized as described in \secref{sec:components} in a permissive manner, which can mark components as ``missing''. This state is amended by letting @{tool "components"} download and unpack components that are published on the default component repository \<^url>\https://isabelle.in.tum.de/components\ in particular. Option \<^verbatim>\-R\ specifies an alternative component repository. Note that \<^verbatim>\file:///\ URLs can be used for local directories. Option \<^verbatim>\-a\ selects all missing components to be resolved. Explicit components may be named as command line-arguments as well. Note that components are uniquely identified by their base name, while the installation takes place in the location that was specified in the attempt to initialize the component before. \<^medskip> Option \<^verbatim>\-l\ lists the current state of available and missing components with their location (full name) within the file-system. \<^medskip> Option \<^verbatim>\-I\ initializes the user settings file to subscribe to the standard components specified in the Isabelle repository clone --- this does not make any sense for regular Isabelle releases. An existing file that does not contain a suitable line ``\<^verbatim>\init_components\\\\\<^verbatim>\components/main\'' needs to be edited according to the printed explanation. \<^medskip> Options \<^verbatim>\-u\ and \<^verbatim>\-x\ operate on user components listed in \<^path>\$ISABELLE_HOME_USER/etc/components\: this avoids manual editing of Isabelle configuration files. \ section \Viewing documentation \label{sec:tool-doc}\ text \ The @{tool_def doc} tool displays Isabelle documentation: @{verbatim [display] \Usage: isabelle doc [DOC ...] View Isabelle PDF documentation.\} If called without arguments, it lists all available documents. Each line starts with an identifier, followed by a short description. Any of these identifiers may be specified as arguments, in order to display the corresponding document. \<^medskip> The @{setting ISABELLE_DOCS} setting specifies the list of directories (separated by colons) to be scanned for documentations. \ section \Shell commands within the settings environment \label{sec:tool-env}\ text \ The @{tool_def env} tool is a direct wrapper for the standard \<^verbatim>\/usr/bin/env\ command on POSIX systems, running within the Isabelle settings environment (\secref{sec:settings}). The command-line arguments are that of the underlying version of \<^verbatim>\env\. For example, the following invokes an instance of the GNU Bash shell within the Isabelle environment: @{verbatim [display] \isabelle env bash\} \ section \Inspecting the settings environment \label{sec:tool-getenv}\ text \The Isabelle settings environment --- as provided by the site-default and user-specific settings files --- can be inspected with the @{tool_def getenv} tool: @{verbatim [display] \Usage: isabelle getenv [OPTIONS] [VARNAMES ...] Options are: -a display complete environment -b print values only (doesn't work for -a) -d FILE dump complete environment to file (NUL terminated entries) Get value of VARNAMES from the Isabelle settings.\} With the \<^verbatim>\-a\ option, one may inspect the full process environment that Isabelle related programs are run in. This usually contains much more variables than are actually Isabelle settings. Normally, output is a list of lines of the form \name\\<^verbatim>\=\\value\. The \<^verbatim>\-b\ option causes only the values to be printed. Option \<^verbatim>\-d\ produces a dump of the complete environment to the specified file. Entries are terminated by the ASCII NUL character, i.e.\ the string terminator in C. Thus the Isabelle/Scala operation \<^scala_method>\isabelle.Isabelle_System.init\ can import the settings environment robustly, and provide its own \<^scala_method>\isabelle.Isabelle_System.getenv\ function. \ subsubsection \Examples\ text \ Get the location of @{setting ISABELLE_HOME_USER} where user-specific information is stored: @{verbatim [display] \isabelle getenv ISABELLE_HOME_USER\} \<^medskip> Get the value only of the same settings variable, which is particularly useful in shell scripts: @{verbatim [display] \isabelle getenv -b ISABELLE_HOME_USER\} \ section \Mercurial repository setup \label{sec:hg-setup}\ text \ The @{tool_def hg_setup} tool simplifies the setup of Mercurial repositories, with hosting via Phabricator (\chref{ch:phabricator}) or SSH file server access. @{verbatim [display] \Usage: isabelle hg_setup [OPTIONS] REMOTE LOCAL_DIR Options are: -n NAME remote repository name (default: base name of LOCAL_DIR) -p PATH Mercurial path name (default: "default") -r assume that remote repository already exists Setup a remote vs. local Mercurial repository: REMOTE either refers to a Phabricator server "user@host" or SSH file server "ssh://user@host/path".\} The \<^verbatim>\REMOTE\ repository specification \<^emph>\excludes\ the actual repository name: that is given by the base name of \<^verbatim>\LOCAL_DIR\, or via option \<^verbatim>\-n\. By default, both sides of the repository are created on demand by default. In contrast, option \<^verbatim>\-r\ assumes that the remote repository already exists: it avoids accidental creation of a persistent repository with unintended name. The local \<^verbatim>\.hg/hgrc\ file is changed to refer to the remote repository, usually via the symbolic path name ``\<^verbatim>\default\''; option \<^verbatim>\-p\ allows to provide a different name. \ subsubsection \Examples\ text \ Setup the current directory as a repository with Phabricator server hosting: @{verbatim [display] \ isabelle hg_setup vcs@vcs.example.org .\} \<^medskip> Setup the current directory as a repository with plain SSH server hosting: @{verbatim [display] \ isabelle hg_setup ssh://files.example.org/data/repositories .\} \<^medskip> Both variants require SSH access to the target server, via public key without password. \ section \Mercurial repository synchronization \label{sec:tool-hg-sync}\ text \ The @{tool_def hg_sync} tool synchronizes a local Mercurial repository with a target directory. @{verbatim [display] \Usage: isabelle hg_sync [OPTIONS] TARGET Options are: -F RULE add rsync filter RULE (e.g. "protect /foo" to avoid deletion) -P protect spaces in target file names: more robust, less portable -R ROOT explicit repository root directory (default: implicit from current directory) -S PATH SSH control path for connection multiplexing -T thorough treatment of file content and directory times -n no changes: dry-run -p PORT SSH port -r REV explicit revision (default: state of working directory) -v verbose Synchronize Mercurial repository with TARGET directory, which can be local or remote (using notation of rsync).\} The \<^verbatim>\TARGET\ specification can be a local or remote directory (via ssh), using \<^verbatim>\rsync\\<^footnote>\\<^url>\https://linux.die.net/man/1/rsync\\ notation for destinations; see also examples below. The content is written directly into the target, \<^emph>\without\ creating a separate sub-directory. The special sub-directory \<^verbatim>\.hg_sync\ within the target contains meta data from the original Mercurial repository. Repeated synchronization is guarded by the presence of a \<^verbatim>\.hg_sync\ sub-directory: this sanity check prevents accidental changes (or deletion!) of targets that were not created by @{tool hg_sync}. \<^medskip> Option \<^verbatim>\-r\ specifies an explicit revision of the repository; the default is the current state of the working directory (which might be uncommitted). \<^medskip> Option \<^verbatim>\-v\ enables verbose mode. Option \<^verbatim>\-n\ enables ``dry-run'' mode: operations are only simulated; use it with option \<^verbatim>\-v\ to actually see results. \<^medskip> Option \<^verbatim>\-F\ adds a filter rule to the underlying \<^verbatim>\rsync\ command; multiple \<^verbatim>\-F\ options may be given to accumulate a list of rules. \<^medskip> Option \<^verbatim>\-R\ specifies an explicit repository root directory. The default is to derive it from the current directory, searching upwards until a suitable \<^verbatim>\.hg\ directory is found. \<^medskip> Option \<^verbatim>\-T\ indicates thorough treatment of file content and directory times. The default is to consider files with equal time and size already as equal, and to ignore time stamps on directories. \<^medskip> Option \<^verbatim>\-p\ specifies an explicit port for the SSH connection underlying \<^verbatim>\rsync\; the default is taken from the user's \<^path>\ssh_config\ file. \<^medskip> Option \<^verbatim>\-S\ specifies the control path (Unix socket) to an existing SSH connection that supports multiplexing (\<^verbatim>\ssh -M -S\~\socket\). \<^medskip> Option \<^verbatim>\-P\ uses \<^verbatim>\rsync --protect-args\ to work robustly with spaces or special characters of the shell. This requires at least \<^verbatim>\rsync 3.0.0\, which is not always available --- notably on macOS. Assuming traditional Unix-style naming of files and directories, it is safe to omit this option for the sake of portability. \ subsubsection \Examples\ text \ Synchronize the current repository onto a remote host, with accurate treatment of all content: @{verbatim [display] \ isabelle hg_sync -T remotename:test/repos\} \ section \Installing standalone Isabelle executables \label{sec:tool-install}\ text \ By default, the main Isabelle binaries (@{executable "isabelle"} etc.) are just run from their location within the distribution directory, probably indirectly by the shell through its @{setting PATH}. Other schemes of installation are supported by the @{tool_def install} tool: @{verbatim [display] \Usage: isabelle install [OPTIONS] BINDIR Options are: -d DISTDIR refer to DISTDIR as Isabelle distribution (default ISABELLE_HOME) Install Isabelle executables with absolute references to the distribution directory.\} The \<^verbatim>\-d\ option overrides the current Isabelle distribution directory as determined by @{setting ISABELLE_HOME}. The \BINDIR\ argument tells where executable wrapper scripts for @{executable "isabelle"} and @{executable isabelle_scala_script} should be placed, which is typically a directory in the shell's @{setting PATH}, such as \<^verbatim>\$HOME/bin\. \<^medskip> It is also possible to make symbolic links of the main Isabelle executables manually, but making separate copies outside the Isabelle distribution directory will not work! \ section \Creating instances of the Isabelle logo\ text \ The @{tool_def logo} tool creates variants of the Isabelle logo, for inclusion in PDF{\LaTeX} documents. @{verbatim [display] \Usage: isabelle logo [OPTIONS] [NAME] Options are: -o FILE alternative output file -q quiet mode Create variant NAME of the Isabelle logo as "isabelle_name.pdf".\} Option \<^verbatim>\-o\ provides an alternative output file, instead of the default in the current directory: \<^verbatim>\isabelle_\\name\\<^verbatim>\.pdf\ with the lower-case version of the given name. \<^medskip> Option \<^verbatim>\-q\ omits printing of the resulting output file name. \<^medskip> Implementors of Isabelle tools and applications are encouraged to make derived Isabelle logos for their own projects using this template. The license is the same as for the regular Isabelle distribution (BSD). \ section \Output the version identifier of the Isabelle distribution\ text \ The @{tool_def version} tool displays Isabelle version information: @{verbatim [display] \Usage: isabelle version [OPTIONS] Options are: -i short identification (derived from Mercurial id) -t symbolic tags (derived from Mercurial id) Display Isabelle version information.\} \<^medskip> The default is to output the full version string of the Isabelle distribution, e.g.\ ``\<^verbatim>\Isabelle2022: October 2022\. \<^medskip> Option \<^verbatim>\-i\ produces a short identification derived from the Mercurial id of the @{setting ISABELLE_HOME} directory; option \<^verbatim>\-t\ prints version tags (if available). These options require either a repository clone or a repository archive (e.g. download of \<^url>\https://isabelle.sketis.net/repos/isabelle/archive/tip.tar.gz\). \ end diff --git a/src/Pure/Tools/build_docker.scala b/src/Pure/Tools/build_docker.scala --- a/src/Pure/Tools/build_docker.scala +++ b/src/Pure/Tools/build_docker.scala @@ -1,172 +1,172 @@ /* Title: Pure/Tools/build_docker.scala Author: Makarius Build docker image from Isabelle application bundle for Linux. */ package isabelle object Build_Docker { - private val default_base = "ubuntu" + private val default_base = "ubuntu:22.04" 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 val packages: List[String] = List("curl", "less", "libfontconfig1", "libgomp1", "openssh-client", "pwgen", "rsync", "unzip") val package_collections: Map[String, List[String]] = Map("X11" -> List("libx11-6", "libxext6", "libxrender1", "libxtst6", "libxi6"), "latex" -> List("texlive-fonts-extra", "texlive-font-utils", "texlive-latex-extra", "texlive-science")) def all_packages: List[String] = packages ::: package_collections.valuesIterator.flatten.toList 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, output: Option[Path] = None, more_packages: List[String] = Nil, tag: String = "", verbose: Boolean = false ): Unit = { val isabelle_name = app_archive match { case Isabelle_Name(name) => name case _ => error("Cannot determine Isabelle distribution name from " + app_archive) } val is_remote = Url.is_wellformed(app_archive) val dockerfile = """## Dockerfile for """ + isabelle_name + """ FROM """ + base + """ SHELL ["/bin/bash", "-c"] # packages ENV DEBIAN_FRONTEND=noninteractive RUN apt-get -y update && \ apt-get install -y """ + Bash.strings(packages ::: more_packages) + """ && \ apt-get clean # user RUN useradd -m isabelle && (echo isabelle:isabelle | chpasswd) USER isabelle # Isabelle WORKDIR /home/isabelle """ + (if (is_remote) "RUN curl --fail --silent " + Bash.string(app_archive) + " > Isabelle.tar.gz" else "COPY Isabelle.tar.gz .") + """ RUN tar xzf Isabelle.tar.gz && \ mv """ + isabelle_name + """ Isabelle && \ sed -i -e 's,ISABELLE_HOME_USER=.*,ISABELLE_HOME_USER="\$USER_HOME/.isabelle",g;' Isabelle/etc/settings && \ sed -i -e 's,ISABELLE_LOGIC=.*,ISABELLE_LOGIC=""" + logic + """,g;' Isabelle/etc/settings && \ Isabelle/bin/isabelle build -o system_heaps -b """ + logic + """ && \ rm Isabelle.tar.gz""" + (if (entrypoint) """ ENTRYPOINT ["Isabelle/bin/isabelle"] """ else "") for (path <- output) { progress.echo("Dockerfile: " + path.absolute) File.write(path, dockerfile) } if (!no_build) { Isabelle_System.make_directory(work_dir) progress.echo("Docker working directory: " + work_dir.absolute) Isabelle_System.with_tmp_dir("docker_build", base_dir = work_dir.file) { tmp_dir => progress.echo("Docker temporary directory: " + tmp_dir.absolute) 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")) } val quiet_option = if (verbose) "" else " -q" val tag_option = if (tag == "") "" else " -t " + Bash.string(tag) progress.bash("docker build" + quiet_option + tag_option + " " + File.bash_path(tmp_dir), echo = true).check } } } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build_docker", "build Isabelle docker image", Scala_Project.here, { 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 var more_packages: List[String] = Nil var verbose = false var tag = "" val getopts = Getopts(""" Usage: isabelle build_docker [OPTIONS] APP_ARCHIVE Options are: -B NAME base image (default """ + quote(default_base) + """) -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 -p NAME additional Ubuntu package -t TAG docker build tag -v verbose Build Isabelle docker image with default logic image, using a standard Isabelle application archive for Linux (local file or remote URL). """, "B:" -> (arg => base = arg), "E" -> (_ => entrypoint = true), "P:" -> (arg => package_collections.get(arg) match { 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))), "p:" -> (arg => more_packages ::= arg), "t:" -> (arg => tag = arg), "v" -> (_ => verbose = true)) val more_args = getopts(args) val app_archive = more_args match { case List(arg) => arg case _ => getopts.usage() } 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) }) }