Stream: Miscellaneous

Topic: ctags for Coq

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Bas Spitters (Jul 17 2021 at 07:14):

We use etags in HoTT

view this post on Zulip Jaehwang Jung (Mar 20 2022 at 16:24):

I just wrote a universal-ctags configuration for coq.

Last updated: May 24 2024 at 22:02 UTC