# HG changeset patch
# User wenzelm
# Date 1737743755 -3600
# Node ID bd8e174b6f9564af8d39b8430131f19110e9b81d
# Parent  6a2f889fa3b9f8f980d002388e085480a76ded5a
more explicit system dependencies;

diff -r 6a2f889fa3b9 -r bd8e174b6f95 src/Pure/Admin/component_hol_light.scala
--- a/src/Pure/Admin/component_hol_light.scala	Fri Jan 24 19:25:31 2025 +0100
+++ b/src/Pure/Admin/component_hol_light.scala	Fri Jan 24 19:35:55 2025 +0100
@@ -35,6 +35,8 @@
 
     if (!only_offline) {
       Linux.check_system()
+      Isabelle_System.require_command("bzip2")
+      Isabelle_System.require_command("m4")
       Isabelle_System.require_command("patch")
       Isabelle_System.require_command("zstd")
     }
@@ -231,6 +233,9 @@
 
     isabelle component_hol_light_import -L Logic/make.ml
     isabelle component_hol_light_import -L 100/thales.ml -L 100/ceva.ml
+
+  The HOL Light build process uses OCaml/OPAM from Isabelle; this requires
+  C development tools with libgmp-dev.
 """,
           "D:" -> (arg => target_dir = Path.explode(arg)),
           "L:" -> (arg => load_more = load_more ::: List(Path.explode(arg))),