pycoq
pycoq copied to clipboard
let `pytest` and `pytype` know about `pycoq.so` somehow, probably by doing some kind of `dune exec -- pytest`
In https://github.com/ejgallego/pycoq/pull/10 I decided to put if __name__ == "__main__":
blocks in the test suite, instead of using test harness pytest
, because I couldn't make pytest
aware of the pycoq
installation.
we also have to cp -r test _build/default/
, which isn't ideal. But it's the minimum viable test suite.
Errors:
$ pytest test
======================================================= ERRORS =======================================================
_______________________________________ ERROR collecting test/py/test_spec.py ________________________________________
test/py/test_spec.py:1: in <module>
import pycoq
pycoq/__init__.py:9: in <module>
dll = PyDLL(f"{curdir}/pycoq.so", RTLD_GLOBAL)
/usr/lib/python3.8/ctypes/__init__.py:373: in __init__
self._handle = _dlopen(self._name, mode)
E OSError: /home/quinn/Dropbox/Projects/misc-coq/pycoq/pycoq/pycoq.so: cannot open shared object file: No such file or directory
============================================== short test summary info ===============================================
pytest _build/default/test
is weirder, the harness says collecting...
then returns me back to the shell, collecting nothing.
I also experimented with the --rootdir
argument to point pytest
to pycoq.so
, no luck.
tox
might be the correct way around it, it's a little more modern than setuptools
anyway.