Skip to content

tomtomjhj/coq.ctags

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

32 Commits
 
 
 
 
 
 
 
 

Repository files navigation

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

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.

Related work

About

Universal Ctags optlib parser for Coq

Topics

Resources

License

Stars

Watchers

Forks

Languages