Merge PR #17403: Deprecating change directory

Reviewed-by: SkySkimmer
Ack-by: jfehrle
Ack-by: Alizter
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>

doc/changelog/08-vernac-commands-and-options/17403-master+deprecating-change-directory.rst

@@ -0,0 +1,6 @@
+- **Deprecated:**
+  The :cmd:`Cd` command.  Instead use the command line option
+  `-output-directory` (see :ref:`command-line-options`) or, for
+  extraction, :opt:`Extraction Output Directory`
+  (`#17403 <https://github.com/coq/coq/pull/17403>`_,
+  by Ali Caglayan and Hugo Herbelin).

doc/sphinx/addendum/extraction.rst

@@ -103,6 +103,12 @@ in the Coq sources.
 
 .. cmd:: Cd {? @string }
 
+   .. deprecated:: 8.20
+
+      Use the command line option :n:`-output-directory` instead (see
+      :ref:`command-line-options`), or the :opt:`Extraction Output Directory`
+      option.
+
    If :n:`@string` is specified, changes the current directory according to
    :token:`string` which can be any valid path.  Otherwise, it displays the
    current directory as :cmd:`Pwd` does.

vernac/g_vernac.mlg

@@ -90,6 +90,10 @@ let test_id_colon =
     lk_ident >> lk_kw ":"
   end
 
+let warn_chdir_pwd = CWarnings.create ~name:"change-dir-pwd-deprecated" ~category:Deprecation.Version.v8_20
+    (fun () -> strbrk "Command \"Cd\" as a synonym of \"Pwd\" is deprecated." ++ spc () ++
+               strbrk "Use \"Pwd\" instead.")
+
 }
 
 GRAMMAR EXTEND Gram
@@ -1044,7 +1048,7 @@ GRAMMAR EXTEND Gram
 
       (* System directory *)
       | IDENT "Pwd" -> { VernacSynterp (VernacChdir None) }
-      | IDENT "Cd" -> { VernacSynterp (VernacChdir None) }
+      | IDENT "Cd" -> { warn_chdir_pwd (); VernacSynterp (VernacChdir None) }
       | IDENT "Cd"; dir = ne_string -> { VernacSynterp (VernacChdir (Some dir)) }
 
       | IDENT "Load"; verbosely = [ IDENT "Verbose" -> { true } | -> { false } ];

vernac/ppvernac.ml

@@ -1375,8 +1375,10 @@ let pr_synterp_vernac_expr v =
     return (
       hov 2 (keyword "Declare ML Module" ++ spc() ++ prlist_with_sep sep qs l)
     )
-  | VernacChdir s ->
-    return (keyword "Cd" ++ pr_opt qs s)
+  | VernacChdir None ->
+    return (keyword "Pwd")
+  | VernacChdir (Some s) ->
+    return (keyword "Cd " ++ qs s)
   | VernacSetOption (export, na,v) ->
     let export = if export then keyword "Export" ++ spc () else mt () in
     let set = if v == OptionUnset then "Unset" else "Set" in

vernac/synterp.ml

@@ -318,9 +318,15 @@ let synterp_declare_ml_module ~local l =
   let l = List.map expand l in
   Mltop.declare_ml_modules local l
 
+let warn_chdir = CWarnings.create ~name:"change-dir-deprecated" ~category:Deprecation.Version.v8_20
+    (fun () -> strbrk "Command \"Cd\" is deprecated." ++ spc () ++
+               strbrk "Use command-line \"-output-directory dir\" instead, or, alternatively, " ++
+               strbrk "for extraction, \"Set Extraction Output Directory\".")
+
 let synterp_chdir = function
   | None -> Feedback.msg_notice (str (Sys.getcwd()))
   | Some path ->
+      warn_chdir ();
       begin
         try Sys.chdir (expand path)
         with Sys_error err ->