Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Strip _build/default when locating files #257

Open
wants to merge 1 commit into
base: master
Choose a base branch
from

Conversation

MackieLoeffel
Copy link

This PR upstreams the heuristic to locate the right file for projects using dune from ProofGeneral/PG#477 (comment).

I don't really understand what exactly is going on in company-coq-library-path and this PR is just a naive adaptation of the code linked above. Please feel free to suggest better ways to write this code. I am also not sure if one should allow customization of which parts should be stripped (e.g. allow the user to give a regex that should be removed).

@Blaisorblade
Copy link

Do you still extend _CoqProject by hand to use this? Is this just about opening the original source instead of dune’s copy in jump-to-definition?

@MackieLoeffel
Copy link
Author

MackieLoeffel commented Jan 6, 2022

This just addresses the second point (jumping to the original source instead of dune's copy in jump-to-definition). You still need to have a _CoqProject file with the right paths.

@aa755
Copy link
Contributor

aa755 commented Jul 20, 2022

this works when I jump to definition for a definition/inductive etc. However, it doesnt work when I jump to definition on a line of the form "Require Import x.y.z". It seems the handling of that doesnt even touch the codepath changed in this MR.

aa755 added a commit to aa755/company-coq that referenced this pull request Jul 20, 2022
@Blaisorblade
Copy link

Thanks for fixing this @aa755 in master...aa755:company-coq:strip-build-dir, would you be okay submitting that as an MR?

@cpitclaudel Is there anyway we can help progress on this MR?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants