From 9eb788ebca0305fc72940c92b9ae35bbaca56c5c Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Fri, 1 May 2020 13:00:52 +0200 Subject: Create section on basics with just lexical conventions and attributes. --- doc/sphinx/language/core/basic.rst | 134 +++++++++++++++++++++++++++++++++++++ 1 file changed, 134 insertions(+) create mode 100644 doc/sphinx/language/core/basic.rst (limited to 'doc/sphinx/language/core/basic.rst') diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst new file mode 100644 index 0000000000..4fadc8da02 --- /dev/null +++ b/doc/sphinx/language/core/basic.rst @@ -0,0 +1,134 @@ +.. _lexical-conventions: + +Lexical conventions +=================== + +Blanks + Space, newline and horizontal tab are considered blanks. + Blanks are ignored but they separate tokens. + +Comments + Comments are enclosed between ``(*`` and ``*)``. They can be nested. + They can contain any character. However, embedded :n:`@string` literals must be + correctly closed. Comments are treated as blanks. + +Identifiers + Identifiers, written :n:`@ident`, are sequences of letters, digits, ``_`` and + ``'``, that do not start with a digit or ``'``. That is, they are + recognized by the following grammar (except that the string ``_`` is reserved; + it is not a valid identifier): + + .. insertprodn ident subsequent_letter + + .. prodn:: + ident ::= @first_letter {* @subsequent_letter } + first_letter ::= {| a .. z | A .. Z | _ | @unicode_letter } + subsequent_letter ::= {| @first_letter | @digit | ' | @unicode_id_part } + + All characters are meaningful. In particular, identifiers are case-sensitive. + :production:`unicode_letter` non-exhaustively includes Latin, + Greek, Gothic, Cyrillic, Arabic, Hebrew, Georgian, Hangul, Hiragana + and Katakana characters, CJK ideographs, mathematical letter-like + symbols and non-breaking space. :production:`unicode_id_part` + non-exhaustively includes symbols for prime letters and subscripts. + +Numerals + Numerals are sequences of digits with an optional fractional part + and exponent, optionally preceded by a minus sign. :n:`@int` is an integer; + a numeral without fractional or exponent parts. :n:`@num` is a non-negative + integer. Underscores embedded in the digits are ignored, for example + ``1_000_000`` is the same as ``1000000``. + + .. insertprodn numeral digit + + .. prodn:: + numeral ::= {+ @digit } {? . {+ @digit } } {? {| e | E } {? {| + | - } } {+ @digit } } + int ::= {? - } {+ @digit } + num ::= {+ @digit } + digit ::= 0 .. 9 + +Strings + Strings begin and end with ``"`` (double quote). Use ``""`` to represent + a double quote character within a string. In the grammar, strings are + identified with :production:`string`. + +Keywords + The following character sequences are reserved keywords that cannot be + used as identifiers:: + + _ Axiom CoFixpoint Definition Fixpoint Hypothesis IF Parameter Prop + SProp Set Theorem Type Variable as at by cofix discriminated else + end exists exists2 fix for forall fun if in lazymatch let match + multimatch return then using where with + + Note that plugins may define additional keywords when they are loaded. + +Other tokens + The set of + tokens defined at any given time can vary because the :cmd:`Notation` + command can define new tokens. A :cmd:`Require` command may load more notation definitions, + while the end of a :cmd:`Section` may remove notations. Some notations + are defined in the basic library (see :ref:`thecoqlibrary`) and are normally + loaded automatically at startup time. + + Here are the character sequences that Coq directly defines as tokens + without using :cmd:`Notation` (omitting 25 specialized tokens that begin with + ``#int63_``):: + + ! #[ % & ' ( () (bfs) (dfs) ) * ** + , - -> + . .( .. ... / : ::= := :> :>> ; < <+ <- <: + <<: <= = => > >-> >= ? @ @{ [ [= ] _ + `( `{ { {| | |- || } + + When multiple tokens match the beginning of a sequence of characters, + the longest matching token is used. + Occasionally you may need to insert spaces to separate tokens. For example, + if ``~`` and ``~~`` are both defined as tokens, the inputs ``~ ~`` and + ``~~`` generate different tokens, whereas if `~~` is not defined, then the + two inputs are equivalent. + +.. _gallina-attributes: + +Attributes +----------- + +.. insertprodn all_attrs legacy_attr + +.. prodn:: + all_attrs ::= {* #[ {*, @attr } ] } {* @legacy_attr } + attr ::= @ident {? @attr_value } + attr_value ::= = @string + | ( {*, @attr } ) + legacy_attr ::= {| Local | Global } + | {| Polymorphic | Monomorphic } + | {| Cumulative | NonCumulative } + | Private + | Program + +Attributes modify the behavior of a command or tactic. +Syntactically, most commands and tactics can be decorated with attributes, but +attributes not supported by the command or tactic will be flagged as errors. + +The order of top-level attributes doesn't affect their meaning. ``#[foo,bar]``, ``#[bar,foo]``, +``#[foo]#[bar]`` and ``#[bar]#[foo]`` are equivalent. + +The legacy attributes (:n:`@legacy_attr`) provide an older, alternate syntax +for certain attributes. They are equivalent to new attributes as follows: + +================ ================================ +Legacy attribute New attribute +================ ================================ +`Local` :attr:`local` +`Global` :attr:`global` +`Polymorphic` :attr:`universes(polymorphic)` +`Monomorphic` :attr:`universes(monomorphic)` +`Cumulative` :attr:`universes(cumulative)` +`NonCumulative` :attr:`universes(noncumulative)` +`Private` :attr:`private(matching)` +`Program` :attr:`program` +================ ================================ + +.. warn:: Unsupported attribute + + This warning is an error by default. It is caused by using a + command with some attribute it does not understand. -- cgit v1.2.3 From a42cf3402094e6f7ce019243edfc6b6137de011a Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Fri, 1 May 2020 13:03:08 +0200 Subject: Create section on basics with just flags, options and tables. --- doc/sphinx/language/core/basic.rst | 127 +++++++++++++++++++++++++++++++++++++ 1 file changed, 127 insertions(+) create mode 100644 doc/sphinx/language/core/basic.rst (limited to 'doc/sphinx/language/core/basic.rst') diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst new file mode 100644 index 0000000000..66a955e48d --- /dev/null +++ b/doc/sphinx/language/core/basic.rst @@ -0,0 +1,127 @@ +.. _flags-options-tables: + +Flags, Options and Tables +----------------------------- + +Coq has many settings to control its behavior. Setting types include flags, options +and tables: + +* A *flag* has a boolean value, such as :flag:`Asymmetric Patterns`. +* An *option* generally has a numeric or string value, such as :opt:`Firstorder Depth`. +* A *table* contains a set of strings or qualids. +* In addition, some commands provide settings, such as :cmd:`Extraction Language`. + +.. FIXME Convert "Extraction Language" to an option. + +Flags, options and tables are identified by a series of identifiers, each with an initial +capital letter. + +.. cmd:: Set @setting_name {? {| @int | @string } } + :name: Set + + .. insertprodn setting_name setting_name + + .. prodn:: + setting_name ::= {+ @ident } + + If :n:`@setting_name` is a flag, no value may be provided; the flag + is set to on. + If :n:`@setting_name` is an option, a value of the appropriate type + must be provided; the option is set to the specified value. + + This command supports the :attr:`local`, :attr:`global` and :attr:`export` attributes. + They are described :ref:`here `. + + .. warn:: There is no flag or option with this name: "@setting_name". + + This warning message can be raised by :cmd:`Set` and + :cmd:`Unset` when :n:`@setting_name` is unknown. It is a + warning rather than an error because this helps library authors + produce Coq code that is compatible with several Coq versions. + To preserve the same behavior, they may need to set some + compatibility flags or options that did not exist in previous + Coq versions. + +.. cmd:: Unset @setting_name + :name: Unset + + If :n:`@setting_name` is a flag, it is set to off. If :n:`@setting_name` is an option, it is + set to its default value. + + This command supports the :attr:`local`, :attr:`global` and :attr:`export` attributes. + They are described :ref:`here `. + +.. cmd:: Add @setting_name {+ {| @qualid | @string } } + + Adds the specified values to the table :n:`@setting_name`. + +.. cmd:: Remove @setting_name {+ {| @qualid | @string } } + + Removes the specified value from the table :n:`@setting_name`. + +.. cmd:: Test @setting_name {? for {+ {| @qualid | @string } } } + + If :n:`@setting_name` is a flag or option, prints its current value. + If :n:`@setting_name` is a table: if the `for` clause is specified, reports + whether the table contains each specified value, otherise this is equivalent to + :cmd:`Print Table`. The `for` clause is not valid for flags and options. + + .. exn:: There is no flag, option or table with this name: "@setting_name". + + This error message is raised when calling the :cmd:`Test` + command (without the `for` clause), or the :cmd:`Print Table` + command, for an unknown :n:`@setting_name`. + + .. exn:: There is no qualid-valued table with this name: "@setting_name". + There is no string-valued table with this name: "@setting_name". + + These error messages are raised when calling the :cmd:`Add` or + :cmd:`Remove` commands, or the :cmd:`Test` command with the + `for` clause, if :n:`@setting_name` is unknown or does not have + the right type. + +.. cmd:: Print Options + + Prints the current value of all flags and options, and the names of all tables. + +.. cmd:: Print Table @setting_name + + Prints the values in the table :n:`@setting_name`. + +.. cmd:: Print Tables + + A synonym for :cmd:`Print Options`. + +.. _set_unset_scope_qualifiers: + +Locality attributes supported by :cmd:`Set` and :cmd:`Unset` +```````````````````````````````````````````````````````````` + +The :cmd:`Set` and :cmd:`Unset` commands support the :attr:`local`, +:attr:`global` and :attr:`export` locality attributes: + +* no attribute: the original setting is *not* restored at the end of + the current module or section. +* :attr:`local` (an alternative syntax is to use the ``Local`` + prefix): the setting is applied within the current module or + section. The original value of the setting is restored at the end + of the current module or section. +* :attr:`export` (an alternative syntax is to use the ``Export`` + prefix): similar to :attr:`local`, the original value of the setting + is restored at the end of the current module or section. In + addition, if the value is set in a module, then :cmd:`Import`\-ing + the module sets the option or flag. +* :attr:`global` (an alternative syntax is to use the ``Global`` + prefix): the original setting is *not* restored at the end of the + current module or section. In addition, if the value is set in a + file, then :cmd:`Require`\-ing the file sets the option. + +Newly opened modules and sections inherit the current settings. + +.. note:: + + The use of the :attr:`global` attribute with the :cmd:`Set` and + :cmd:`Unset` commands is discouraged. If your goal is to define + project-wide settings, you should rather use the command-line + arguments ``-set`` and ``-unset`` for setting flags and options + (cf. :ref:`command-line-options`). -- cgit v1.2.3 From 90285ff50290a49d20d60ffc59725bf87c6acd14 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Fri, 1 May 2020 13:22:42 +0200 Subject: Move essential vocabulary and syntax conventions to section on basics. --- doc/sphinx/language/core/basic.rst | 354 ++++++++++++++++++++++++++++++++----- 1 file changed, 306 insertions(+), 48 deletions(-) (limited to 'doc/sphinx/language/core/basic.rst') diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index 03da59e0bf..9473cc5a15 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -1,7 +1,84 @@ +============================= +Basic notions and conventions +============================= + +This section provides some essential notions and conventions for reading +the manual. + +We start by explaining the syntax and lexical conventions used in the +manual. Then, we present the essential vocabulary necessary to read +the rest of the manual. Other terms are defined throughout the manual. +The reader may refer to the :ref:`glossary index ` +for a complete list of defined terms. Finally, we describe the various types of +settings that |Coq| provides. + +Syntax and lexical conventions +------------------------------ + +Syntax conventions +~~~~~~~~~~~~~~~~~~ + +The syntax described in this documentation is equivalent to that +accepted by the |Coq| parser, but the grammar has been edited +to improve readability and presentation. + +In the grammar presented in this manual, the terminal symbols are +black (e.g. :n:`forall`), whereas the nonterminals are green, italic +and hyperlinked (e.g. :n:`@term`). Some syntax is represented +graphically using the following kinds of blocks: + +:n:`{? item }` + An optional item. + +:n:`{+ item }` + A list of one or more items. + +:n:`{* item }` + An optional list of items. + +:n:`{+s item}` + A list of one or more items separated by "s" (e.g. :n:`item__1 s item__2 s item__3`). + +:n:`{*s item}` + An optional list of items separated by "s". + +:n:`{| item__1 | item__2 | ... }` + Alternatives (either :n:`item__1` or :n:`item__2` or ...). + +`Precedence levels +`_ that are +implemented in the |Coq| parser are shown in the documentation by +appending the level to the nonterminal name (as in :n:`@term100` or +:n:`@ltac_expr3`). + +.. note:: + + |Coq| uses an extensible parser. Plugins and the :ref:`notation + system ` can extend the + syntax at run time. Some notations are defined in the prelude, + which is loaded by default. The documented grammar doesn't include + these notations. Precedence levels not used by the base grammar + are omitted from the documentation, even though they could still be + populated by notations or plugins. + + Furthermore, some parsing rules are only activated in certain + contexts (:ref:`interactive proof mode `, + :ref:`custom entries `...). + +.. warning:: + + Given the complexity of these parsing rules, it would be extremely + difficult to create an external program that can properly parse a + |Coq| document. Therefore, tool writers are advised to delegate + parsing to |Coq|, by communicating with it, for instance through + `SerAPI `_. + +.. seealso:: :cmd:`Print Grammar` + .. _lexical-conventions: Lexical conventions -=================== +~~~~~~~~~~~~~~~~~~~ Blanks Space, newline and horizontal tab are considered blanks. @@ -56,24 +133,22 @@ Keywords The following character sequences are reserved keywords that cannot be used as identifiers:: - _ Axiom CoFixpoint Definition Fixpoint Hypothesis IF Parameter Prop - SProp Set Theorem Type Variable as at by cofix discriminated else - end exists exists2 fix for forall fun if in lazymatch let match - multimatch return then using where with + _ Axiom CoFixpoint Definition Fixpoint Hypothesis Parameter Prop + SProp Set Theorem Type Variable as at cofix discriminated else end + fix for forall fun if in let match return then where with - Note that plugins may define additional keywords when they are loaded. + Note that notations and plugins may define additional keywords. Other tokens The set of tokens defined at any given time can vary because the :cmd:`Notation` command can define new tokens. A :cmd:`Require` command may load more notation definitions, while the end of a :cmd:`Section` may remove notations. Some notations - are defined in the basic library (see :ref:`thecoqlibrary`) and are normally + are defined in the standard library (see :ref:`thecoqlibrary`) and are generally loaded automatically at startup time. - Here are the character sequences that Coq directly defines as tokens - without using :cmd:`Notation` (omitting 25 specialized tokens that begin with - ``#int63_``):: + Here are the character sequences that |Coq| directly defines as tokens + without using :cmd:`Notation`:: ! #[ % & ' ( () (bfs) (dfs) ) * ** + , - -> . .( .. ... / : ::= := :> :>> ; < <+ <- <: @@ -87,28 +162,190 @@ Other tokens ``~~`` generate different tokens, whereas if `~~` is not defined, then the two inputs are equivalent. -.. _gallina-attributes: +Essential vocabulary +-------------------- + +This section presents the most essential notions to understand the +rest of the |Coq| manual: :term:`terms ` and :term:`types +` on the one hand, :term:`commands ` and :term:`tactics +` on the other hand. + +.. glossary:: + + term + + Terms are the basic expressions of |Coq|. Terms can represent + mathematical expressions, propositions and proofs, but also + executable programs and program types. + + Here is the top-level syntax of terms. Each of the listed + constructs is presented in a dedicated section. Some of these + constructs (like :n:`@term_forall_or_fun`) are part of the core + language that the kernel of |Coq| understands and are therefore + described in :ref:`this chapter `, while + others (like :n:`@term_if`) are language extensions that are + presented in :ref:`the next chapter `. + + .. insertprodn term qualid_annotated + + .. prodn:: + term ::= @term_forall_or_fun + | @term_let + | @term_if + | @term_fix + | @term_cofix + | @term100 + term100 ::= @term_cast + | @term10 + term10 ::= @term_application + | @one_term + one_term ::= @term_explicit + | @term1 + term1 ::= @term_projection + | @term_scope + | @term0 + term0 ::= @qualid_annotated + | @sort + | @primitive_notations + | @term_evar + | @term_match + | @term_record + | @term_generalizing + | @term_ltac + | ( @term ) + qualid_annotated ::= @qualid {? @univ_annot } + + .. note:: + + Many :term:`commands ` and :term:`tactics ` + use :n:`@one_term` (in the syntax of their arguments) rather + than :n:`@term`. The former need to be enclosed in + parentheses unless they're very simple, such as a single + identifier. This avoids confusing a space-separated list of + terms or identifiers with a :n:`@term_application`. + + type + + To be valid and accepted by the |Coq| kernel, a term needs an + associated type. We express this relationship by “:math:`x` *of + type* :math:`T`”, which we write as “:math:`x:T`”. Informally, + “:math:`x:T`” can be thought as “:math:`x` *belongs to* + :math:`T`”. + + The |Coq| kernel is a type checker: it verifies that a term has + the expected type by applying a set of typing rules (see + :ref:`Typing-rules`). If that's indeed the case, we say that the + term is :gdef:`well-typed`. + + A special feature of the |Coq| language is that types can depend + on terms (we say that the language is `dependently-typed + `_). Because of + this, types and terms share a common syntax. All types are terms, + but not all terms are types: + + .. insertprodn type type + + .. prodn:: + type ::= @term + + Intuitively, types may be viewed as sets containing terms. We + say that a type is :gdef:`inhabited` if it contains at least one + term (i.e. if we can find a term which is associated with this + type). We call such terms :gdef:`witness`\es. Note that deciding + whether a type is inhabited is `undecidable + `_. + + Formally, types can be used to construct logical foundations for + mathematics alternative to the standard `"set theory" + `_: we call such + logical foundations `"type theories" + `_. |Coq| is based on + the Calculus of Inductive Constructions, which is a particular + instance of type theory. + + sentence + + |Coq| documents are made of a series of sentences that contain + :term:`commands ` or :term:`tactics `, generally + terminated with a period and optionally decorated with + :term:`attributes `. + + .. insertprodn document sentence + + .. prodn:: + document ::= {* @sentence } + sentence ::= {? @attributes } @command . + | {? @attributes } {? @num : } @query_command . + | {? @attributes } {? @toplevel_selector } @ltac_expr {| . | ... } + | @control_command + + :n:`@ltac_expr` syntax supports both simple and compound + :term:`tactics `. For example: ``split`` is a simple + tactic while ``split; auto`` combines two simple tactics. + + command + + A :production:`command` can be used to modify the state of a |Coq| + document, for instance by declaring a new object, or to get + information about the current state. + + By convention, command names begin with uppercase letters. + Commands appear in the HTML documentation in blue or gray boxes + after the label "Command". In the pdf, they appear after the + boldface label "Command:". Commands are listed in the + :ref:`command_index`. Example: + + .. cmd:: Comments {* @string } + + This command prints "Comments ok" and does not change anything + to the state of the document. + + tactic + + Tactics specify how to transform the current proof state as a + step in creating a proof. They are syntactically valid only when + |Coq| is in proof mode, such as after a :cmd:`Theorem` command + and before any subsequent proof-terminating command such as + :cmd:`Qed`. See :ref:`proofhandling` for more on proof mode. + + By convention, tactic names begin with lowercase letters. Tactic + appear in the HTML documentation in blue or gray boxes after the + label "Tactic". In the pdf, they appear after the boldface label + "Tactic:". Tactics are listed in the :ref:`tactic_index`. + +Settings +-------- + +There are several mechanisms for changing the behavior of |Coq|. The +:term:`attribute` mechanism is used to modify the behavior of a single +:term:`sentence`. The :term:`flag`, :term:`option` and :term:`table` +mechanisms are used to modify the behavior of |Coq| more globally in a +document or project. + +.. _attributes: Attributes ------------ +~~~~~~~~~~ + +An :gdef:`attribute` modifies the behavior of a single sentence. +Syntactically, most commands and tactics can be decorated with +attributes (cf. :n:`@sentence`), but attributes not supported by the +command or tactic will trigger :warn:`This command does not support +this attribute`. -.. insertprodn all_attrs legacy_attr +.. insertprodn attributes legacy_attr .. prodn:: - all_attrs ::= {* #[ {*, @attr } ] } {* @legacy_attr } - attr ::= @ident {? @attr_value } + attributes ::= {* #[ {*, @attribute } ] } {* @legacy_attr } + attribute ::= @ident {? @attr_value } attr_value ::= = @string - | ( {*, @attr } ) + | ( {*, @attribute } ) legacy_attr ::= {| Local | Global } | {| Polymorphic | Monomorphic } | {| Cumulative | NonCumulative } | Private | Program -Attributes modify the behavior of a command or tactic. -Syntactically, most commands and tactics can be decorated with attributes, but -attributes not supported by the command or tactic will be flagged as errors. - The order of top-level attributes doesn't affect their meaning. ``#[foo,bar]``, ``#[bar,foo]``, ``#[foo]#[bar]`` and ``#[bar]#[foo]`` are equivalent. @@ -128,22 +365,38 @@ Legacy attribute New attribute `Program` :attr:`program` ================ ================================ -.. warn:: Unsupported attribute +Attributes appear in the HTML documentation in blue or gray boxes +after the label "Attribute". In the pdf, they appear after the +boldface label "Attribute:". Attributes are listed in the +:ref:`attribute_index`. + +.. warn:: This command does not support this attribute: @ident. + :name: This command does not support this attribute + + This warning is configured to behave as an error by default. You + may turn it into a normal warning by using the :opt:`Warnings` option: + + .. coqtop:: none - This warning is an error by default. It is caused by using a - command with some attribute it does not understand. + Set Silent. + + .. coqtop:: all warn + + Set Warnings "unsupported-attributes". + #[ foo ] Comments. .. _flags-options-tables: Flags, Options and Tables ------------------------------ +~~~~~~~~~~~~~~~~~~~~~~~~~ -Coq has many settings to control its behavior. Setting types include flags, options -and tables: +The following types of settings can be used to change the behavior of |Coq| in +subsequent commands and tactics (see :ref:`set_unset_scope_qualifiers` for a +more precise description of the scope of these settings): -* A *flag* has a boolean value, such as :flag:`Asymmetric Patterns`. -* An *option* generally has a numeric or string value, such as :opt:`Firstorder Depth`. -* A *table* contains a set of strings or qualids. +* A :gdef:`flag` has a boolean value, such as :flag:`Universe Polymorphism`. +* An :gdef:`option` generally has a numeric or string value, such as :opt:`Firstorder Depth`. +* A :gdef:`table` contains a set of :token:`string`\s or :token:`qualid`\s. * In addition, some commands provide settings, such as :cmd:`Extraction Language`. .. FIXME Convert "Extraction Language" to an option. @@ -151,6 +404,11 @@ and tables: Flags, options and tables are identified by a series of identifiers, each with an initial capital letter. +Flags, options and tables appear in the HTML documentation in blue or +gray boxes after the labels "Flag", "Option" and "Table". In the pdf, +they appear after a boldface label. They are listed in the +:ref:`options_index`. + .. cmd:: Set @setting_name {? {| @int | @string } } :name: Set @@ -172,10 +430,10 @@ capital letter. This warning message can be raised by :cmd:`Set` and :cmd:`Unset` when :n:`@setting_name` is unknown. It is a warning rather than an error because this helps library authors - produce Coq code that is compatible with several Coq versions. + produce |Coq| code that is compatible with several |Coq| versions. To preserve the same behavior, they may need to set some compatibility flags or options that did not exist in previous - Coq versions. + |Coq| versions. .. cmd:: Unset @setting_name :name: Unset @@ -198,7 +456,7 @@ capital letter. If :n:`@setting_name` is a flag or option, prints its current value. If :n:`@setting_name` is a table: if the `for` clause is specified, reports - whether the table contains each specified value, otherise this is equivalent to + whether the table contains each specified value, otherwise this is equivalent to :cmd:`Print Table`. The `for` clause is not valid for flags and options. .. exn:: There is no flag, option or table with this name: "@setting_name". @@ -230,33 +488,33 @@ capital letter. .. _set_unset_scope_qualifiers: Locality attributes supported by :cmd:`Set` and :cmd:`Unset` -```````````````````````````````````````````````````````````` +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ The :cmd:`Set` and :cmd:`Unset` commands support the :attr:`local`, :attr:`global` and :attr:`export` locality attributes: * no attribute: the original setting is *not* restored at the end of the current module or section. -* :attr:`local` (an alternative syntax is to use the ``Local`` - prefix): the setting is applied within the current module or - section. The original value of the setting is restored at the end - of the current module or section. -* :attr:`export` (an alternative syntax is to use the ``Export`` - prefix): similar to :attr:`local`, the original value of the setting - is restored at the end of the current module or section. In - addition, if the value is set in a module, then :cmd:`Import`\-ing - the module sets the option or flag. -* :attr:`global` (an alternative syntax is to use the ``Global`` - prefix): the original setting is *not* restored at the end of the - current module or section. In addition, if the value is set in a - file, then :cmd:`Require`\-ing the file sets the option. +* :attr:`local` (or alternatively, the ``Local`` prefix): the setting + is applied within the current module or section. The original value + of the setting is restored at the end of the current module or + section. +* :attr:`export` (or alternatively, the ``Export`` prefix): similar to + :attr:`local`, the original value of the setting is restored at the + end of the current module or section. In addition, if the value is + set in a module, then :cmd:`Import`\-ing the module sets the option + or flag. +* :attr:`global` (or alternatively, the ``Global`` prefix): the + original setting is *not* restored at the end of the current module + or section. In addition, if the value is set in a file, then + :cmd:`Require`\-ing the file sets the option. Newly opened modules and sections inherit the current settings. .. note:: - The use of the :attr:`global` attribute with the :cmd:`Set` and - :cmd:`Unset` commands is discouraged. If your goal is to define + We discourage using the :attr:`global` attribute with the :cmd:`Set` and + :cmd:`Unset` commands. If your goal is to define project-wide settings, you should rather use the command-line arguments ``-set`` and ``-unset`` for setting flags and options (cf. :ref:`command-line-options`). -- cgit v1.2.3