Definition lookup via TAGS

[wintersteiger]

By simply adding .fst/.fsti to the OCaml parser in universal-ctags, we gain a super-fast tag file generator that allows for super-fast symbol lookup that doesn't require a running F* process.

E.g. ctags -e -R *.fst *.fsti $FSTAR_HOME/ulib/* produces a nice index that emacs can read/search quickly and M-x xref-find-definitions jumps to a definition or, if it's not sure which one to pick, displays a small list of matches within milliseconds.

Worth pursuing? E.g. I think it would need some parser customization so that it gets the right module names/scopes and to differentiate definitions from declarations, etc. For me personally this is going to save me a bunch of time even without further work I think.

@nikswamy @protz @cpitclaudel

[wintersteiger]

Also, as a free bonus, emacs picks up the symbols in those TAGS files for auto-completion.

[cpitclaudel]

Sounds like a good idea. It would be especially nice to generate tags as part of the default build process of the stdlib. And it's great to be able to jump without a running F*.

Have you noticed performance issues with the current jump-to-definition feature though?

For completion I'm not too convinced, since tags don't help much with figuring how to qualify the identifier.

[wintersteiger]

Yeah, exactly what I was thinking, shipping ulib with a TAGS file would be great.

Re performance: not directly with the emacs mode, but it takes a while to spin up an F process and to wait for it to read all the imports. This has gotten better as I recently got a new desktop machine, but it's still annoying. But, much more important than that is that I can only go one level deep before I have to start up another F process for whatever file I just jumped to. This is so much slicker with TAGS that get loaded only once. Even the trivial method of generating a whole new TAGS for everything after opening the first file, is a much better experience!

[cpitclaudel]

But, much more important than that is that I can only go one level deep before I have to start up another F* process for whatever file I just jumped to.

This is arguably a bug; the new buffer should inherit the existing process. Can you create a separate issue for that? :)

[wintersteiger]

Seriously?! This has never worked for me, I just accepted that as normal. I'll open an issue right away.

[s-zanella]

Jumping to a definition in a buffer spawned after looking for a definition in the main buffer never worked for me either and that's something I will find really convenient.

[cpitclaudel]

It's never worked for anyone, because it was never implemented :) But it should be.

[cpitclaudel]

Closing this, since buffers created by jumping now inherit the parent process. Please reopen when/if F* gets a TAGS file