Awesome

coq.ctags

coq.ctags is a Universal Ctags configuration ("optlib parser") for Coq.

Features

• Supports most built-in commands that define some identifiers.
• Supports unicode identifiers.
• Doesn't get confused by string, comments, attributes, etc.

Not supported (yet)

• Axiom, Conjecture, Parameter, Hypothesis, Variable
• Theorem ... with, Record ... with (Inductive ... with and Fixpoint ... with are supported)
• Automatically generated identifiers
  • Build_XXX
  • XXX_ind, ...
• constructors_or_record
• Notations
  • basic notation
  • tactic notation
  • (Abbreviations are supported)
• ... ?

Caveat

• Assumes that parentheses/braces/brackets in terms are well-balanced.
• Notations that contain ; confuses record field parsing. This results in some unwanted tag entries.

Requirements

A recent version of Universal Ctags with +pcre2 feature is required.

$ ctags --list-features
#NAME             DESCRIPTION
...
pcre2             has pcre2 regex engine
...

You may need to build Universal Ctags from source. In that case, to enable pcre2, run the configure script like so: ./configure --enable-pcre2.

Usage

$ ctags --options=/path/to/coq.ctags [options] [file(s)]

Some notable [options]:

• -R: Recurse into directories
• -e: Output TAGS file for Emacs
• -V: Verbose output for debugging

Please see ctags(1) for more details.

Example usage with fd:

$ fd -e v -X ctags --options=/path/to/coq.ctags

Implementation

coq.ctags uses some experimental features of Universal Ctags.

• PCRE2
• Multiple regex table
• (Not used yet, but would be necessary for adding support for more Coq features) Optscript

Related work

• etags configuration from HoTT project
• coqtags Perl script from Proof General
• coqdoc uses .glob files to generate hyperlinks.