<commit_before>.. _vernacularcommands:

Vernacular commands
=============================

.. _displaying:

Displaying
----------


.. _Print:

.. cmd:: Print {? Term } @smart_qualid {? @univ_name_list }

   .. insertprodn univ_name_list univ_name_list

   .. prodn::
      univ_name_list ::= @%{ {* @name } %}

   Displays definitions of terms, including opaque terms, for the object :n:`@smart_qualid`.

   * :n:`Term` - a syntactic marker to allow printing a term
     that is the same as one of the various :n:`Print` commands.  For example,
     :cmd:`Print All` is a different command, while :n:`Print Term All` shows
     information on the object whose name is ":n:`All`".

   * :n:`@univ_name_list` - locally renames the
     polymorphic universes of :n:`@smart_qualid`.
     The name `_` means the usual name is printed.

   .. exn:: @qualid not a defined object.
      :undocumented:

   .. exn:: Universe instance should have length @num.
      :undocumented:

   .. exn:: This object does not support universe names.
      :undocumented:


.. cmd:: Print All

   This command displays information about the current state of the
   environment, including sections and modules.

.. cmd:: Inspect @num

   This command displays the :n:`@num` last objects of the
   current environment, including sections and modules.

.. cmd:: Print Section @qualid

   Displays the objects defined since the beginning of the section named :n:`@qualid`.

   .. todo: "A.B" is permitted but unnecessary for modules/sections.
      should the command just take an @ident?


.. _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 <set_unset_scope_qualifiers>`.

   .. warn:: There is no option @setting_name.

      This message also appears for unknown flags.

.. 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 <set_unset_scope_qualifiers>`.

.. 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.

.. 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<commit_msg>Document changed warnings and erros following #12038.<commit_after>.. _vernacularcommands:

Vernacular commands
=============================

.. _displaying:

Displaying
----------


.. _Print:

.. cmd:: Print {? Term } @smart_qualid {? @univ_name_list }

   .. insertprodn univ_name_list univ_name_list

   .. prodn::
      univ_name_list ::= @%{ {* @name } %}

   Displays definitions of terms, including opaque terms, for the object :n:`@smart_qualid`.

   * :n:`Term` - a syntactic marker to allow printing a term
     that is the same as one of the various :n:`Print` commands.  For example,
     :cmd:`Print All` is a different command, while :n:`Print Term All` shows
     information on the object whose name is ":n:`All`".

   * :n:`@univ_name_list` - locally renames the
     polymorphic universes of :n:`@smart_qualid`.
     The name `_` means the usual name is printed.

   .. exn:: @qualid not a defined object.
      :undocumented:

   .. exn:: Universe instance should have length @num.
      :undocumented:

   .. exn:: This object does not support universe names.
      :undocumented:


.. cmd:: Print All

   This command displays information about the current state of the
   environment, including sections and modules.

.. cmd:: Inspect @num

   This command displays the :n:`@num` last objects of the
   current environment, including sections and modules.

.. cmd:: Print Section @qualid

   Displays the objects defined since the beginning of the section named :n:`@qualid`.

   .. todo: "A.B" is permitted but unnecessary for modules/sections.
      should the command just take an @ident?


.. _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 <set_unset_scope_qualifiers>`.

   .. 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 <set_unset_scope_qualifiers>`.

.. 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
{'fraction_non_alphanumeric': 0.12693286357408495, 'fraction_numerical': 0.0004893325504012527, 'mean_word_length': 3.4682990817665065, 'pattern_counts': {'":': 2, '<': 7, '<?xml version=': 0, '>': 7, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2882536', 'n_tokens_mistral': 3039, 'n_tokens_neox': 2913, 'n_words': 1258}