a nix build and testing infra

[quinn-dougherty]

TODO:

• fix everything so I can get the thing to run
• implement some basic pytest stuff.

[quinn-dougherty]

If the nix stuff works we'll have made a lot of progress on #1, but not enough to close it. Still, in an upcoming push I changed setup.py a lot. I'm also thinking of migrating to setup.cfg

[quinn-dougherty]

Python version of #7 is in an upcoming push.

[quinn-dougherty]

lmao, dune exec -- python3 test/py/unit/spec.py was working perfectly a second ago and suddenly stopped working.

[ejgallego]

lmao, dune exec -- python3 test/py/unit/spec.py was working perfectly a second ago and suddenly stopped working.

@quinn-dougherty , what is the error message? Note that dune exec -- cmd is a bit of a special command, it basically:

• sets up the ocaml path enviroment, needed in our case as we have OCaml plugins in Coq, so PyCoq knows how to locate them
• if dune knows about cmd, then it will build cmd
• if it doesn't know about cmd, then it won't build it

Note that dune exec doesn't build any other stuff needed for the python3 call. I bet that's the problem!

So for example, dune exec -- python test.py will fail after a dune clean, however it will succeed after a dune build.

In the dune world this is fixed by letting dune manage the tests, so you have something like:

(rule
  (targets test_output.log)
  (deps pycoq.so test.py)
  (action (run python3 test.py)))

This is cool as this way your test suite can be run incrementally!

How to best integrate this into python, I'm unsure.

[quinn-dougherty]

ok that's good info. I'm being careful to run it after the dune build.

quinn@Latitude-3340:~/Dropbox/Projects/misc-coq/pycoq$ dune exec -- python3 test/py/unit/spec.py 
Traceback (most recent call last):
  File "test/py/unit/spec.py", line 1, in <module>
    import pycoq
  File "/home/quinn/.local/lib/python3.8/site-packages/pycoq/__init__.py", line 9, in <module>
    dll = PyDLL(f"{curdir}/pycoq.so", RTLD_GLOBAL)
  File "/usr/lib/python3.8/ctypes/__init__.py", line 373, in __init__
    self._handle = _dlopen(self._name, mode)
OSError: /home/quinn/.local/lib/python3.8/site-packages/pycoq/pycoq.so: cannot open shared object file: No such file or directory

[quinn-dougherty]

Can we maybe pass test files to dune like you suggested? It would maybe bring us further away from using a proper python test harness like pytest, but who's to say we need to be on a proper python test harness.

[ejgallego]

pytest, but who's to say we need to be on a proper python test harness.

Up to us indeed, but actually it is not that hard to make pytest work, usually the way people integrate this is to add a dune rule for running pytest.

This way you can ensure a) the correct deps are built and b) the test suite is run in a hygineic mode, and some other features of dune such as different profiles are used.

So a rule like that would be (need to fix the paths)

(rule
  (targets test_results.log)
  (deps pycoq.so pycoq.py (glob tests/*.py) etc....)
  (action (run pytest args...)))

[quinn-dougherty]

@ejgallego I should take a break, but perhaps you can provide the dune code you're talking about to this branch? If not I can take a crack at it when I get back.

git remote add quinn git@github.com:quinn-dougherty/pycoq.git
git fetch quinn

[quinn-dougherty]

this should be workaroundable if I import coq from inside a pytest.fixture.

[ejgallego]

Also you may want to put this inside a dune rule, actually Dune 3 supports directory targets so that would work pretty nicely I think? Depends on what the targets are.

[quinn-dougherty]

pycoq/test/dune

Line 3 in 087d3e9

(:test-dir py)

I think I already have a directory target? this seems to be working.

[ejgallego]

This has conflicts, we follow Coq policy here w.r.t. rebasing / squashing, see https://github.com/coq/coq/blob/master/CONTRIBUTING.md

[ejgallego]

Had a quick look despite the conflicts, thanks!

I think we have a few unrelated things here, I suggest we cherry-pick them to their own PR, a some of them are ready:

• Nix setup: need to look a bit more into this, but I understand it is not working yet? I think also that opam2nix should not be used, but start from the coq-serapi derivation
• renaming tests, spelling fixes: these are trivial so let's put them on their own PR so they can be merged quickly
• test-suite setup: IMHO that should also be separate from the Nix infra

[quinn-dougherty]

Had a quick look despite the conflicts, thanks!

I think we have a few unrelated things here, I suggest we cherry-pick them to their own PR, a some of them are ready:

* Nix setup: need to look a bit more into this, but I understand it is not working yet? I think also that opam2nix should not be used, but start from the coq-serapi derivation

* renaming tests, spelling fixes: these are trivial so let's put them on their own PR so they can be merged quickly

* test-suite setup: IMHO that should also be separate from the Nix infra

Roger, can make a bunch of smaller PRs.

Did the whole rebase process but I'm right back to square one, it's as if I didn't do anything.

also magit didn't give me an opportunity to squash during rebase, or i missed the option.

[Zimmi48]

You probably didn't do a true rebase, because I don't see a force-push operation here. You should probably reset hard to fc0ba5e and do it again. Furthermore, I suggest that you squash fixup commits with the commits that they are supposed to fix before rebasing, otherwise, you risk a lot of pain.