Merge PR #6818: Sphinx doc infrastructure

1 files changed, 10 insertions, 15 deletions

diff --git a/configure.ml b/configure.ml
index 1eae3bd93..4726831e4 100644
--- a/configure.ml
+++ b/configure.ml
@@ -957,23 +957,18 @@ let strip =
 
 (** * Documentation : do we have latex, hevea, ... *)
 
+let check_sphinx_deps () =
+  ignore (run (which "python3") ["doc/tools/coqrst/checkdeps.py"])
+
 let check_doc () =
   let err s =
-    ceprintf "%s was not found; documentation will not be available" s;
-    raise Not_found
+    die (sprintf "A documentation build was requested, but %s was not found." s);
   in
-  try
-    if not !prefs.withdoc then raise Not_found;
-    if not (program_in_path "latex") then err "latex";
-    if not (program_in_path "hevea") then err "hevea";
-    if not (program_in_path "hacha") then err "hacha";
-    if not (program_in_path "fig2dev") then err "fig2dev";
-    if not (program_in_path "convert") then err "convert";
-    true
-  with Not_found -> false
-
-let withdoc = check_doc ()
+  if not (program_in_path "python3") then err "python3";
+  if not (program_in_path "sphinx-build") then err "sphinx-build";
+  check_sphinx_deps ()
 
+let _ = if !prefs.withdoc then check_doc ()
 
 (** * Installation directories : bindir, libdir, mandir, docdir, etc *)
 
@@ -1114,7 +1109,7 @@ let print_summary () =
     pr "  Mac OS integration is on\n";
   pr "  CoqIde                      : %s\n" coqide;
   pr "  Documentation               : %s\n"
-    (if withdoc then "All" else "None");
+    (if !prefs.withdoc then "All" else "None");
   pr "  Web browser                 : %s\n" browser;
   pr "  Coq web site                : %s\n" !prefs.coqwebsite;
   pr "  Bytecode VM enabled         : %B\n" !prefs.bytecodecompiler;
@@ -1342,7 +1337,7 @@ let write_makefile f =
   pr "# Defining REVISION\n";
   pr "CHECKEDOUT=%s\n\n" vcs;
   pr "# Option to control compilation and installation of the documentation\n";
-  pr "WITHDOC=%s\n\n" (if withdoc then "all" else "no");
+  pr "WITHDOC=%s\n\n" (if !prefs.withdoc then "all" else "no");
   pr "# Option to produce precompiled files for native_compute\n";
   pr "NATIVECOMPUTE=%s\n" (if !prefs.nativecompiler then "-native-compiler" else "");
   close_out o;