Coq ctags generation snippet.

gen_ctags.sh

#!/usr/bin/env bash
set -euo pipefail
COMPCERT_SRC=~/temp/CompCert-3.7
CTAGS_DEFINITION=/Users/lightquantum/.config/coq.ctags

# Generate tags for Compcert + stdlib + all files under cwd
IFS=" " read -r -a loadpath <<< "$(echo 'Print LoadPath.' | coqtop 2>/dev/null | python loadpath.py)"
find . ${loadpath[@]} $COMPCERT_SRC -type f -name "*.v" -print0 | xargs -0 ctags --options=$CTAGS_DEFINITION

loadpath.py

#!/usr/bin/env python
import re
import sys

def main():
    # Parse `Print Loadpath` and return loaded coq library names.
    src = "\n".join(sys.stdin.readlines())
    pat = re.compile("^[\w.]+\n? +(\/.+\/[^\n\/]+)", re.MULTILINE);
    print(" ".join(pat.findall(src)))

if __name__ == "__main__":
    main()