Extending the use of -output-directory to Redirect and Print Universes.

doc/sphinx/addendum/extraction.rst

@@ -476,8 +476,11 @@ Additional settings
 
 .. opt:: Extraction Output Directory @string
 
-   Sets the directory where extracted files will be written.
-   The default is the current directory, which can be displayed with :cmd:`Pwd`.
+   Sets the directory where extracted files will be written. If unset,
+   the default is to use the directory set with the command line
+   option :n:`-output-directory` (see :ref:`command-line-options`). If
+   the latter is itself unset, the default is to use the current
+   directory, which can be displayed with :cmd:`Pwd`.
 
 Differences between Coq and ML type systems
 ----------------------------------------------

doc/sphinx/addendum/universe-polymorphism.rst

@@ -607,6 +607,9 @@ Printing universes
    If :n:`@string` ends in ``.dot`` or ``.gv``, the constraints are printed in the DOT
    language, and can be processed by Graphviz tools. The format is
    unspecified if `string` doesn’t end in ``.dot`` or ``.gv``.
+   The directory in which the file is created (or overriden) can be set
+   with the command line option `-output-directory` (see
+   :ref:`command-line-options`).
 
 Polymorphic definitions
 ~~~~~~~~~~~~~~~~~~~~~~~

doc/sphinx/practical-tools/coq-commands.rst

@@ -354,6 +354,9 @@ and ``coqtop``, unless stated otherwise:
 
 :-native-output-dir *dir*: Set the directory in which to put the aforementioned
   ``.cmxs`` for :tacn:`native_compute`. Defaults to ``.coq-native``.
+:-output-directory *dir*, -output-dir *dir*: Set the directory in which some commands,
+  such as :ref:`extraction` commands, or :cmd:`Redirect`, or :cmd:`Print Universes`,
+  may decide to output the files they create.
 :-vos: Indicate Coq to skip the processing of opaque proofs
   (i.e., proofs ending with :cmd:`Qed` or :cmd:`Admitted`), output a ``.vos`` files
   instead of a ``.vo`` file, and to load ``.vos`` files instead of ``.vo`` files

doc/sphinx/proof-engine/vernacular-commands.rst

@@ -911,6 +911,9 @@ Quitting and debugging
    Executes :n:`@sentence`, redirecting its
    output to the file ":n:`@string`.out".
 
+   The directory in which the file is created (or overriden) can be set
+   with the command line option `-output-directory` (see
+   :ref:`command-line-options`).
 
 .. cmd:: Timeout @natural @sentence
 

vernac/topfmt.ml

@@ -400,8 +400,22 @@ let print_err_exn any =
   let msg = CErrors.iprint (e, info) ++ fnl () in
   std_logger ?pre_hdr Feedback.Error msg
 
+let warn_using_current_directory =
+  CWarnings.create ~name:"redirect-default-directory" ~category:"redirect"
+    (fun s ->
+       Pp.(strbrk "Output directory is unset, using \"" ++ str s ++ str "\"." ++ spc () ++
+           strbrk "Use command line option \"-output-directory to set a default directory."))
+
 let with_output_to_file fname func input =
-  let channel = open_out (String.concat "." [fname; "out"]) in
+  let fname = String.concat "." [fname; "out"] in
+  let fullfname =
+    match Filename.is_relative fname, !Flags.output_directory with
+    | false, _ | _, None ->
+      let pwd = Sys.getcwd () in warn_using_current_directory pwd;
+      Filename.concat pwd fname
+    | true, Some dir -> Filename.concat dir fname in
+  System.mkdirhier (Filename.dirname fullfname);
+  let channel = open_out fullfname in
   let old_fmt = !std_ft, !err_ft, !deep_ft in
   let new_ft = Format.formatter_of_out_channel channel in
   set_gp new_ft (get_gp !std_ft);

vernac/vernacentries.ml

@@ -311,6 +311,12 @@ let print_registered () =
   in
   hov 0 (prlist_with_sep fnl pr_lib_ref @@ Coqlib.get_lib_refs ())
 
+let warn_using_current_directory =
+  CWarnings.create ~name:"print-universes-default-directory" ~category:"print-universes"
+    (fun s ->
+       Pp.(strbrk "Output directory is unset, using \"" ++ str s ++ str "\"." ++ spc () ++
+           strbrk "Use command line option \"-output-directory to set a default directory."))
+
 let dump_universes output g =
   let open Univ in
   let dump_arc u = function
@@ -324,6 +330,13 @@ let dump_universes output g =
   Univ.Level.Map.iter dump_arc g
 
 let dump_universes_gen prl g s =
+  let fulls =
+    match Filename.is_relative s, !Flags.output_directory with
+    | false, _ | _, None ->
+      let pwd = Sys.getcwd () in warn_using_current_directory pwd;
+      Filename.concat pwd s
+    | true, Some dir -> Filename.concat dir s in
+  System.mkdirhier (Filename.dirname fulls);
   let output = open_out s in
   let output_constraint, close =
     if Filename.check_suffix s ".dot" || Filename.check_suffix s ".gv" then begin