From cb60825aec0f6ff79b7a7a3f21c1ab4d8e11dae7 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 11 May 2019 22:20:15 +0200 Subject: Command line: adding variants for Require, aligning on the vernac syntax. We deprecate -require (= Require Import) to avoid the confusion with Require. We propose a regular equivalent to all vernac variants in expanded and short version: -require-import, -require-export -require-import-from, -require-export-from -ri, -re -rifrom, -refrom We also add -rfrom, but wait for the end of deprecation of -require to replace -load-vernac-object by -require and to introduce a shorthand -r for the new -require. --- toplevel/coqargs.ml | 21 ++++++++++++++++++++- toplevel/usage.ml | 17 +++++++++++++++-- 2 files changed, 35 insertions(+), 3 deletions(-) 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\ -- cgit v1.2.3 From 5261067a906c190c20d571086692dfb04bc4d0de Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 27 May 2019 17:00:21 +0200 Subject: Documenting new options -require-import, -require-export, etc. Slight improving of style in passing. --- doc/sphinx/practical-tools/coq-commands.rst | 23 +++++++++++++++-------- 1 file changed, 15 insertions(+), 8 deletions(-) diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index bdda35fcc0..3729dcd974 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 -- cgit v1.2.3 From 08a32f04b77b29ad17db75f7ba98c122c31b96aa Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 27 May 2019 17:30:19 +0200 Subject: Mini fix documentation coqtop in passing. --- doc/sphinx/practical-tools/coq-commands.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 3729dcd974..48d5f4075e 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -200,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:: -- cgit v1.2.3 From 6f05a46e08fdb8de2319c36f07a737b1acebfe31 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 27 May 2019 17:23:37 +0200 Subject: Updated changelog. --- doc/changelog/08-tools/10245-require-command-line.rst | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 doc/changelog/08-tools/10245-require-command-line.rst 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 `_ + by Hugo Herbelin, review by Emilio Gallego). -- cgit v1.2.3