pycoq icon indicating copy to clipboard operation
pycoq copied to clipboard

Published 20 hours ago • verified publisher icon ejgallego

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

Open quinn-dougherty opened this issue 3 years ago • 1 comments

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).

quinn-dougherty avatar Nov 05 '21 05:11 quinn-dougherty

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

ejgallego avatar Nov 05 '21 11:11 ejgallego