Skip to content

Conversation

ali-ghanbari
Copy link
Contributor

Hi,
Thanks for creating this extremely useful tool.
During my experiments with CoqPyt, I realized that I cannot pass physical-to-logical path mapping options (-Q/-R) to Coq-LSP.
I have added an (optional) extra parameter for some of the classes to accept extra parameters from the client code.
Let me know if you need further clarification/refactoring.

Copy link
Member

@Nfsaavedra Nfsaavedra left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hi @ali-ghanbari! Thanks for your interest in our tool and for the contribution! Overall the code LGTM, however there are two issues:

  1. The linter step of the CI is failing. Please use black to format the files so this step does not fail.
  2. The tests are failing. I think all the failures are related to the same problem. You can see the logs here. I had to cancel these jobs because they wouldn't finish. I think one process is hanging due to the errors.

Copy link
Member

@Nfsaavedra Nfsaavedra left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM! I'll merge! Thanks!

@Nfsaavedra Nfsaavedra merged commit 75a3cca into sr-lab:master May 4, 2025
5 checks passed
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