diff --git a/.gitignore b/.gitignore
index d49e32744..50ead7d5e 100644
--- a/.gitignore
+++ b/.gitignore
@@ -3,6 +3,7 @@
 env
 .idea
 .vagrant*
+.toolchains/
 .vscode
 .yarn
 *.bkp
diff --git a/Vagrantfile b/Vagrantfile
index 5ad06e6a0..80b1724cd 100644
--- a/Vagrantfile
+++ b/Vagrantfile
@@ -1,6 +1,17 @@
 $frontend = <<-SHELL
   #!/bin/bash -eux
 
+  # Keep downloaded .deb files in a host-side cache, so a reprovision does not
+  # re-fetch them. Redirected rather than bind-mounted over
+  # /var/cache/apt/archives, so apt's lock and partial/ handling stays
+  # explicit. This must precede anything that runs apt, including the
+  # NodeSource setup script below.
+  mkdir -p /vagrant_cache/apt/partial
+  echo 'Dir::Cache::Archives "/vagrant_cache/apt";' > /etc/apt/apt.conf.d/99-learn-cache
+  # apt drops privileges to the _apt user to download, which cannot read a
+  # vboxsf share owned by vagrant; without this it warns on every invocation.
+  echo 'APT::Sandbox::User "root";' >> /etc/apt/apt.conf.d/99-learn-cache
+
   # Enable the NodeSource repository
   curl -sL https://deb.nodesource.com/setup_24.x | bash -
 
@@ -23,9 +34,15 @@ $frontend = <<-SHELL
       libjpeg-dev \
       make
 
-  # Install/check packages from list for reproducibility
-  DEBIAN_FRONTEND=noninteractive apt-get install \
-    --allow-downgrades -y $(cat /home/vagrant/vm_apt.txt)
+  # Install/check packages from list for reproducibility.
+  # Set VM_APT_PIN=0 to skip this step. That is needed when bootstrapping a
+  # new Ubuntu base box, whose archive does not carry the pinned versions.
+  if [ "${VM_APT_PIN:-1}" = "1" ]; then
+    DEBIAN_FRONTEND=noninteractive apt-get install \
+      --allow-downgrades -y $(cat /home/vagrant/vm_apt.txt)
+  else
+    echo "VM_APT_PIN=0 -- skipping installation of pinned packages"
+  fi
 
   # Force packages to be set as automatically installed
   apt-mark auto $(cat /vagrant/vm_apt_list.txt | grep "\\[installed,automatic\\]" | awk -F/ -v ORS=" " 'NR>1 {print $1}')
@@ -44,6 +61,30 @@ $frontend = <<-SHELL
   echo default_version_gnat:         $default_version_gnat
   echo toolchain_versions_gnat:      $toolchain_versions_gnat
 
+  # Toolchain download cache: fetch each tarball into the host-side folder
+  # mounted at /vagrant_cache/gnat, verified against its upstream .sha256.
+  # The script also runs on the host -- `vm_cache_gnat.sh fetch --all` warms
+  # the cache before `vagrant up`.
+  export LEARN_VM_CACHE_GNAT=/vagrant_cache/gnat
+  gnat_cache=/vagrant/frontend/vm/vm_cache_gnat.sh
+
+  install_toolchain () {
+    local tool=$1
+    local ver=$2
+    local tarball
+    local tmp
+
+    # Invoked via bash rather than directly: the repo has
+    # core.fileMode disabled and the script arrives over a vboxsf
+    # share, so the executable bit cannot be relied on here.
+    tarball=$(bash ${gnat_cache} fetch "${tool}" "${ver}")
+    # Extract on the VM's own disk, never onto the shared cache folder.
+    tmp=$(mktemp -d)
+    tar xzf "${tarball}" -C "${tmp}"
+    mv "${tmp}"/${tool}-* ${path_ada_toolchain_root}/${tool}/${ver}
+    rm -rf "${tmp}"
+  }
+
   # Install FSF GNAT
   # (Required tool: gnatchop)
   mkdir -p ${path_ada_toolchain_root}
@@ -54,10 +95,7 @@ $frontend = <<-SHELL
   mkdir ${path_ada_toolchain_root}/gnat
   for tool_version in ${gnat_version[@]}; do
     echo Installing GNAT $tool_version
-    wget -O gnat.tar.gz https://github.com/alire-project/GNAT-FSF-builds/releases/download/gnat-${tool_version}/gnat-x86_64-linux-${tool_version}.tar.gz && \
-    tar xzf gnat.tar.gz && \
-    mv gnat-* ${path_ada_toolchain_root}/gnat/${tool_version} && \
-    rm *.tar.gz
+    install_toolchain gnat ${tool_version}
   done
 
   ln -sf ${path_ada_toolchain_root}/gnat/${default_version_gnat}            ${path_ada_toolchain_default}/gnat
@@ -86,6 +124,17 @@ SHELL
 $epub = <<-SHELL
   #!/bin/bash -eux
 
+  # Keep downloaded .deb files in a host-side cache, so a reprovision does not
+  # re-fetch them. Redirected rather than bind-mounted over
+  # /var/cache/apt/archives, so apt's lock and partial/ handling stays
+  # explicit. This must precede anything that runs apt, including the
+  # NodeSource setup script below.
+  mkdir -p /vagrant_cache/apt/partial
+  echo 'Dir::Cache::Archives "/vagrant_cache/apt";' > /etc/apt/apt.conf.d/99-learn-cache
+  # apt drops privileges to the _apt user to download, which cannot read a
+  # vboxsf share owned by vagrant; without this it warns on every invocation.
+  echo 'APT::Sandbox::User "root";' >> /etc/apt/apt.conf.d/99-learn-cache
+
   # Enable the NodeSource repository
   curl -sL https://deb.nodesource.com/setup_22.x | bash -
 
@@ -127,9 +176,15 @@ $epub = <<-SHELL
       wget \
       libc6-dev
 
-  # Install/check packages from list for reproducibility
-  DEBIAN_FRONTEND=noninteractive apt-get install \
-    --allow-downgrades -y $(cat /home/vagrant/vm_apt.txt)
+  # Install/check packages from list for reproducibility.
+  # Set VM_APT_PIN=0 to skip this step. That is needed when bootstrapping a
+  # new Ubuntu base box, whose archive does not carry the pinned versions.
+  if [ "${VM_APT_PIN:-1}" = "1" ]; then
+    DEBIAN_FRONTEND=noninteractive apt-get install \
+      --allow-downgrades -y $(cat /home/vagrant/vm_apt.txt)
+  else
+    echo "VM_APT_PIN=0 -- skipping installation of pinned packages"
+  fi
 
   # Force packages to be set as automatically installed
   apt-mark auto $(cat /vagrant/vm_apt_list.txt | grep "\\[installed,automatic\\]" | awk -F/ -v ORS=" " 'NR>1 {print $1}')
@@ -156,6 +211,30 @@ $epub = <<-SHELL
   echo toolchain_versions_gnatprove  $toolchain_versions_gnatprove
   echo toolchain_versions_gprbuild   $toolchain_versions_gprbuild
 
+  # Toolchain download cache: fetch each tarball into the host-side folder
+  # mounted at /vagrant_cache/gnat, verified against its upstream .sha256.
+  # The script also runs on the host -- `vm_cache_gnat.sh fetch --all` warms
+  # the cache before `vagrant up`.
+  export LEARN_VM_CACHE_GNAT=/vagrant_cache/gnat
+  gnat_cache=/vagrant/frontend/vm/vm_cache_gnat.sh
+
+  install_toolchain () {
+    local tool=$1
+    local ver=$2
+    local tarball
+    local tmp
+
+    # Invoked via bash rather than directly: the repo has
+    # core.fileMode disabled and the script arrives over a vboxsf
+    # share, so the executable bit cannot be relied on here.
+    tarball=$(bash ${gnat_cache} fetch "${tool}" "${ver}")
+    # Extract on the VM's own disk, never onto the shared cache folder.
+    tmp=$(mktemp -d)
+    tar xzf "${tarball}" -C "${tmp}"
+    mv "${tmp}"/${tool}-* ${path_ada_toolchain_root}/${tool}/${ver}
+    rm -rf "${tmp}"
+  }
+
   # Install FSF GNAT
   mkdir -p ${path_ada_toolchain_root}
   mkdir -p ${path_ada_toolchain_default}
@@ -165,30 +244,21 @@ $epub = <<-SHELL
   mkdir ${path_ada_toolchain_root}/gnat
   for tool_version in ${gnat_version[@]}; do
     echo Installing GNAT $tool_version
-    wget -O gnat.tar.gz https://github.com/alire-project/GNAT-FSF-builds/releases/download/gnat-${tool_version}/gnat-x86_64-linux-${tool_version}.tar.gz && \
-    tar xzf gnat.tar.gz && \
-    mv gnat-* ${path_ada_toolchain_root}/gnat/${tool_version} && \
-    rm *.tar.gz
+    install_toolchain gnat ${tool_version}
   done
 
   gnat_prove_version=(${toolchain_versions_gnatprove})
   mkdir ${path_ada_toolchain_root}/gnatprove
   for tool_version in ${gnat_prove_version[@]}; do
     echo Installing GNATprove $tool_version
-    wget -O gnatprove.tar.gz https://github.com/alire-project/GNAT-FSF-builds/releases/download/gnatprove-${tool_version}/gnatprove-x86_64-linux-${tool_version}.tar.gz && \
-    tar xzf gnatprove.tar.gz && \
-    mv gnatprove-* ${path_ada_toolchain_root}/gnatprove/${tool_version} && \
-    rm *.tar.gz
+    install_toolchain gnatprove ${tool_version}
   done
 
   gprbuild_version=(${toolchain_versions_gprbuild})
   mkdir ${path_ada_toolchain_root}/gprbuild
   for tool_version in ${gprbuild_version[@]}; do
     echo Installing GPRbuild $tool_version
-    wget -O gprbuild.tar.gz https://github.com/alire-project/GNAT-FSF-builds/releases/download/gprbuild-${tool_version}/gprbuild-x86_64-linux-${tool_version}.tar.gz && \
-    tar xzf gprbuild.tar.gz && \
-    mv gprbuild-* ${path_ada_toolchain_root}/gprbuild/${tool_version} && \
-    rm *.tar.gz
+    install_toolchain gprbuild ${tool_version}
   done
 
   rm -f ${path_ada_toolchain_default}/*
@@ -218,6 +288,58 @@ $epub = <<-SHELL
 
 SHELL
 
+require 'fileutils'
+
+# Installation of the pinned package versions is enabled by default.
+# Set VM_APT_PIN=0 to disable it for a base-box bootstrap.
+vm_apt_pin = ENV.fetch("VM_APT_PIN", "1")
+
+# Several checkouts of this repository can run their own web/epub VMs at the
+# same time: VirtualBox names each VM after its directory, and the ports below
+# can be moved out of one another's way.
+
+# Host port for the web VM's dev server (guest 8080). Override it to run more
+# than one web VM at once. auto_correct still picks a free port if this one is
+# taken too -- `vagrant port web` then reports what was chosen.
+web_port = Integer(ENV.fetch("LEARN_WEB_PORT", "8080"))
+
+# SSH host ports. Vagrant forwards SSH under the reserved id "ssh", so
+# redeclaring that id overrides its default rather than adding a second rule.
+# The defaults reproduce what Vagrant picks unaided for a single checkout:
+# 2222 for the first machine, and 2200 -- the base of the auto-correct range
+# -- for the second. Pinning them keeps the numbers predictable when several
+# checkouts run at once.
+#
+# auto_correct stays on, so a clash degrades to a warning rather than a
+# refusal to boot. These are therefore a preference, not a guarantee:
+# `vagrant ssh-config <machine>` remains authoritative, and anything scripted
+# should ask rather than assume.
+web_ssh_port  = Integer(ENV.fetch("LEARN_WEB_SSH_PORT",  "2222"))
+epub_ssh_port = Integer(ENV.fetch("LEARN_EPUB_SSH_PORT", "2200"))
+
+# Host-side download cache for the GNAT-FSF toolchain tarballs, so that
+# destroying a VM does not throw them away. Redirect it with
+# LEARN_VM_CACHE_GNAT -- it holds several GB and may belong on another disk.
+vm_cache_gnat = File.expand_path(
+  ENV.fetch("LEARN_VM_CACHE_GNAT", ".toolchains/gnat"), __dir__)
+
+# Host-side apt archive, shared by both VMs. Redirect it with
+# LEARN_VM_CACHE_APT.
+vm_cache_apt = File.expand_path(
+  ENV.fetch("LEARN_VM_CACHE_APT", ".toolchains/apt"), __dir__)
+
+# Expanded against this file's directory, so that a relative override still
+# names one place: the helper scripts in frontend/vm/ resolve it the same way.
+#
+# Vagrant refuses to start if a synced folder's source does not exist, so the
+# cache directories have to be created before they are declared below.
+[vm_cache_gnat, vm_cache_apt].each { |d| FileUtils.mkdir_p(d) }
+
+# The download caches are shared between checkouts, so a temporary file there
+# has to name the checkout as well as the machine: two "web" VMs would
+# otherwise write to the same .part file.
+project = File.basename(__dir__)
+
 Vagrant.configure("2") do |config|
 
   config.vm.provider "virtualbox" do |vb|
@@ -229,26 +351,39 @@ Vagrant.configure("2") do |config|
   config.vm.define "web" do |web|
     web.vm.box = "bento/ubuntu-24.04"
     web.vm.box_version = "202510.26.0"
-    web.vm.network "forwarded_port", guest: 8080, host: 8080, host_ip: "127.0.0.1"
+    web.vm.network "forwarded_port", guest: 8080, host: web_port,
+                   host_ip: "127.0.0.1", auto_correct: true
+    web.vm.network "forwarded_port", guest: 22, host: web_ssh_port,
+                   id: "ssh", auto_correct: true
 
     web.vm.synced_folder './frontend', '/vagrant/frontend'
     web.vm.synced_folder './content', '/vagrant/content'
+    web.vm.synced_folder vm_cache_gnat, '/vagrant_cache/gnat'
+    web.vm.synced_folder vm_cache_apt,  '/vagrant_cache/apt'
 
     web.vm.provision "file", source: "./frontend/python/rst_code_example_pipeline/src/rst_code_example_pipeline/data/toolchain.ini", destination: "/home/vagrant/toolchain.ini"
-    web.vm.provision "file", source: "./frontend/vm_apt_web.txt", destination: "/home/vagrant/vm_apt.txt"
-    web.vm.provision :shell, inline: $frontend
+    web.vm.provision "file", source: "./frontend/vm/vm_apt_web.txt", destination: "/home/vagrant/vm_apt.txt"
+    web.vm.provision :shell, inline: $frontend,
+                     env: { "VM_APT_PIN" => vm_apt_pin,
+                            "LEARN_VM_NAME" => "#{project}-web" }
   end
 
   config.vm.define "epub" do |epub|
     epub.vm.box = "bento/ubuntu-24.04"
     epub.vm.box_version = "202510.26.0"
+    epub.vm.network "forwarded_port", guest: 22, host: epub_ssh_port,
+                    id: "ssh", auto_correct: true
 
     epub.vm.synced_folder './frontend', '/vagrant/frontend'
     epub.vm.synced_folder './content', '/vagrant/content'
+    epub.vm.synced_folder vm_cache_gnat, '/vagrant_cache/gnat'
+    epub.vm.synced_folder vm_cache_apt,  '/vagrant_cache/apt'
 
     epub.vm.provision "file", source: "./frontend/python/rst_code_example_pipeline/src/rst_code_example_pipeline/data/toolchain.ini", destination: "/home/vagrant/toolchain.ini"
-    epub.vm.provision "file", source: "./frontend/vm_apt_epub.txt", destination: "/home/vagrant/vm_apt.txt"
-    epub.vm.provision :shell, inline: $epub
+    epub.vm.provision "file", source: "./frontend/vm/vm_apt_epub.txt", destination: "/home/vagrant/vm_apt.txt"
+    epub.vm.provision :shell, inline: $epub,
+                      env: { "VM_APT_PIN" => vm_apt_pin,
+                             "LEARN_VM_NAME" => "#{project}-epub" }
   end
 
 end
diff --git a/frontend/vm/README.md b/frontend/vm/README.md
new file mode 100644
index 000000000..57d68257b
--- /dev/null
+++ b/frontend/vm/README.md
@@ -0,0 +1,286 @@
+# Vagrant VM: How to
+
+This file provides more details about setting up the Vagrant VMs for this
+repository. It covers:
+
+- what `vagrant up` actually installs, and how to connect to each VM
+- how to run the VMs of several checkouts side by side
+- how to avoid re-downloading several GB every time a VM is rebuilt
+- what the pinned package lists are, and how to update them
+- how to bring up a VM on a new Ubuntu base box
+
+Everything here is optional, though. A simple `vagrant up` should be
+sufficient.
+
+## Bringing up the VMs
+
+To create both VMs and install everything they need, run:
+
+```
+$ vagrant up
+```
+
+This creates two VMs and provisions each of them. Provisioning installs the
+apt packages, the Node.js release from NodeSource, the Ada toolchains listed
+in `toolchain.ini` (into `/opt/ada`), a Python virtual environment at
+`/vagrant/venv`, and the frontend's npm dependencies.
+
+The two VMs get different toolchains: `web` installs every GNAT version,
+since it only needs `gnatchop`, while `epub` also installs GNATprove and
+GPRbuild because it builds and runs the course examples.
+
+Expect the first run to take a while: the toolchains alone are over 2 GB.
+The section on caching below removes that cost from every later run.
+
+To bring up just one of them:
+
+```
+$ vagrant up web
+$ vagrant up epub
+```
+
+## Connecting
+
+Once the VMs are up, open a shell on either of them with:
+
+```
+$ vagrant ssh web
+$ vagrant ssh epub
+```
+
+Inside either VM, the checkout is mounted at `/vagrant`: `frontend/` and
+`content/` are the live directories from your host, so edits on either side
+are visible immediately.
+
+The Ada toolchain is on the `PATH` of a login shell. A command run
+non-interactively does not read `~/.profile`, so use a login shell when you
+need the toolchain:
+
+```
+$ vagrant ssh epub -c "bash -lc 'gnatchop --version'"
+```
+
+## Running several checkouts at the same time
+
+If you have more than one checkout of this repository, each can have its own
+pair of VMs. VirtualBox names each VM after the directory it was created in,
+so they do not clash — but the host ports do, and `vagrant up` fails with
+"Vagrant cannot forward the specified ports on this VM".
+
+Give the second checkout its own ports:
+
+```
+$ export LEARN_WEB_PORT=8081
+$ export LEARN_WEB_SSH_PORT=2232
+$ export LEARN_EPUB_SSH_PORT=2230
+$ vagrant up
+```
+
+| Variable | Default | Effect |
+|---|---|---|
+| `LEARN_WEB_PORT` | `8080` | Host port for the `web` development server |
+| `LEARN_WEB_SSH_PORT` | `2222` | Host port for SSH to `web` |
+| `LEARN_EPUB_SSH_PORT` | `2200` | Host port for SSH to `epub` |
+
+Set them in the shell you use for that checkout, so that every later
+`vagrant` command in it agrees.
+
+These are a preference, not a guarantee: if a port you ask for is also taken,
+Vagrant moves it and warns rather than failing. To see what a machine ended
+up with:
+
+```
+$ vagrant port web
+$ vagrant ssh-config web
+```
+
+`vagrant ssh` always connects correctly, so prefer it over a hard-coded port.
+
+## Avoiding repeated downloads
+
+Destroying a VM throws away everything provisioning downloaded. To avoid
+paying for that twice, the Ada toolchain tarballs and the `.deb` files are
+kept on the host instead, in directories mounted into both VMs.
+
+Nothing needs to be configured for this — the caches fill themselves on the
+first `vagrant up` and are reused from then on. The defaults live in
+`.toolchains/` inside the checkout and are gitignored:
+
+| Variable | Default | Holds |
+|---|---|---|
+| `LEARN_VM_CACHE_GNAT` | `.toolchains/gnat` | Ada toolchain tarballs and their checksums |
+| `LEARN_VM_CACHE_APT` | `.toolchains/apt` | Downloaded `.deb` files |
+
+Because the default is inside the checkout, a second checkout starts with an
+empty cache. To share one set of downloads between them, point both variables
+somewhere outside. For example:
+
+```
+$ export LEARN_VM_CACHE_GNAT=~/vm-cache/gnat
+$ export LEARN_VM_CACHE_APT=~/vm-cache/apt
+```
+
+Use absolute paths. A relative one is resolved against the repository root,
+not your current directory.
+
+### Filling the cache in advance
+
+You can download the toolchains before creating any VM, so that provisioning
+fetches nothing. This runs on the host:
+
+```
+$ frontend/vm/vm_cache_gnat.sh fetch --all
+```
+
+This is useful when you expect to rebuild a VM several times, or want the
+download out of the way before going offline. To fetch a single version:
+
+```
+$ frontend/vm/vm_cache_gnat.sh fetch gnat 15.1.0-2
+```
+
+Each tarball is checked against the SHA-256 published alongside it upstream,
+every time it is used rather than only when downloaded, so a truncated or
+damaged file is replaced automatically instead of breaking a later build.
+
+### Checking and cleaning up
+
+To see what the caches currently hold, run:
+
+```
+$ frontend/vm/vm_cache_report.sh
+```
+
+This shows where each cache is, how large it is, and which of its entries
+are no longer required. Both caches accumulate those on their own: the
+toolchain cache keeps tarballs whose version has been dropped from
+`toolchain.ini`, and the apt cache keeps package files superseded by a
+later capture of the pinned lists.
+
+To get rid of those leftovers, run:
+
+```
+$ frontend/vm/vm_cache_clean.sh             # shows what it would remove
+$ frontend/vm/vm_cache_clean.sh --delete    # removes it
+```
+
+The first form changes nothing, so it is safe to run to see the list.
+
+One caveat for the apt cache: a package file counts as required only if one
+of the pinned lists names it. Immediately after a bootstrap with
+`VM_APT_PIN=0`, or after upgrading a VM in place, the lists do not yet
+describe the VM, so almost the whole cache is reported as removable. The
+report prints a warning whenever most of the cache is no longer required.
+Nothing breaks if you delete anyway — provisioning only installs what the
+lists name, so it never asks for a file that was removed — but the next
+`vagrant up` re-downloads what it needs. Therefore, regenerate the lists
+first, so that the cache remains useful.
+
+Both commands are entry points covering every cache. The work is done by one
+script per cache — `vm_cache_gnat.sh` and `vm_cache_apt.sh` — which can be
+run directly when you only care about one of them:
+
+```
+$ frontend/vm/vm_cache_gnat.sh report
+$ frontend/vm/vm_cache_apt.sh clean --delete
+```
+
+## The pinned package lists
+
+Both VMs run Ubuntu, so their system software is installed with `apt`, the
+package manager Debian and Ubuntu share. Left to itself, `apt` installs
+whichever version of a package the Ubuntu archive happens to offer on the day
+you ask for it, which means two people running `vagrant up` a month apart get
+two different machines.
+
+To avoid that, this directory keeps a record of the apt packages each VM
+should have: `vm_apt_web.txt` and `vm_apt_epub.txt`, one file per VM, listing
+one `package=version` per line. Provisioning installs exactly those versions,
+so a `vagrant up` reproduces a known machine rather than today's archive.
+
+That matters because these VMs produce published artifacts. A new texlive or
+font package can change the PDFs without anything failing, and the difference
+would only show up when someone compared a course against an earlier release.
+
+Provisioning passes `--allow-downgrades` deliberately: if a package on the VM
+is newer than the pinned version, it is moved *back*. The pinned versions are
+expected to lag the archive, and that is the point.
+
+### Updating the packages in a VM
+
+Upgrading is a deliberate step, not something that happens on its own. Bring
+the VMs up, upgrade in place, and check the result before recording it:
+
+```
+$ vagrant ssh epub
+$ sudo apt update && sudo apt full-upgrade
+```
+
+Then build the content and confirm the output is still correct — at minimum a
+successful `make site`, and a generated course PDF compared against the
+published one. Only then record the new state, from the host:
+
+```
+$ frontend/vm/vm_apt_capture.sh epub
+$ frontend/vm/vm_apt_capture.sh          # or both VMs at once
+```
+
+This rewrites the lists in place. Read the diff before committing it: the
+snapshot freezes whatever is installed at that moment — including anything
+you installed by hand while debugging — and every later `vagrant up` will
+then demand it.
+
+## Bringing up a new Ubuntu base box
+
+Moving the VMs to a newer Ubuntu release has one complication: the pinned
+lists name versions that the new release's archive has never carried, so
+provisioning aborts before it can get far enough to record new ones. The
+first run therefore has to be made without pinning:
+
+| Variable | Default | Effect |
+|---|---|---|
+| `VM_APT_PIN` | `1` | Set to `0` to skip installing the pinned versions |
+
+The full sequence is:
+
+1. Set the new box and version in the `Vagrantfile`. Both the `web` and the
+   `epub` block need it:
+
+   ```ruby
+   web.vm.box = "bento/ubuntu-<release>"
+   web.vm.box_version = "<version>"
+   ```
+
+2. Rebuild the VMs with pinning switched off:
+
+   ```
+   $ vagrant destroy -f
+   $ VM_APT_PIN=0 vagrant up
+   ```
+
+   Expect to iterate here. A new Ubuntu release is where renamed or dropped
+   packages turn up, and the failure will be in the package list in the
+   `Vagrantfile` rather than in the pinned lists, which are switched off.
+
+3. Verify the result, as when updating packages: a successful build on both
+   VMs, and a generated course PDF compared against the published one.
+
+4. Record the new package set:
+
+   ```
+   $ frontend/vm/vm_apt_capture.sh
+   ```
+
+5. Rebuild once more, this time *with* pinning, to confirm the new lists
+   install cleanly from scratch:
+
+   ```
+   $ vagrant destroy -f
+   $ vagrant up
+   ```
+
+   This step is not optional: a list that cannot be replayed is worse than no
+   list, because it will only fail for the next person.
+
+6. Commit the captured lists together with the `box_version` change. On their
+   own, neither half describes a working configuration.
diff --git a/frontend/vm/vm_apt_capture.sh b/frontend/vm/vm_apt_capture.sh
new file mode 100755
index 000000000..6101722d2
--- /dev/null
+++ b/frontend/vm/vm_apt_capture.sh
@@ -0,0 +1,72 @@
+#!/bin/bash -eu
+#
+# Capture the apt package set of a provisioned VM into its pin list.
+#
+# The pin lists (vm_apt_web.txt, vm_apt_epub.txt) record the exact package
+# versions of a VM whose output has been verified, so that a later
+# `vagrant up` reproduces that machine rather than whatever the archive
+# serves on the day. This script is how a new snapshot is taken.
+#
+# Run it on the host, from the working copy the VMs were created in.
+# Only snapshot a VM that has been provisioned and whose build output has
+# been checked: whatever is installed at that moment is frozen into the
+# list and demanded of every future provision.
+#
+# Usage:
+#   frontend/vm/vm_apt_capture.sh web
+#   frontend/vm/vm_apt_capture.sh epub
+#   frontend/vm/vm_apt_capture.sh            # both
+
+set -o pipefail
+
+here=$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)
+repo=$(cd "${here}/../.." && pwd)
+
+# The one thing this script exists to record. `${binary:Package}` keeps the
+# `:arch` suffix that multi-arch packages carry (bind9-libs:amd64) and omits
+# it elsewhere, which is the format `apt-get install` expects back.
+dpkg_format='${binary:Package}=${Version}\n'
+
+capture () {
+  local vm=$1
+  local out="${repo}/frontend/vm/vm_apt_${vm}.txt"
+  local tmp="${out}.new"
+  local rc=0
+
+  echo "Capturing package set of the '${vm}' VM ..."
+
+  # Go through `vagrant ssh` rather than a hardcoded port/key, so the script
+  # keeps working if the forwarded ports move.
+  #
+  # `|| rc=$?` matters: the redirection below creates ${tmp} before the
+  # command runs, so letting `set -e` abort here would leave an empty file
+  # behind. Capture the status instead and clean up explicitly.
+  ( cd "${repo}" \
+      && vagrant ssh "${vm}" -c "dpkg-query -W -f='${dpkg_format}'" -- -T ) \
+    > "${tmp}" || rc=$?
+
+  if [ "${rc}" -ne 0 ] || [ ! -s "${tmp}" ]; then
+    rm -f "${tmp}"
+    echo "error: could not capture the package set of '${vm}'" \
+         "(exit ${rc}); '${out}' left unchanged" >&2
+    return 1
+  fi
+
+  mv "${tmp}" "${out}"
+  echo "  -> frontend/vm/vm_apt_${vm}.txt ($(wc -l < "${out}") packages)"
+}
+
+vms=("$@")
+if [ ${#vms[@]} -eq 0 ]; then
+  vms=(web epub)
+fi
+
+for vm in "${vms[@]}"; do
+  capture "${vm}"
+done
+
+cat <<'EOF'
+
+Review the diff before committing it. The snapshot freezes whatever is
+installed right now, including anything installed by hand while debugging.
+EOF
diff --git a/frontend/vm_apt_epub.txt b/frontend/vm/vm_apt_epub.txt
similarity index 100%
rename from frontend/vm_apt_epub.txt
rename to frontend/vm/vm_apt_epub.txt
diff --git a/frontend/vm_apt_web.txt b/frontend/vm/vm_apt_web.txt
similarity index 100%
rename from frontend/vm_apt_web.txt
rename to frontend/vm/vm_apt_web.txt
diff --git a/frontend/vm/vm_cache_apt.sh b/frontend/vm/vm_cache_apt.sh
new file mode 100755
index 000000000..8e1d8886e
--- /dev/null
+++ b/frontend/vm/vm_cache_apt.sh
@@ -0,0 +1,184 @@
+#!/bin/bash
+#
+# Operate on the cache of apt package files.
+#
+# Reports the contents of the cache, identifies entries that are no longer
+# required, and removes them.
+#
+# The cache holds the .deb files apt downloaded during provisioning, so that
+# rebuilding a VM does not fetch them again. Both VMs use the same cache.
+#
+# An entry is no longer required when its package and version appear in
+# neither vm_apt_web.txt nor vm_apt_epub.txt. Those are the same lists the
+# provisioner installs from, so the two cannot diverge. A .deb file is named
+# <package>_<version>_<architecture>.deb, with the epoch separator of a
+# version encoded as %3a.
+#
+# Note that the lists only describe a VM provisioned with package pinning
+# enabled. After a bootstrap with VM_APT_PIN=0, or after upgrading a VM in
+# place, the cache legitimately holds versions no list mentions yet; capture
+# the lists first, otherwise those entries are reported as no longer required.
+#
+# Invoked by vm_cache_report.sh and vm_cache_clean.sh. May also be invoked
+# directly to operate on this cache alone.
+#
+# Usage:
+#   vm_cache_apt.sh summary          # one line for the caches table
+#   vm_cache_apt.sh report           # contents and entries to remove
+#   vm_cache_apt.sh orphans          # their paths, one per line
+#   vm_cache_apt.sh clean            # dry run -- what would be removed
+#   vm_cache_apt.sh clean --delete   # remove it
+#
+# Environment:
+#   LEARN_VM_CACHE_APT   cache directory (default: <repo>/.toolchains/apt)
+
+set -eu
+set -o pipefail
+
+here=$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)
+repo=$(cd "${here}/../.." && pwd)
+
+pin_lists=("${here}/vm_apt_web.txt" "${here}/vm_apt_epub.txt")
+
+# Expand a cache location against the repository root, matching how the
+# Vagrantfile expands it against its own directory. An absolute value is used
+# as-is; a relative one must not depend on the caller's working directory.
+abspath () {
+  case "$1" in
+    /*) echo "$1" ;;
+    *)  echo "${repo}/$1" ;;
+  esac
+}
+
+cache=$(abspath "${LEARN_VM_CACHE_APT:-.toolchains/apt}")
+
+size_of () {
+  if [ -d "$1" ]; then du -sh "$1" 2>/dev/null | cut -f1; else echo "-"; fi
+}
+
+require_lists () {
+  local f
+  for f in "${pin_lists[@]}"; do
+    if [ ! -f "${f}" ]; then
+      echo "error: ${f} not found" >&2
+      exit 1
+    fi
+  done
+}
+
+# "<package> <version>" for every entry of both pin lists. The architecture
+# qualifier a multi-arch entry carries (bind9-libs:amd64=...) is dropped: the
+# same package and version may be cached as _amd64.deb or _all.deb.
+wanted_pairs () {
+  cat "${pin_lists[@]}" \
+    | sed -e 's/:[a-z0-9][a-z0-9-]*=/=/' -e 's/=/ /' \
+    | LC_ALL=C sort -u
+}
+
+# "<package> <version>" for every .deb in the cache. Only regular files
+# directly in the directory are considered: apt also keeps `lock`, `partial/`
+# and `apt/` there, which are not ours to touch.
+present_pairs () {
+  [ -d "${cache}" ] || return 0
+  find "${cache}" -maxdepth 1 -type f -name '*.deb' -printf '%f\n' 2>/dev/null \
+    | sed 's/\.deb$//' \
+    | awk -F_ '{ gsub(/%3a/, ":", $2); print $1, $2 }' \
+    | LC_ALL=C sort -u
+}
+
+# Paths of the .deb files whose package and version are in neither list.
+orphans () {
+  [ -d "${cache}" ] || return 0
+  local stale
+  # LC_ALL=C throughout: comm compares byte-wise, so both inputs must be
+  # sorted the same way.
+  stale=$(LC_ALL=C comm -13 <(wanted_pairs) <(present_pairs))
+  [ -n "${stale}" ] || return 0
+  # Map each stale pair back to the file carrying it. A version in a filename
+  # has its epoch separator encoded, so encode before matching.
+  echo "${stale}" | while read -r pkg ver; do
+    find "${cache}" -maxdepth 1 -type f \
+         -name "${pkg}_${ver//:/%3a}_*.deb" -print 2>/dev/null
+  done
+}
+
+do_summary () {
+  printf '%-8s %-8s %s\n' "apt" "$(size_of "${cache}")" "${cache}"
+}
+
+do_report () {
+  require_lists
+  local total stale_list stale_count f
+
+  if [ ! -d "${cache}" ]; then
+    echo "Package files present: (cache directory does not exist yet)"
+    return 0
+  fi
+
+  total=$(find "${cache}" -maxdepth 1 -type f -name '*.deb' 2>/dev/null | wc -l)
+  stale_list=$(orphans)
+  stale_count=$([ -z "${stale_list}" ] && echo 0 || echo "${stale_list}" | wc -l)
+
+  echo "Package files present: ${total}"
+  echo "Required by the pinned lists: $((total - stale_count))"
+
+  echo
+  if [ "${stale_count}" -eq 0 ]; then
+    echo "No entries to remove."
+    return 0
+  fi
+
+  echo "Entries no longer required (in neither pinned list):"
+  echo "${stale_list}" | while read -r f; do
+    printf '  %-8s %s\n' "$(du -h "${f}" 2>/dev/null | cut -f1)" "${f##*/}"
+  done
+
+  if [ "${stale_count}" -gt $((total - stale_count)) ]; then
+    echo
+    echo "Most of the cache is reported as no longer required, which suggests"
+    echo "the pinned lists do not describe the VMs the cache was filled from."
+    echo "Capture the lists before removing anything."
+  fi
+
+  echo
+  echo "Remove them with: frontend/vm/vm_cache_clean.sh --delete"
+}
+
+do_clean () {
+  require_lists
+  local delete=$1
+  local list count f
+
+  list=$(orphans)
+  if [ -z "${list}" ]; then
+    echo "No apt cache entries to remove."
+    return 0
+  fi
+  count=$(echo "${list}" | wc -l)
+
+  if [ "${delete}" = true ]; then
+    echo "${list}" | while read -r f; do
+      echo "removing ${f}"
+      rm -f "${f}"
+    done
+    echo "Removed ${count} package file$([ "${count}" -eq 1 ] || echo s)."
+  else
+    echo "Would remove ${count} package file$([ "${count}" -eq 1 ] || echo s):"
+    echo "${list}" | while read -r f; do
+      printf '  %-8s %s\n' "$(du -h "${f}" 2>/dev/null | cut -f1)" "${f}"
+    done
+    echo
+    echo "This was a dry run. Re-run with --delete to remove them."
+  fi
+}
+
+case "${1:-}" in
+  summary)  do_summary ;;
+  report)   do_report ;;
+  orphans)  orphans ;;
+  clean)    do_clean "$([ "${2:-}" = "--delete" ] && echo true || echo false)" ;;
+  -h|--help|"")
+    sed -n '3,34p' "${BASH_SOURCE[0]}" | sed 's/^# \{0,1\}//'; exit 0 ;;
+  *)
+    echo "error: unknown command '$1'" >&2; exit 1 ;;
+esac
diff --git a/frontend/vm/vm_cache_clean.sh b/frontend/vm/vm_cache_clean.sh
new file mode 100755
index 000000000..cf0107d0d
--- /dev/null
+++ b/frontend/vm/vm_cache_clean.sh
@@ -0,0 +1,41 @@
+#!/bin/bash
+#
+# Remove entries that are no longer required from the VM download caches.
+#
+# The caches are handled by one script each: vm_cache_gnat.sh and
+# vm_cache_apt.sh, which define what makes an entry no longer required and
+# may also be invoked directly.
+#
+# Defaults to a dry run. The cache directories are configurable and may be
+# located anywhere on the host, so removal must be requested explicitly.
+#
+# Usage:
+#   vm_cache_clean.sh            # dry run -- show what would be removed
+#   vm_cache_clean.sh --delete   # actually remove it
+#
+# Environment:
+#   LEARN_VM_CACHE_GNAT / _APT   override the cache locations
+#   (defaults: <repo>/.toolchains/{gnat,apt})
+
+set -eu
+set -o pipefail
+
+here=$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)
+gnat="${here}/vm_cache_gnat.sh"
+apt="${here}/vm_cache_apt.sh"
+
+args=()
+case "${1:-}" in
+  --delete)        args=(clean --delete) ;;
+  -n|--dry-run|"") args=(clean) ;;
+  -h|--help)       sed -n '3,18p' "${BASH_SOURCE[0]}" | sed 's/^# \{0,1\}//'; exit 0 ;;
+  *)               echo "error: unknown option '$1'" >&2; exit 1 ;;
+esac
+
+# Each cache is processed even if another fails, so that one broken cache
+# does not leave the rest uncleaned. The worst status is returned.
+rc=0
+"${gnat}" "${args[@]}" || rc=$?
+echo
+"${apt}" "${args[@]}" || rc=$?
+exit "${rc}"
diff --git a/frontend/vm/vm_cache_gnat.sh b/frontend/vm/vm_cache_gnat.sh
new file mode 100755
index 000000000..6e534f62b
--- /dev/null
+++ b/frontend/vm/vm_cache_gnat.sh
@@ -0,0 +1,168 @@
+#!/bin/bash
+#
+# Operate on the cache of GNAT toolchain tarballs.
+#
+# Downloads toolchain tarballs into the cache, reports its contents,
+# identifies entries that are no longer required, and removes them.
+#
+# An entry is no longer required when its version is not listed in
+# toolchain.ini, or when it is a .part file left behind by an interrupted
+# download. The list of required versions is read from the same toolchain.ini
+# the provisioner reads, so the two cannot diverge.
+#
+# Invoked by vm_cache_report.sh and vm_cache_clean.sh. May also be invoked
+# directly to operate on this cache alone.
+#
+# Usage:
+#   vm_cache_gnat.sh fetch <tool> <version>
+#                                     # download one toolchain into the cache
+#   vm_cache_gnat.sh fetch --all      # download every version in toolchain.ini
+#   vm_cache_gnat.sh summary          # one line for the caches table
+#   vm_cache_gnat.sh report           # versions, contents and orphans
+#   vm_cache_gnat.sh orphans          # orphan paths, one per line
+#   vm_cache_gnat.sh clean            # dry run -- what would be removed
+#   vm_cache_gnat.sh clean --delete   # remove it
+#
+# Environment:
+#   LEARN_VM_CACHE_GNAT   cache directory (default: <repo>/.toolchains/gnat)
+
+set -eu
+set -o pipefail
+
+here=$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)
+repo=$(cd "${here}/../.." && pwd)
+
+toolchain_ini="${repo}/frontend/python/rst_code_example_pipeline/src/rst_code_example_pipeline/data/toolchain.ini"
+
+# Expand a cache location against the repository root, matching how the
+# Vagrantfile expands it against its own directory. An absolute value is used
+# as-is; a relative one must not depend on the caller's working directory.
+abspath () {
+  case "$1" in
+    /*) echo "$1" ;;
+    *)  echo "${repo}/$1" ;;
+  esac
+}
+
+cache=$(abspath "${LEARN_VM_CACHE_GNAT:-.toolchains/gnat}")
+
+# Downloading is large enough to keep in its own file.
+fetch_impl="${here}/vm_cache_gnat_fetch.sh"
+
+size_of () {
+  if [ -d "$1" ]; then du -sh "$1" 2>/dev/null | cut -f1; else echo "-"; fi
+}
+
+versions_of () {
+  sed -n '/^\[toolchains\]/,/^\[/p' "${toolchain_ini}" \
+    | sed -n "s/^$1[[:space:]]*=[[:space:]]*//p"
+}
+
+# The basenames this cache is required to contain.
+wanted_names () {
+  local tool ver
+  for tool in gnat gnatprove gprbuild; do
+    for ver in $(versions_of "${tool}"); do
+      echo "${tool}-x86_64-linux-${ver}.tar.gz"
+      echo "${tool}-x86_64-linux-${ver}.tar.gz.sha256"
+    done
+  done
+}
+
+# Entries present in the cache that are not required. A .part file is also
+# treated as such: a completed download is always renamed into place, so one
+# that remains is the residue of an interrupted run.
+orphans () {
+  [ -d "${cache}" ] || return 0
+  local wanted
+  # LC_ALL=C throughout: comm compares byte-wise, so both inputs must be
+  # sorted that way too. Locale collation ignores the '-', which puts
+  # gnat-... and gnatprove-... in an order comm rejects.
+  wanted=$(wanted_names | LC_ALL=C sort)
+  find "${cache}" -maxdepth 1 -type f -printf '%f\n' 2>/dev/null \
+    | LC_ALL=C sort \
+    | LC_ALL=C comm -23 - <(echo "${wanted}") \
+    | while read -r f; do echo "${cache}/${f}"; done
+}
+
+require_ini () {
+  if [ ! -f "${toolchain_ini}" ]; then
+    echo "error: ${toolchain_ini} not found" >&2
+    exit 1
+  fi
+}
+
+do_summary () {
+  printf '%-8s %-8s %s\n' "gnat" "$(size_of "${cache}")" "${cache}"
+}
+
+do_report () {
+  require_ini
+  local tool orphan_list f
+
+  echo "Toolchain versions wanted by toolchain.ini:"
+  for tool in gnat gnatprove gprbuild; do
+    printf '  %-10s %s\n' "${tool}" "$(versions_of "${tool}" | tr -s ' ')"
+  done
+
+  echo
+  echo "Toolchain tarballs present:"
+  if [ -d "${cache}" ]; then
+    find "${cache}" -maxdepth 1 -type f -name '*.tar.gz' -printf '  %f\n' \
+      2>/dev/null | sort || true
+  else
+    echo "  (cache directory does not exist yet)"
+  fi
+
+  echo
+  orphan_list=$(orphans)
+  if [ -z "${orphan_list}" ]; then
+    echo "No orphaned entries."
+  else
+    echo "Orphaned entries (not wanted by toolchain.ini):"
+    echo "${orphan_list}" | while read -r f; do
+      printf '  %-8s %s\n' "$(du -h "${f}" 2>/dev/null | cut -f1)" "${f##*/}"
+    done
+    echo
+    echo "Remove them with: frontend/vm/vm_cache_clean.sh --delete"
+  fi
+}
+
+do_clean () {
+  local delete=$1
+  local list count f
+
+  list=$(orphans)
+  if [ -z "${list}" ]; then
+    echo "No orphaned cache entries."
+    return 0
+  fi
+  count=$(echo "${list}" | wc -l)
+
+  if [ "${delete}" = true ]; then
+    echo "${list}" | while read -r f; do
+      echo "removing ${f}"
+      rm -f "${f}"
+    done
+    echo "Removed ${count} entr$([ "${count}" -eq 1 ] && echo y || echo ies)."
+  else
+    echo "Would remove ${count} orphaned entr$([ "${count}" -eq 1 ] && echo y || echo ies):"
+    echo "${list}" | while read -r f; do
+      printf '  %-8s %s\n' "$(du -h "${f}" 2>/dev/null | cut -f1)" "${f}"
+    done
+    echo
+    echo "This was a dry run. Re-run with --delete to remove them."
+  fi
+}
+
+case "${1:-}" in
+  fetch)    shift; exec bash "${fetch_impl}" "$@" ;;
+  summary)  do_summary ;;
+  report)   do_report ;;
+  orphans)  orphans ;;
+  clean)    do_clean "$([ "${2:-}" = "--delete" ] && echo true || echo false)" ;;
+  -h|--help|"")
+    sed -n '3,27p' "${BASH_SOURCE[0]}" | sed 's/^# \{0,1\}//'; exit 0 ;;
+  *)
+    echo "error: unknown command '$1'" >&2; exit 1 ;;
+esac
diff --git a/frontend/vm/vm_cache_gnat_fetch.sh b/frontend/vm/vm_cache_gnat_fetch.sh
new file mode 100755
index 000000000..b4ba88af0
--- /dev/null
+++ b/frontend/vm/vm_cache_gnat_fetch.sh
@@ -0,0 +1,148 @@
+#!/bin/bash
+#
+# Fetch a GNAT-FSF-builds toolchain tarball into the download cache and print
+# its path.
+#
+# This is the implementation of `vm_cache_gnat.sh fetch`, which is the
+# documented way to invoke it.
+#
+# The cache exists so that destroying a VM does not throw the toolchains away:
+# a full reprovision otherwise re-downloads several GB. Upstream publishes a
+# .sha256 sidecar for every asset, and it is verified on every use -- not only
+# after downloading -- so a file corrupted later is re-fetched rather than
+# failing extraction with a confusing tar error.
+#
+# Runs on the host as well as inside a VM. On the host it can be used to warm
+# the cache before `vagrant up`, so that provisioning downloads nothing.
+#
+# Usage:
+#   vm_cache_gnat_fetch.sh <tool> <version>   # print the verified cached path
+#   vm_cache_gnat_fetch.sh --all              # every version in toolchain.ini
+#
+# Environment:
+#   LEARN_VM_CACHE_GNAT   cache directory
+#                         (default: <repo>/.toolchains/gnat; the Vagrantfile
+#                          passes /vagrant_cache/gnat inside the VMs)
+#   LEARN_VM_NAME         suffix for temporary files, so that two VMs sharing
+#                         one cache cannot collide (default: the hostname)
+
+set -eu
+set -o pipefail
+
+here=$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)
+repo=$(cd "${here}/../.." && pwd)
+
+toolchain_ini="${repo}/frontend/python/rst_code_example_pipeline/src/rst_code_example_pipeline/data/toolchain.ini"
+
+# Expand a cache location against the repository root, matching how the
+# Vagrantfile expands it against its own directory. An absolute value is used
+# as-is; a relative one must not depend on the caller's working directory.
+abspath () {
+  case "$1" in
+    /*) echo "$1" ;;
+    *)  echo "${repo}/$1" ;;
+  esac
+}
+
+cache=$(abspath "${LEARN_VM_CACHE_GNAT:-.toolchains/gnat}")
+tag="${LEARN_VM_NAME:-$(hostname)}"
+
+base_url=https://github.com/alire-project/GNAT-FSF-builds/releases/download
+
+usage () {
+  sed -n '3,27p' "${BASH_SOURCE[0]}" | sed 's/^# \{0,1\}//'
+  exit "${1:-1}"
+}
+
+# Fetch one tarball, verified against its upstream .sha256 sidecar.
+# Prints the cached path on stdout; progress goes to stderr so the path can be
+# captured with $(...).
+fetch () {
+  local tool=$1
+  local ver=$2
+  local name="${tool}-x86_64-linux-${ver}.tar.gz"
+  local url="${base_url}/${tool}-${ver}/${name}"
+  local tarball="${cache}/${name}"
+  local sum="${cache}/${name}.sha256"
+  # Two VMs share one cache and fetch the same gnat tarballs, so their
+  # temporaries must not collide.
+  local part="${tarball}.${tag}.part"
+  local sum_part="${sum}.${tag}.part"
+  local rc=0
+
+  mkdir -p "${cache}"
+
+  if [ ! -s "${sum}" ]; then
+    echo "Fetching checksum for ${name}" >&2
+    wget -q -O "${sum_part}" "${url}.sha256" || rc=$?
+    if [ "${rc}" -ne 0 ] || [ ! -s "${sum_part}" ]; then
+      rm -f "${sum_part}"
+      echo "error: could not fetch ${url}.sha256 (exit ${rc})" >&2
+      return 1
+    fi
+    mv "${sum_part}" "${sum}"
+  fi
+
+  if [ -f "${tarball}" ] && verify "${sum}" "${tarball}"; then
+    echo "Using cached ${name}" >&2
+  else
+    [ -f "${tarball}" ] && echo "Cached ${name} failed verification; re-fetching" >&2
+    rm -f "${tarball}"
+    echo "Downloading ${name}" >&2
+    # The redirection creates ${part} before wget runs, so a failure must be
+    # caught rather than left to `set -e` -- otherwise an empty file survives.
+    wget -O "${part}" "${url}" || rc=$?
+    if [ "${rc}" -ne 0 ]; then
+      rm -f "${part}"
+      echo "error: could not download ${url} (exit ${rc})" >&2
+      return 1
+    fi
+    if ! verify "${sum}" "${part}"; then
+      rm -f "${part}"
+      echo "error: ${name} failed checksum verification after download" >&2
+      return 1
+    fi
+    mv "${part}" "${tarball}"
+  fi
+
+  echo "${tarball}"
+}
+
+verify () {
+  local sum=$1
+  local file=$2
+  # The sidecar holds a bare hash with no filename, so pair it up here.
+  echo "$(cat "${sum}")  ${file}" | sha256sum -c - > /dev/null 2>&1
+}
+
+# Read a whitespace-separated list of versions out of toolchain.ini.
+versions_of () {
+  local tool=$1
+  if [ ! -f "${toolchain_ini}" ]; then
+    echo "error: ${toolchain_ini} not found" >&2
+    return 1
+  fi
+  sed -n '/^\[toolchains\]/,/^\[/p' "${toolchain_ini}" \
+    | sed -n "s/^${tool}[[:space:]]*=[[:space:]]*//p"
+}
+
+fetch_all () {
+  local tool ver
+  for tool in gnat gnatprove gprbuild; do
+    for ver in $(versions_of "${tool}"); do
+      fetch "${tool}" "${ver}" > /dev/null
+    done
+  done
+  echo "Cache ready: ${cache}" >&2
+  du -sh "${cache}" 2>/dev/null >&2 || true
+}
+
+case "${1:-}" in
+  --all)          fetch_all ;;
+  -h|--help|"")   usage 0 ;;
+  -*)             echo "error: unknown option '$1'" >&2; usage 1 ;;
+  *)
+    [ $# -eq 2 ] || { echo "error: expected <tool> <version>" >&2; usage 1; }
+    fetch "$1" "$2"
+    ;;
+esac
diff --git a/frontend/vm/vm_cache_report.sh b/frontend/vm/vm_cache_report.sh
new file mode 100755
index 000000000..dc249c4ec
--- /dev/null
+++ b/frontend/vm/vm_cache_report.sh
@@ -0,0 +1,60 @@
+#!/bin/bash
+#
+# Report on the VM download caches.
+#
+# Prints one summary line per cache, followed by the detailed report of each
+# cache that provides one.
+#
+# The caches are handled by one script each: vm_cache_gnat.sh and
+# vm_cache_apt.sh. Either may also be invoked directly.
+#
+# Usage:
+#   vm_cache_report.sh            # all caches
+#   vm_cache_report.sh --orphans  # just the orphan paths, one per line
+#
+# Environment:
+#   LEARN_VM_CACHE_GNAT / _APT   override the cache locations
+#   (defaults: <repo>/.toolchains/{gnat,apt})
+
+set -eu
+set -o pipefail
+
+here=$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)
+
+gnat="${here}/vm_cache_gnat.sh"
+apt="${here}/vm_cache_apt.sh"
+
+case "${1:-}" in
+  --orphans)
+    # Each cache is reported even if another fails, so that one broken cache
+    # does not hide the rest. The worst status is returned.
+    rc=0
+    "${gnat}" orphans || rc=$?
+    "${apt}" orphans || rc=$?
+    exit "${rc}"
+    ;;
+  -h|--help)
+    sed -n '3,17p' "${BASH_SOURCE[0]}" | sed 's/^# \{0,1\}//'
+    exit 0
+    ;;
+  "") ;;
+  *)  echo "error: unknown option '$1'" >&2; exit 1 ;;
+esac
+
+printf '%-8s %-8s %s\n' "CACHE" "SIZE" "LOCATION"
+"${gnat}" summary
+"${apt}" summary
+
+rc=0
+
+echo
+echo "GNAT toolchain cache"
+echo "--------------------"
+"${gnat}" report || rc=$?
+
+echo
+echo "apt package cache"
+echo "-----------------"
+"${apt}" report || rc=$?
+
+exit "${rc}"