\[\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}\]
Libraries and plugins
Libraries and plugins contain compiled Coq scripts with useful definitions,
theorems, notations and settings that can be loaded at runtime. In addition,
plugins can add new tactics and commands written in OCaml.
Coq is distributed with a standard library and a set of internal
plugins (most of which provide tactics that have already been
presented in Basic proof writing). This chapter presents this
standard library and some of these internal plugins which provide
features that are not tactics.
In addition, Coq has a rich ecosystem of external libraries and
plugins. These libraries and plugins can be browsed online through
the Coq Package Index and
installed with the opam package manager.
Libraries contain only compiled Coq scripts.
Plugins can also include compiled OCaml code that can change
the behavior of Coq. Both are packages.
While users configure and load them identically, there are a few differences
to consider:
Nearly all plugins add functionality that could not be added otherwise
and they likely add new top-level commands or tactics.
Compared to libraries, plugins can change Coq's behavior in many possibly
unexpected ways. Therefore, using a plugin requires a higher degree of trust
in its authors than is needed for libraries. If desired, you can mitigate
trust issues by running Compiled libraries checker (coqchk) on compiled files produced from Coq
scripts that load plugins. (coqchk doesn't load plugins, so they won't be
part of trusted code base.)
Plugins that aren't in Coq's
CI (continuous integration) system
are more likely
to break across major versions due to source code changes to Coq. You may want to
consider this before adopting a new plugin for your project.