Wolf Honore (Jul 15 2021 at 17:02): Wolf Honore (Jul 15 2021 at 17:02):Has anyone worked on a tool to generate tag files for Coq (like what ctags creates)? The .glob files look promising, but I think I remember seeing somewhere that their format isn't fixed across versions and shouldn't be relied on? What does coqdoc use to create links to where things are defined?
Théo Zimmermann (Jul 15 2021 at 17:07):I believe it uses the glob files. @Jason Gross also uses this for his bug minimizer. I think the format is somewhat stable.
Bas Spitters (Jul 17 2021 at 07:14):We use etags in HoTT
https://github.com/HoTT/HoTT/blob/master/INSTALL.md#41-tags-for-emacs
Jaehwang Jung (Mar 20 2022 at 16:24):I just wrote a universal-ctags configuration for coq. https://github.com/tomtomjhj/coq.ctags
Last updated: Dec 01 2023 at 06:01 UTC