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

codesmell: breaks when import pycoq is omitted even tho pycoq is not invoked. #11

Open
quinn-dougherty opened this issue Nov 5, 2021 · 1 comment

Comments

@quinn-dougherty
Copy link
Collaborator

when I comment out import pycoq, I get

dune exec -- python3 _build/default/examples/add_commutative.py
Traceback (most recent call last):
  File "_build/default/examples/add_commutative.py", line 2, in <module>
    import coq
ModuleNotFoundError: No module named 'coq'
make: *** [Makefile:14: examples] Error 1

even tho pycoq is not invoked at all in add_commutative.py. This means we are guaranteed to raise the lint message "no unused imports" (unless we ignore that rule, which we do in my upcoming PR).

@ejgallego
Copy link
Owner

I think import pycoq is needed so the .so file with the coq module is loaded?

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

No branches or pull requests

2 participants