From 73563c2ff4a4214a3b6aa2333c3f413086500a0e Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Thu, 2 Apr 2020 15:37:24 +0200 Subject: Remove deprecated -require option. This option is confusing because it does Require Import, not Require. It was deprecated in 8.11. We remove it in 8.12 in order to reintroduce it in 8.13 as a replacement for -load-vernac-object, which is the option that does Require without Import as of today. --- doc/sphinx/practical-tools/coq-commands.rst | 1 - toplevel/coqargs.ml | 8 -------- 2 files changed, 9 deletions(-) diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index aa4b6edd7d..85ed0112ae 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -172,7 +172,6 @@ and ``coqtop``, unless stated otherwise: This is equivalent to running :n:`From` :n:`@dirpath` :cmd:`Require Import` :n:`@qualid`. :-refrom *dirpath* *qualid*, -require-export-from *dirpath* *qualid*: Load |Coq| compiled library :n:`@qualid` and transitively import it. This is equivalent to running :n:`From` :n:`@dirpath` :cmd:`Require Export` :n:`@qualid`. -:-require *qualid*: Deprecated; use ``-ri`` *qualid*. :-batch: Exit just after argument parsing. Available for ``coqtop`` only. :-compile *file.v*: Deprecated; use ``coqc`` instead. Compile file *file.v* into *file.vo*. This option implies -batch (exit just after argument parsing). It is available only diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 4963a806f5..d974fc0f7c 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -203,10 +203,6 @@ let warn_deprecated_inputstate = CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated" (fun () -> Pp.strbrk "The inputstate option is deprecated and discouraged.") -let warn_deprecated_simple_require = - CWarnings.create ~name:"deprecated-boot" ~category:"deprecated" - (fun () -> Pp.strbrk "The -require option is deprecated, please use -require-import instead.") - let set_inputstate opts s = warn_deprecated_inputstate (); { opts with pre = { opts.pre with inputstate = Some s }} @@ -422,10 +418,6 @@ let parse_args ~help ~init arglist : t * string list = |"-rfrom" -> let from = next () in add_vo_require oval (next ()) (Some from) None - |"-require" -> - warn_deprecated_simple_require (); - add_vo_require oval (next ()) None (Some false) - |"-require-import" | "-ri" -> add_vo_require oval (next ()) None (Some false) |"-require-export" | "-re" -> add_vo_require oval (next ()) None (Some true) -- cgit v1.2.3 From efa833d06990262174195fdc43a542d272b480a3 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Thu, 2 Apr 2020 15:47:34 +0200 Subject: Fix options listed in asycTaskQueue. --- stm/asyncTaskQueue.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index c8eb7b08f1..87d844edb3 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -138,7 +138,9 @@ module Make(T : Task) () = struct set_slave_opt tl (* We need to pass some options with one argument *) | ( "-I" | "-include" | "-top" | "-topfile" | "-coqlib" | "-exclude-dir" | "-compat" - | "-require" | "-w" | "-color" | "-init-file" + | "-require-import" | "-require-export" | "-require-import-from" | "-require-export-from" + | "-ri" | "-re" | "-rifrom" | "-refrom" | "-load-vernac-object" + | "-w" | "-color" | "-init-file" | "-profile-ltac-cutoff" | "-main-channel" | "-control-channel" | "-mangle-names" | "-set" | "-unset" | "-diffs" | "-mangle-name" | "-dump-glob" | "-bytecode-compiler" | "-native-compiler" as x) :: a :: tl -> x :: a :: set_slave_opt tl -- cgit v1.2.3 From 0c1382bd0a9c41b559a912695e2154b758de7b18 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Thu, 2 Apr 2020 15:51:09 +0200 Subject: Minimal fix to man pages. --- man/coqide.1 | 2 +- man/coqtop.1 | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/man/coqide.1 b/man/coqide.1 index 62a102af03..c1af046019 100644 --- a/man/coqide.1 +++ b/man/coqide.1 @@ -69,7 +69,7 @@ Load Coq library (Require .IR path .). .TP -.BI \-require\ path +.BI \-require-import\ path Load Coq library .IR path and import it (Require Import diff --git a/man/coqtop.1 b/man/coqtop.1 index 25d0ef7718..e799bc7748 100644 --- a/man/coqtop.1 +++ b/man/coqtop.1 @@ -79,7 +79,7 @@ load Coq library (Require path.) .TP -.BI \-require \ path +.BI \-require-import \ path load Coq library .I path and import it (Require Import path.) -- cgit v1.2.3 From cb1e693d84013b56c9a8e6154e101245c950f85f Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Thu, 2 Apr 2020 15:59:53 +0200 Subject: Add changelog entry for #12005. --- doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst diff --git a/doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst b/doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst new file mode 100644 index 0000000000..e38f2f337a --- /dev/null +++ b/doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst @@ -0,0 +1,5 @@ +- **Removed:** + Confusingly-named and deprecated since 8.11 `-require` option. + Use `-require-import` instead + (`#12005 `_, + by Théo Zimmermann). -- cgit v1.2.3 From e3e1133fe5685213460a6cc3f761283815223e3d Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Thu, 2 Apr 2020 22:23:02 +0200 Subject: Document -rfrom option in reference manual. So far it was only documented in coqtop --help. --- doc/sphinx/practical-tools/coq-commands.rst | 2 ++ 1 file changed, 2 insertions(+) diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 85ed0112ae..958d295219 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -164,6 +164,8 @@ and ``coqtop``, unless stated otherwise: it is executed. :-load-vernac-object *qualid*: Load |Coq| compiled library :n:`@qualid`. This is equivalent to running :cmd:`Require` :n:`qualid`. +:-rfrom *dirpath* *qualid*: Load |Coq| compiled library :n:`@qualid`. + This is equivalent to running :n:`From` :n:`@dirpath` :cmd:`Require Import` :n:`@qualid`. :-ri *qualid*, -require-import *qualid*: Load |Coq| compiled library :n:`@qualid` and import it. This is equivalent to running :cmd:`Require Import` :n:`@qualid`. :-re *qualid*, -require-export *qualid*: Load |Coq| compiled library :n:`@qualid` and transitively import it. -- cgit v1.2.3 From 8ac8f5aa327ca8de66e90bb33d1950d9a4749177 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Fri, 3 Apr 2020 10:27:15 +0200 Subject: Update doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst Co-Authored-By: Gaëtan Gilbert --- doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst b/doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst index e38f2f337a..affb685fcb 100644 --- a/doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst +++ b/doc/changelog/08-tools/12005-remove-deprecated-coqtop-options.rst @@ -1,5 +1,5 @@ - **Removed:** Confusingly-named and deprecated since 8.11 `-require` option. - Use `-require-import` instead + Use the equivalent `-require-import` instead (`#12005 `_, by Théo Zimmermann). -- cgit v1.2.3