Add general option -output-directory

doc/changelog/09-cli-tools/17392-master+add-output-directory.rst

@@ -0,0 +1,6 @@
+- **Added:**
+  Command line option :n:`-output-directory dir` to set the default output directory
+  for extraction, :cmd:`Redirect` and :cmd:`Print Universes`
+  (`#17392 <https://github.com/coq/coq/pull/17392>`_,
+  fixes `#8649 <https://github.com/coq/coq/issues/8649>`_,
+  by Hugo Herbelin).

doc/sphinx/addendum/extraction.rst

@@ -490,8 +490,10 @@ 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 not set,
+   files will be written to the directory specified by the command line
+   option :n:`-output-directory`, if set (see :ref:`command-line-options`) and
+   otherwise, the current directory.  Use :cmd:`Pwd` to display the current directory.
 
 Differences between Coq and ML type systems
 ----------------------------------------------

doc/sphinx/addendum/universe-polymorphism.rst

@@ -608,6 +608,10 @@ 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``.
+   If :n:`@string` is a relative filename, it refers to the directory
+   specified by the command line option `-output-directory`, if set
+   (see :ref:`command-line-options`) and otherwise, the current
+   directory. Use :cmd:`Pwd` to display the current directory.
 
 Polymorphic definitions
 ~~~~~~~~~~~~~~~~~~~~~~~

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

@@ -365,6 +365,8 @@ 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*: Sets the output directory for commands that
+  write output to files, such as :ref:`extraction` commands, :cmd:`Redirect` and :cmd:`Print Universes`.
 :-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

@@ -865,6 +865,10 @@ Quitting and debugging
    Executes :n:`@sentence`, redirecting its
    output to the file ":n:`@string`.out".
 
+   If :n:`@string` is a relative filename, it refers to the directory
+   specified by the command line option `-output-directory`, if set
+   (see :ref:`command-line-options`) and otherwise, the current
+   directory. Use :cmd:`Pwd` to display the current directory.
 
 .. cmd:: Timeout @natural @sentence
 

kernel/nativelib.ml

@@ -168,8 +168,8 @@ let compile_library (code, symb) fn =
   let header = mk_library_header symb in
   let fn = fn ^ source_ext in
   let basename = Filename.basename fn in
-  let dirname = Filename.dirname fn in
-  let dirname = dirname / !output_dir in
+  let dirname =
+    if Filename.is_relative !output_dir then Filename.dirname fn / !output_dir else !output_dir in
   let () =
     try Unix.mkdir dirname 0o755
     with Unix.Unix_error (Unix.EEXIST, _, _) -> ()

lib/flags.ml

@@ -80,3 +80,7 @@ let get_inline_level () = !inline_level
 
 let profile_ltac = ref false
 let profile_ltac_cutoff = ref 2.0
+
+(* Default output directory *)
+
+let output_directory = ref None

lib/flags.mli

@@ -96,3 +96,6 @@ val default_inline_level : int
 (** Global profile_ltac flag  *)
 val profile_ltac : bool ref
 val profile_ltac_cutoff : float ref
+
+(** Default output directory *)
+val output_directory : CUnix.physical_path option ref

lib/system.ml

@@ -225,6 +225,21 @@ let is_in_system_path filename =
     warn_path_not_found ();
     false
 
+let warn_using_current_directory =
+  CWarnings.create ~name:"default-output-directory" ~category:CWarnings.CoreCategories.filesystem
+    Pp.(fun s ->
+           strbrk "Output directory is unset, using \"" ++ str s ++ str "\"." ++ spc () ++
+           strbrk "Use command line option \"-output-directory to set a default directory.")
+
+let get_output_path filename =
+  if not (Filename.is_relative filename) then filename
+  else match !Flags.output_directory with
+  | None ->
+    let pwd = Sys.getcwd () in
+    warn_using_current_directory pwd;
+    Filename.concat pwd filename
+  | Some dir -> Filename.concat dir filename
+
 let error_corrupted file s =
   CErrors.user_err (str file ++ str ": " ++ str s ++ str ". Try to rebuild it.")
 

lib/system.mli

@@ -58,6 +58,10 @@ val is_in_system_path : string -> bool
 val where_in_path :
   ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string
 
+(** [get_output_path fname] relativizes [fname] with respect to the
+    default output directory if [fname] is not absolute *)
+val get_output_path : CUnix.physical_path -> CUnix.physical_path
+
 (** [find_file_in_path ?warn loadpath filename] returns the directory
     name and long name of the first physical occurrence [filename] in
     one of the directory of the [loadpath];

plugins/extraction/table.ml

@@ -523,7 +523,8 @@ let warn_using_current_directory =
        Pp.(strbrk
              "Setting extraction output directory by default to \"" ++ str s ++ strbrk "\". Use \"" ++
            str "Set Extraction Output Directory" ++
-           strbrk "\" to set a different directory for extracted files to appear in."))
+           strbrk "\" or command line option \"-output-directory\" to " ++
+           strbrk "set a different directory for extracted files to appear in."))
 
 let output_directory_key = ["Extraction"; "Output"; "Directory"]
 
@@ -532,13 +533,12 @@ let { Goptions.get = output_directory } =
     ~key:output_directory_key ()
 
 let output_directory () =
-  match output_directory () with
-  | Some dir ->
+  match output_directory (), !Flags.output_directory with
+  | Some dir, _ | None, Some dir ->
       (* Ensure that the directory exists *)
       System.mkdir dir;
       dir
-      (* CErrors.user_err Pp.(str "Extraction output directory " ++ str dir ++ str " does not exist.") *)
-  | None ->
+  | None, None ->
     let pwd = Sys.getcwd () in
     warn_using_current_directory pwd;
     (* Note: in case of error in the caller of output_directory, the effect of the setting will be undo *)

sysinit/coqargs.ml

@@ -66,6 +66,7 @@ type coqargs_config = {
   native_compiler : native_compiler;
   native_output_dir : CUnix.physical_path;
   native_include_dirs : CUnix.physical_path list;
+  output_directory : CUnix.physical_path option;
   time        : time_config option;
   profile : string option;
   print_emacs : bool;
@@ -123,6 +124,7 @@ let default_config = {
   native_compiler = default_native;
   native_output_dir = ".coq-native";
   native_include_dirs = [];
+  output_directory = None;
   time         = None;
   profile = None;
   print_emacs  = false;
@@ -382,6 +384,11 @@ let parse_args ~usage ~init arglist : t * string list =
       let native_output_dir = next () in
       { oval with config = { oval.config with native_output_dir } }
 
+    |"-output-dir" | "-output-directory" ->
+      let dir = next () in
+      let dir = if Filename.is_relative dir then Filename.concat (Sys.getcwd ()) dir else dir in
+      { oval with config = { oval.config with output_directory = Some dir } }
+
     |"-nI" ->
       let include_dir = next () in
       { oval with config = {oval.config with native_include_dirs = include_dir :: oval.config.native_include_dirs } }

sysinit/coqargs.mli

@@ -58,6 +58,7 @@ type coqargs_config = {
   native_compiler : native_compiler;
   native_output_dir : CUnix.physical_path;
   native_include_dirs : CUnix.physical_path list;
+  output_directory : CUnix.physical_path option;
   time        : time_config option;
   profile : string option;
   print_emacs : bool;

sysinit/coqinit.ml

@@ -171,6 +171,9 @@ let init_runtime opts =
   Nativelib.output_dir := opts.config.native_output_dir;
   Nativelib.include_dirs := opts.config.native_include_dirs;
 
+  (* Default output dir *)
+  Flags.output_directory := opts.config.output_directory;
+
   (* Paths for loading stuff *)
   init_load_paths opts;
 

vernac/topfmt.ml

@@ -401,7 +401,10 @@ let print_err_exn any =
   std_logger ?pre_hdr Feedback.Error msg
 
 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 = System.get_output_path fname in
+  System.mkdir (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

@@ -329,7 +329,9 @@ let dump_universes output g =
   Univ.Level.Map.iter dump_arc g
 
 let dump_universes_gen prl g s =
-  let output = open_out s in
+  let fulls = System.get_output_path s in
+  System.mkdir (Filename.dirname fulls);
+  let output = open_out fulls in
   let output_constraint, close =
     if Filename.check_suffix s ".dot" || Filename.check_suffix s ".gv" then begin
       (* the lazy unit is to handle errors while printing the first line *)