diff --git a/doc/changelog/08-vernac-commands-and-options/17403-master+deprecating-change-directory.rst b/doc/changelog/08-vernac-commands-and-options/17403-master+deprecating-change-directory.rst new file mode 100644 index 000000000000..d607f90e5a5c --- /dev/null +++ b/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 `_, + by Ali Caglayan and Hugo Herbelin). diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst index b415b41f08b6..0de573d20398 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/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. diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 36cc0bad1ad9..ada9b14a0217 100644 --- a/vernac/g_vernac.mlg +++ b/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 } ]; diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 42165144e322..e8ff558c0d95 100644 --- a/vernac/ppvernac.ml +++ b/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 diff --git a/vernac/synterp.ml b/vernac/synterp.ml index 22a2ad1a2b9c..ae309a4e46fd 100644 --- a/vernac/synterp.ml +++ b/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 ->