Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

deprecate Cd command #16119

Closed
wants to merge 2 commits into from
Closed

deprecate Cd command #16119

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
cce5a19
deprecate Cd command
Alizter May 31, 2022
ad6f92f
TODO: FOR TESTING: Make Cd deprecation warning an error
Alizter May 31, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
5 changes: 2 additions & 3 deletions vernac/g_vernac.mlg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -921,9 +921,8 @@ GRAMMAR EXTEND Gram
{ VernacDeclareScope sc }

(* System directory *)
| IDENT "Pwd" -> { VernacChdir None }
| IDENT "Cd" -> { VernacChdir None }
| IDENT "Cd"; dir = ne_string -> { VernacChdir (Some dir) }
| IDENT "Pwd" -> { VernacPwd }
| IDENT "Cd"; dir = ne_string -> { VernacChdir dir }

| IDENT "Load"; verbosely = [ IDENT "Verbose" -> { true } | -> { false } ];
s = [ s = ne_string -> { s } | s = IDENT -> { s } ] ->
Expand Down
4 changes: 3 additions & 1 deletion vernac/ppvernac.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1087,7 +1087,9 @@ let pr_vernac_expr v =
hov 2 (keyword "Declare ML Module" ++ spc() ++ prlist_with_sep sep qs l)
)
| VernacChdir s ->
return (keyword "Cd" ++ pr_opt qs s)
return (keyword "Cd" ++ qs s)
| VernacPwd ->
return (keyword "Pwd")

(* Commands *)
| VernacCreateHintDb (dbname,b) ->
Expand Down
2 changes: 1 addition & 1 deletion vernac/vernac_classifier.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -138,7 +138,7 @@ let classify_vernac e =
| VernacUniverse _ | VernacConstraint _
| VernacCanonical _ | VernacCoercion _ | VernacIdentityCoercion _
| VernacAddLoadPath _ | VernacRemoveLoadPath _ | VernacAddMLPath _
| VernacChdir _
| VernacChdir _ | VernacPwd
| VernacCreateHintDb _ | VernacRemoveHints _ | VernacHints _
| VernacArguments _
| VernacReserve _
Expand Down
30 changes: 18 additions & 12 deletions vernac/vernacentries.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1584,18 +1584,22 @@ let vernac_declare_ml_module ~local l =
let l = List.map expand l in
Mltop.declare_ml_modules local l

let vernac_chdir = function
| None -> Feedback.msg_notice (str (Sys.getcwd()))
| Some path ->
begin
try Sys.chdir (expand path)
with Sys_error err ->
(* Cd is typically used to control the output directory of
extraction. A failed Cd could lead to overwriting .ml files
so we make it an error. *)
user_err Pp.(str ("Cd failed: " ^ err))
end;
Flags.if_verbose Feedback.msg_info (str (Sys.getcwd()))
let warn_cd = CWarnings.create ~name:"cd-deprecated" ~category:"deprecated" ~default:CWarnings.AsError
(fun () -> strbrk "The command \"Cd\" is deprecated." ++ spc () ++
(* TODO: *)
strbrk "TODO: something about how extraction will/does support an output dir so use that instead" ++ spc () ++
strbrk "Use the \"Pwd\" command to print the current working directory." ++ spc () ++
strbrk "If \"Cd\" is an important feature for you, please open an issue at" ++ spc () ++
strbrk "https://github.com/coq/coq/issues" ++ spc () ++ strbrk "and explain your workflow.")

let vernac_chdir path =
warn_cd ();
try Sys.chdir (expand path)
with Sys_error err ->
(* Cd is typically used to control the output directory of
extraction. A failed Cd could lead to overwriting .ml files
so we make it an error. *)
user_err Pp.(str ("Cd failed: " ^ err))

(************)
(* Commands *)
Expand Down Expand Up @@ -2469,6 +2473,8 @@ let translate_vernac ?loc ~atts v = let open Vernacextend in match v with
vtdefault(fun () -> with_locality ~atts vernac_declare_ml_module l)
| VernacChdir s ->
vtdefault(fun () -> unsupported_attributes atts; vernac_chdir s)
| VernacPwd ->
vtdefault(fun () -> unsupported_attributes atts; Feedback.msg_notice (str (Sys.getcwd ())))

(* Commands *)
| VernacCreateHintDb (dbname,b) ->
Expand Down
3 changes: 2 additions & 1 deletion vernac/vernacexpr.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -415,7 +415,8 @@ type nonrec vernac_expr =
| VernacRemoveLoadPath of string
| VernacAddMLPath of string
| VernacDeclareMLModule of string list
| VernacChdir of string option
| VernacChdir of string
| VernacPwd

(* Resetting *)
| VernacResetName of lident
Expand Down