\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\In}{\kw{in}} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[4]{\kw{Ind}_{#4}[#1](#2:=#3)} \newcommand{\Indpstr}[5]{\kw{Ind}_{#4}[#1](#2:=#3)/{#5}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} \newcommand{\lra}{\longrightarrow} \newcommand{\Match}{\kw{match}} \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} \newcommand{\ModImp}[3]{{\kw{Mod}}({#1}:{#2}:={#3})} \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} \newcommand{\nO}{\textsf{O}} \newcommand{\node}{\textsf{node}} \newcommand{\nS}{\textsf{S}} \newcommand{\odd}{\textsf{odd}} \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} \newcommand{\plus}{\mathsf{plus}} \newcommand{\SProp}{\textsf{SProp}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\Sort}{\mathcal{S}} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\trii}{\triangleright_\iota} \newcommand{\Type}{\textsf{Type}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)} \newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} \end{split}\]

# Writing Rocq libraries and plugins

This section presents the part of the Rocq language that is useful only to library and plugin authors. A tutorial for writing Rocq plugins is available in the Rocq repository in doc/plugin_tutorial.

## Deprecating library objects, tactics or library files

You may use the following attribute to deprecate a notation, tactic, definition, axiom, theorem or file. When renaming a definition or theorem, you can introduce a deprecated compatibility alias using `Abbreviation` (see the example below).

Attribute deprecated ( since = string ,? note = string ,? use = qualid? )

  At least one of `since` or `note` must be present. If both are present, either one may appear first and they must be separated by a comma. If they are present, they will be used in the warning message, and `since` will also be used in the warning name and categories. Spaces inside `since` are changed to hyphens.

  This attribute is supported by the following commands: `Ltac`, `Tactic Notation`, `Notation`, `Infix`, `Ltac2`, `Ltac2 Notation`, `Ltac2 external`, `Definition`, `Theorem`, and similar commands. To attach it to a compiled library file, use `Attributes`.

  The `use` attribute can be used for commands such as `Definition`, `Theorem`, and `Abbreviation`. Its value must refer to an existing constant or abbreviation and is printed as part of the warning message as well as used by LSP based user interfaces as a quick fix.

  It can trigger the following warnings:

  Warning Library File qualid is deprecated since stringsince. stringnote. Use qualiduse instead.
  Warning Library File (transitively required) qualid is deprecated since stringsince. stringnote. Use qualiduse instead.
  Warning Ltac2 alias qualid is deprecated since stringsince. stringnote.
  Warning Ltac2 definition qualid is deprecated since stringsince. stringnote.
  Warning Ltac2 notation ltac2_syntax_class+ is deprecated since stringsince. stringnote.
  Warning Ltac2 constructor qualid is deprecated since stringsince. stringnote.
  Warning Notation string is deprecated since stringsince. stringnote. Use qualiduse instead.
  Warning Tactic qualid is deprecated since stringsince. stringnote.
  Warning Tactic Notation qualid is deprecated since stringsince. stringnote.

    `qualid` or `string` is the notation, `stringsince` is the version number, `stringnote` is the note (usually explains the replacement).

    Explicitly `Require`ing a file that has been deprecated, using the `Attributes` command, triggers a `Library File` deprecation warning. Requiring a deprecated file, even indirectly through a chain of `Require`s, will produce a `Library File (transitively required)` deprecation warning if the `Warnings` option "deprecated-transitive-library-file" is set (it is "-deprecated-transitive-library-file" by default, silencing the warning).

Note

Rocq and its standard library follow this deprecation policy:

- it should always be possible for a project written in Rocq to be compatible with two successive major versions,

- features must be deprecated in one major version before removal,

- Rocq developers should provide an estimate of the required effort to fix a project with respect to a given change,

- breaking changes should be clearly documented in the public release notes, along with recommendations on how to fix a project if it breaks.

See [Zim19], Section 3.6.3, for more details.

## Triggering warning for library objects or library files

You may use the following attribute to trigger a warning on a notation, definition, axiom, theorem or file.

Attribute warn ( note = string , cats = string? )

  The `note` field will be used as the warning message, and `cats` is a comma separated list of categories to be used in the warning name and categories. Leading and trailing spaces in each category are trimmed, whereas internal spaces are changed to hyphens. If both `note` and `cats` are present, either one may appear first and they must be separated by a comma.

  This attribute is supported by the following commands: `Notation`, `Infix`, `Definition`, `Theorem`, and similar commands. To attach it to a compiled library file, use `Attributes`.

  It can trigger the following warning:

  Warning stringnote

    `stringnote` is the note. It's common practice to start it with a capital and end it with a period.

    Explicitly `Require`ing a file that has a warn message set using the `Attributes` command, triggers a `warn-library-file` warning. Requiring such a file, even indirectly through a chain of `Require`s, will produce a `warn-transitive-library-file` warning if the `Warnings` option "warn-transitive-library-file" is set (it is "-warn-transitive-library-file" by default, silencing the warning).

Example: Deprecating a tactic.

#[deprecated(since="mylib 0.9", note="Use idtac instead.")] Ltac foo := idtac.
  foo is defined
Goal True.
  1 goal ============================ True
Proof.
now foo.
  Toplevel input, characters 4-7: > now foo. > ^^^ Warning: Tactic foo is deprecated since mylib 0.9. Use idtac instead. [deprecated-tactic-since-mylib-0.9,deprecated-since-mylib-0.9,deprecated-tactic,deprecated,default] No more goals.

Example: Introducing a compatibility alias

Let's say your library initially contained:

Definition foo x := S x.
  foo is defined

and you want to rename `foo` into `bar`, but you want to avoid breaking your users' code without advanced notice. To do so, replace the previous code by the following:

Definition bar x := S x.
  bar is defined
#[deprecated(since="mylib 1.2", note="Use bar instead.")] Abbreviation foo := bar (only parsing).

Then, the following code still works, but emits a warning:

Check (foo 0).
  Toplevel input, characters 7-10: > Check (foo 0). > ^^^ Warning: Notation foo is deprecated since mylib 1.2. Use bar instead. [deprecated-syntactic-definition-since-mylib-1.2,deprecated-since-mylib-1.2,deprecated-syntactic-definition,deprecated,default] bar 0 : nat

Other versions v: 9.2

Versions
  dev
  stable
  9.2
  9.1
  9.0
  8.20
  8.19
  8.18
  8.17
  8.16
  8.15
  8.14
  8.13
  8.12
  8.11
  8.10
  8.9
  8.8
  8.7
  8.6
  8.5
  8.4
  8.3
  8.2
  8.1
  8.0

Downloads
  PDF