Merge PR #10245: Command line: adding variants for Require, aligning on the vernac syntax

Reviewed-by: cpitclaudel
Reviewed-by: ejgallego
Ack-by: herbelin

4 files changed, 57 insertions, 12 deletions

diff --git a/doc/changelog/08-tools/10245-require-command-line.rst b/doc/changelog/08-tools/10245-require-command-line.rst
new file mode 100644
index 0000000000..54417077f5
--- /dev/null
+++ b/doc/changelog/08-tools/10245-require-command-line.rst
@@ -0,0 +1,6 @@
+- Add command line options `-require-import`, `-require-export`,
+  `-require-import-from` and `-require-export-from`, as well as their
+  shorthand, `-ri`, `-re`, `-refrom` and -`rifrom`. Deprecate
+  confusing command line option `-require`
+  (`#10245 <https://github.com/coq/coq/pull/10245>`_
+  by Hugo Herbelin, review by Emilio Gallego).
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index bdda35fcc0..48d5f4075e 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -124,11 +124,11 @@ and ``coqtop``, unless stated otherwise:
 
      :ref:`names-of-libraries` and the
      command Declare ML Module Section :ref:`compiled-files`.
-:-Q *directory* dirpath: Add physical path *directory* to the list of
+:-Q *directory* *dirpath*: Add physical path *directory* to the list of
   directories where |Coq| looks for a file and bind it to the logical
   directory *dirpath*. The subdirectory structure of *directory* is
   recursively available from |Coq| using absolute names (extending the
-  dirpath prefix) (see Section :ref:`qualified-names`).Note that only those
+  :n:`@dirpath` prefix) (see Section :ref:`qualified-names`). Note that only those
   subdirectories and files which obey the lexical conventions of what is
   an :n:`@ident` are taken into account. Conversely, the
   underlying file systems or operating systems may be more restrictive
@@ -138,13 +138,13 @@ and ``coqtop``, unless stated otherwise:
   disallow two files differing only in the case in the same directory.
 
   .. seealso:: Section :ref:`names-of-libraries`.
-:-R *directory* dirpath: Do as -Q *directory* dirpath but make the
+:-R *directory* *dirpath*: Do as ``-Q`` *directory* *dirpath* but make the
   subdirectory structure of *directory* recursively visible so that the
   recursive contents of physical *directory* is available from |Coq| using
   short or partially qualified names.
 
   .. seealso:: Section :ref:`names-of-libraries`.
-:-top dirpath: Set the toplevel module name to dirpath instead of Top.
+:-top *dirpath*: Set the toplevel module name to :n:`@dirpath` instead of ``Top``.
   Not valid for `coqc` as the toplevel module name is inferred from the
   name of the output file.
 :-exclude-dir *directory*: Exclude any subdirectory named *directory*
@@ -164,10 +164,17 @@ and ``coqtop``, unless stated otherwise:
 :-lv *file*, -load-vernac-source-verbose *file*: Load and execute the
   |Coq| script from *file.v*. Write its contents to the standard output as
   it is executed.
-:-load-vernac-object dirpath: Load |Coq| compiled library dirpath. This
-  is equivalent to runningRequire dirpath.
-:-require dirpath: Load |Coq| compiled library dirpath and import it.
-  This is equivalent to running Require Import dirpath.
+:-load-vernac-object *qualid*: Load |Coq| compiled library :n:`@qualid`. This
+  is equivalent to running :cmd:`Require` :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.
+  This is equivalent to running :cmd:`Require Export` :n:`@qualid`.
+:-rifrom *dirpath* *qualid*, -require-import-from *dirpath* *qualid*: Load |Coq| compiled library :n:`@qualid` and import it.
+  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
@@ -193,7 +200,7 @@ and ``coqtop``, unless stated otherwise:
 :-emacs, -ide-slave: Start a special toplevel to communicate with a
   specific IDE.
 :-impredicative-set: Change the logical theory of |Coq| by declaring the
-   sort Set impredicative.
+   sort :g:`Set` impredicative.
 
    .. warning::
 
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 4ef31c73b7..9180cae389 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -184,6 +184,10 @@ 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 inputstate = Some s }
@@ -416,7 +420,22 @@ let parse_args ~help ~init arglist : t * string list =
       Flags.profile_ltac_cutoff := get_float opt (next ());
       oval
 
-    |"-require" -> add_vo_require oval (next ()) None (Some false)
+    |"-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)
+
+    |"-require-import-from" | "-rifrom" ->
+      let from = next () in add_vo_require oval (next ()) (Some from) (Some false)
+
+    |"-require-export-from" | "-refrom" ->
+      let from = next () in add_vo_require oval (next ()) (Some from) (Some true)
 
     |"-top" ->
       let topname = Libnames.dirpath_of_string (next ()) in
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 29948d50b2..84d3992f5c 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -44,10 +44,23 @@ let print_usage_common co command =
 \n  -load-ml-source f      load ML file f\
 \n  -load-vernac-source f  load Coq file f.v (Load \"f\".)\
 \n  -l f                   (idem)\
-\n  -require path          load Coq library path and import it (Require Import path.)\
 \n  -load-vernac-source-verbose f  load Coq file f.v (Load Verbose \"f\".)\
 \n  -lv f	           (idem)\
-\n  -load-vernac-object path  load Coq library path (Require path)\
+\n  -load-vernac-object lib, -r lib\
+\n                         load Coq library lib (Require lib)\
+\n  -rfrom root lib        load Coq library lib (From root Require lib.)\
+\n  -require-import lib, -ri lib\
+\n                         load and import Coq library lib\
+\n                         (equivalent to Require Import lib.)\
+\n  -require-export lib, -re lib\
+\n                         load and transitively import Coq library lib\
+\n                         (equivalent to Require Export lib.)\
+\n  -require-import-from root lib, -rifrom lib\
+\n                         load and import Coq library lib\
+\n                         (equivalent to From root Require Import lib.)\
+\n  -require-export-from root lib, -refrom lib\
+\n                         load and transitively import Coq library lib\
+\n                         (equivalent to From root Require Export lib.)\
 \n\
 \n  -where                 print Coq's standard library location and exit\
 \n  -config, --config      print Coq's configuration information and exit\