Stream: Proof General users

Topic: [company-coq] jmp-to-definition and dune

view this post on Zulip Yannick Zakowski (Apr 07 2023 at 11:51):

Hello,
I have seen the question discussed here and there for a few years but I'm not sure what is the current status: is there a solution to get jmp-to -definition to jump to the source file rather than its read-only copy in _build when working with dune by any chance?

view this post on Zulip Erik Martin-Dorel (Apr 07 2023 at 13:06):

Pinging @Clément Pit-Claudel about this very feature.

In the meantime, you might be interested in the patch submitted in PR https://github.com/cpitclaudel/company-coq/pull/261

view this post on Zulip Emilio Jesús Gallego Arias (Apr 07 2023 at 13:15):

Tuareg in emacs just strips the _build prefix and works pretty well in all OCaml projects, so indeed, I'd recommend doing that (simple and effective)

Last updated: Oct 13 2024 at 01:02 UTC