Quinn (Nov 04 2021 at 21:47): Quinn (Nov 04 2021 at 21:47):For a start, we need handle errors correctly and to adhere to Python conventions. A large amount of feedback is required from Python experts as I am not familiar with Python myself at all.
I have some battle-forged python opinions, and can certainly throw do some devops and throw pytype, pytest, hypothesis, flake8 into any codebase. but can you point me to some code that you want a python expert to look at? a scenario where you suspect the error handling isn't ideal?
Emilio Jesús Gallego Arias (Nov 04 2021 at 21:50):Hi @Quinn , that's amazing, thanks a lot for your help!
Emilio Jesús Gallego Arias (Nov 04 2021 at 21:50):Actually we have fixed the error handling problem
Emilio Jesús Gallego Arias (Nov 04 2021 at 21:51):so I think the main point now is how to package PyCoq correctly so it can be submitted to PIP etc...
Emilio Jesús Gallego Arias (Nov 04 2021 at 21:51):I am not very familiar with Python packaging
Quinn (Nov 04 2021 at 21:52):ok
Emilio Jesús Gallego Arias (Nov 04 2021 at 21:52):The way PyCoq works is as follows:
pythonlib, in such a way that we can use the OCaml runtime [and thus Coq] from Python ; this build process is standard for OCaml packages, and we could indeed upload a package to the OCaml package manager Emilio Jesús Gallego Arias (Nov 04 2021 at 21:53):so I wonder how can we have a Python package to depend on an OCaml one
Emilio Jesús Gallego Arias (Nov 04 2021 at 21:53):The way we are working is that we specify the "coq" object as an OCaml module, then we add the methods for those
Emilio Jesús Gallego Arias (Nov 04 2021 at 21:53):so in a sense, the canonical API is defined in OCaml, this is a bit more convenient
Quinn (Nov 04 2021 at 21:53):I wonder that too. I have some packaging experience with pypi but zilch with the opam ecosystem.
Emilio Jesús Gallego Arias (Nov 04 2021 at 21:54):opam will just install the .so in the corresponding root
Emilio Jesús Gallego Arias (Nov 04 2021 at 21:54):opam root I mean, that can be in $home/.opam/$switch
Emilio Jesús Gallego Arias (Nov 04 2021 at 21:54):or also local to a directory in _opam
Emilio Jesús Gallego Arias (Nov 04 2021 at 21:55):opam supports several "switches" so you can have different ocaml installations with different versions etc...
Quinn (Nov 04 2021 at 21:55):The thing is, my gut tells me (I haven't set up an environment to check) the IBM/pycoq pypi listing is something where if you pip install pycoq without the underlying ocaml situation under control, you might get into a scenario where the pip install works and code doesn't crash until runtime.
Quinn (Nov 04 2021 at 21:55):That's an outcome that IMO is worse than not being on pypi at all.
Emilio Jesús Gallego Arias (Nov 04 2021 at 21:55):ibm/pycoq has the same problem
Emilio Jesús Gallego Arias (Nov 04 2021 at 21:55):needs to have sertop installed
Emilio Jesús Gallego Arias (Nov 04 2021 at 21:56):that is to say, both python bindings need to install Coq before they can be used
Emilio Jesús Gallego Arias (Nov 04 2021 at 21:56):ibm/pycoq needs sertop which gives access to Coq via an RPC protocol
Emilio Jesús Gallego Arias (Nov 04 2021 at 21:56):ejgallego/pycoq skips the RPC and provides access to Coq via Python's FFI [using a .so]
Emilio Jesús Gallego Arias (Nov 04 2021 at 21:57):So I dunno what's the best way here, but in a sense this is the same that for example depending on gtk
Emilio Jesús Gallego Arias (Nov 04 2021 at 21:57):or any C library that will be used by the Python code
Quinn (Nov 04 2021 at 22:01):in the c or c++ dependency case, python will happily put you in a situation where a caller finds out by surprise that the dependency isn't there. So without experimenting I can guess a misconfigured opam, ocaml, sertop etc. will do the same for pycoq. An ideal solution would not have this property. Let me do some research into setup.py files real quick and see if we can dodge this property at that level.
Emilio Jesús Gallego Arias (Nov 04 2021 at 22:02):Great thanks!
Emilio Jesús Gallego Arias (Nov 04 2021 at 22:02):If that's the case that's not too bad, we can just require that Coq is installed, and if it is not, we fail gracefully
Emilio Jesús Gallego Arias (Nov 04 2021 at 22:03):installing Coq is not too hard these days using opam, so I'd be reasonable to require setting up opam first
Emilio Jesús Gallego Arias (Nov 04 2021 at 22:03):I will try to do an OPAM release ASAP
Quinn (Nov 04 2021 at 22:04):Meanwhile, I opened up this issue on the quite young python.on-nix.com project. The maintainer there might come up with a solution, which would be awesome.
Quinn (Nov 04 2021 at 22:07):Meanwhile, it looks like your examples dir is for running code to read the output, but would you like unit and/or property tests?
Emilio Jesús Gallego Arias (Nov 04 2021 at 22:07):Quinn said:
Meanwhile, I opened up this issue on the quite young
python.on-nix.comproject. The maintainer there might come up with a solution, which would be awesome.
Thanks!
Emilio Jesús Gallego Arias (Nov 04 2021 at 22:08):Quinn said:
Meanwhile, it looks like your
examplesdir is for running code to read the output, but would you like unit and/or property tests?
Definitively it would be great to set some testing infrastructure, I'd suggest to do only one small test for now, until we can push a better API
Emilio Jesús Gallego Arias (Nov 04 2021 at 22:09):The current API is just a Proof of Concept, but as I mentioned, we'll push a unified pyCoq / SerAPI soon
Emilio Jesús Gallego Arias (Nov 04 2021 at 22:09):then we can add a few more tests indeed
Emilio Jesús Gallego Arias (Nov 04 2021 at 22:09):Feel free to open a Pull Request
Quinn (Nov 04 2021 at 22:10):ok i'll get you set up to run pytest both locally and in ci and seed a testing infra that can be built on later
Emilio Jesús Gallego Arias (Nov 04 2021 at 22:55):Thanks @Quinn , just pushed a commit improving the packing on the OCaml side
Emilio Jesús Gallego Arias (Nov 04 2021 at 22:55):should make pyCoq much easier to install
Quinn (Nov 04 2021 at 22:58):that's great. I failed my first attempt at make haha. Could be a number of things.
Quinn (Nov 04 2021 at 23:00):did some snooping about a nix situation and filed a nixpkgs packaging request for ppx_python. I don't actually know how to add to nixpkgs myself yet.
Quinn (Nov 04 2021 at 23:03):@Emilio Jesús Gallego Arias i'm not sure you pushed. it still says the latest commit was 28 days ago
Emilio Jesús Gallego Arias (Nov 04 2021 at 23:05):Sorry I just did it, had trouble with the submodule
Emilio Jesús Gallego Arias (Nov 04 2021 at 23:05):You don't need ppx_python with the latest commit
Emilio Jesús Gallego Arias (Nov 04 2021 at 23:05):It is a long story, but pycoq requires both ppx_import and ppx_python
Emilio Jesús Gallego Arias (Nov 04 2021 at 23:07):and due to some portability issues it was not possible to install both
Quinn (Nov 04 2021 at 23:07):i'm not too familiar with submodules. do I cd coq-serapi; git checkout 7099b6c?
Emilio Jesús Gallego Arias (Nov 04 2021 at 23:08):it seems to be broken, one sec
Emilio Jesús Gallego Arias (Nov 04 2021 at 23:09):I also struggle with submodules, something is off
Quinn (Nov 04 2021 at 23:10):I ran cd coq-serapi; git submodule update --init --recursive which may have brought me to the wrong commit
Quinn (Nov 04 2021 at 23:15):but that was a while ago
Quinn (Nov 04 2021 at 23:15):I'm looking at this and thinking maybe we should write a .opam file? I've never used one of those before.
Emilio Jesús Gallego Arias (Nov 04 2021 at 23:15):Ok, I think I've fixed it
Quinn (Nov 04 2021 at 23:15):great
Emilio Jesús Gallego Arias (Nov 04 2021 at 23:15):There is already an opam file
Emilio Jesús Gallego Arias (Nov 04 2021 at 23:16):oh no, there is none
Emilio Jesús Gallego Arias (Nov 04 2021 at 23:16):sorry, will fix
Emilio Jesús Gallego Arias (Nov 04 2021 at 23:16):the submodule should work now, sorry for the hassle
Quinn (Nov 04 2021 at 23:17):lmk when i should git fetch upstream
Emilio Jesús Gallego Arias (Nov 04 2021 at 23:18):Done
Emilio Jesús Gallego Arias (Nov 04 2021 at 23:19):I'm always confused with git submodules, maybe you need to do git submodules sync ?
Emilio Jesús Gallego Arias (Nov 04 2021 at 23:19):Or maybe clone again? Not sure
Emilio Jesús Gallego Arias (Nov 04 2021 at 23:20):@Quinn need to go now, thanks for all the feedback
Emilio Jesús Gallego Arias (Nov 04 2021 at 23:20):will be around later today, for now the CI seems to work
Quinn (Nov 04 2021 at 23:21):cool, see ya around
Quinn (Nov 05 2021 at 00:12):why not put coq-serapi in pycoq.opam?
Emilio Jesús Gallego Arias (Nov 05 2021 at 00:13):@Quinn it will happen eventually, but we didn't yet release a version of coq-serapi with python support
Quinn (Nov 05 2021 at 00:13):oh, roger. thanks
Emilio Jesús Gallego Arias (Nov 05 2021 at 00:14):so now pycoq is building its own branch of coq-serapi
Emilio Jesús Gallego Arias (Nov 05 2021 at 00:14):OCaml has a build system called Dune
Emilio Jesús Gallego Arias (Nov 05 2021 at 00:14):which is very practical, as it allows you just to drop another project and things just work
Emilio Jesús Gallego Arias (Nov 05 2021 at 00:14):so hence the serapi submodule
Quinn (Nov 05 2021 at 00:15):i'm thinking of writing a .nix file for coq-serapi
Emilio Jesús Gallego Arias (Nov 05 2021 at 00:16):@quinn there should be already one
Emilio Jesús Gallego Arias (Nov 05 2021 at 00:16):@Théo Zimmermann may tell you more
Quinn (Nov 05 2021 at 00:16):but it might be easier to use fetchFromGitHub
Emilio Jesús Gallego Arias (Nov 05 2021 at 00:17):I'm not sure how Nix works, but IIANM, all the packages needed should be in place except for pythonlib and maybe pyml
Emilio Jesús Gallego Arias (Nov 05 2021 at 00:18):see https://github.com/ejgallego/coq-serapi/issues/241
Quinn (Nov 05 2021 at 00:57):pyml is in neither coq-serapi.opam nor pycoq.opam
Emilio Jesús Gallego Arias (Nov 05 2021 at 00:57):@Quinn it is pulled by pythonlib
Quinn (Nov 05 2021 at 00:58):roger
Emilio Jesús Gallego Arias (Nov 05 2021 at 00:58):That's actually a bad practice we do, sometimes we rely on implicit transitive deps
Emilio Jesús Gallego Arias (Nov 05 2021 at 00:58):That's been the case for a while, I should fix that in SerAPI / PyCoq
Emilio Jesús Gallego Arias (Nov 05 2021 at 00:58):Actually I have amended the opam file in a branch, now reads
Emilio Jesús Gallego Arias (Nov 05 2021 at 00:59): "ppx_base"
"ppxlib" { >= "0.15.0" & < "0.18.0" }
"pyml" { >= "20200115" }
+ pythonlib
Emilio Jesús Gallego Arias (Nov 05 2021 at 00:59):So for the nix package, you need all deps of serapi + these ones
Quinn (Nov 05 2021 at 01:00):I actually read that coq-serapi.opam and pycoq.opam are nearly identical
Quinn (Nov 05 2021 at 01:01):pycoq.opam has pythonlib and coq-serapi.opam doesn't, but that's the difference
Quinn (Nov 05 2021 at 01:01):which branch is that?
Quinn (Nov 05 2021 at 01:05):So i still don't know how pycoq.so is generated nor how coq-serapi.install is generated. This is probably because I haven't gotten make to work. I think it has something to do with coq versioning on my system, based on the error message, the coq version that gets installed via the .opam file isn't overriding the other coq version I have on $PATH, in fact I have no evidence it's installing at all.
Emilio Jesús Gallego Arias (Nov 05 2021 at 01:06):I've pushed a few more changes
Emilio Jesús Gallego Arias (Nov 05 2021 at 01:06):What message are you getting?
Emilio Jesús Gallego Arias (Nov 05 2021 at 01:06):Quinn said:
pycoq.opamhaspythonlibandcoq-serapi.opamdoesn't, but that's the difference
exactly
Emilio Jesús Gallego Arias (Nov 05 2021 at 01:07):the serapi branch for python support is this one
Emilio Jesús Gallego Arias (Nov 05 2021 at 01:07):https://github.com/ejgallego/coq-serapi/pull/240
Emilio Jesús Gallego Arias (Nov 05 2021 at 01:08):Quinn said:
So i still don't know how
pycoq.sois generated nor howcoq-serapi.installis generated. This is probably because I haven't gottenmaketo work. I think it has something to do withcoqversioning on my system, based on the error message, thecoqversion that gets installed via the.opamfile isn't overriding the othercoqversion I have on$PATH, in fact I have no evidence it's installing at all.
The generation of the .so file is just by a regular dune build command, see the makefile, same for python
Emilio Jesús Gallego Arias (Nov 05 2021 at 01:08):ocamlfind list will provide you a list of the things in scope
Emilio Jesús Gallego Arias (Nov 05 2021 at 01:09):I am not familiar with Nix (I struggle often with it), but there could be two potential problem sources:
eval $(opam env) so the right path etc... is set? Quinn (Nov 05 2021 at 01:10):i'll check it out. ocamlfind list | grep coq is empty. I used this. PR is up in draft.
Quinn (Nov 05 2021 at 01:12):eval $(opam env) put all the coq stuff in ocamlfind list | grep coq! but not coq.plugins.ring which is what I need.
Emilio Jesús Gallego Arias (Nov 05 2021 at 01:13):what's your coq version?
Emilio Jesús Gallego Arias (Nov 05 2021 at 01:13):beware it has to be 8.13 for this branch
Emilio Jesús Gallego Arias (Nov 05 2021 at 01:13):you can force opam to stay at a fixed version with opam pin add coq.8.13.1 etc...
Emilio Jesús Gallego Arias (Nov 05 2021 at 01:13):or using the opam file opam install --deps-only .
Emilio Jesús Gallego Arias (Nov 05 2021 at 01:14):pin avoids upgrades tho
Emilio Jesús Gallego Arias (Nov 05 2021 at 01:14):Coq stuff is tricky anyways, I think you may have a bit better luck starting from the serapi derivation
Emilio Jesús Gallego Arias (Nov 05 2021 at 01:14):adding the missing stuff should be easy
Quinn (Nov 05 2021 at 01:15):I know. my background system coq version is 8.12 but I was _hoping_ opam2nix would create a shell for me in which coqc --version is 8.13 since that's the one that's in the .opam file.
Emilio Jesús Gallego Arias (Nov 05 2021 at 01:16):That particular error you get is due to the version then
Quinn (Nov 05 2021 at 01:16):and opam-install --deps-only . says "Nothing to do"
Emilio Jesús Gallego Arias (Nov 05 2021 at 01:16):what does opam show coq say?
Quinn (Nov 05 2021 at 01:16):which doesn't make sense, because coq in .opam file is 8.13
Emilio Jesús Gallego Arias (Nov 05 2021 at 01:16):but if you use the derivation for serapi, your background version will be the right one I understand, but not in opam
Emilio Jesús Gallego Arias (Nov 05 2021 at 01:17):maybe both nix and opam are providing the coq version?
Emilio Jesús Gallego Arias (Nov 05 2021 at 01:17):likely you may want not to use opam if you are on nix
Emilio Jesús Gallego Arias (Nov 05 2021 at 01:18):I'm sure when the Coq Nix experts wake up they will be able to provide the right recipe maybe
Emilio Jesús Gallego Arias (Nov 05 2021 at 01:18)::)
Quinn (Nov 05 2021 at 01:18):well, some nix/store/.../coq8.13... or something would be the which coqc if nix was working.
Quinn (Nov 05 2021 at 01:18):yeah, i'd use the coqPackages.coq-serapi but we're using a non-main branch of coq-serapi
Emilio Jesús Gallego Arias (Nov 05 2021 at 01:21):can't you just pull the deps ?
Emilio Jesús Gallego Arias (Nov 05 2021 at 01:21):for that derivation, so you would have the right coq, ppx toolchaing, etc...
Emilio Jesús Gallego Arias (Nov 05 2021 at 01:21):you could just add pyml ppx_base pythonlib and you would be ok I think
Emilio Jesús Gallego Arias (Nov 05 2021 at 01:22):pycoq is just coq-serapi extended a bit
Emilio Jesús Gallego Arias (Nov 05 2021 at 01:22):know what I mean? So maybe if you just clone the derivation, and tweak it a bit, that will produce a working setup
Emilio Jesús Gallego Arias (Nov 05 2021 at 01:22):I hope
Emilio Jesús Gallego Arias (Nov 05 2021 at 01:22):sorry for not being able to help with Nix
Quinn (Nov 05 2021 at 01:23):does this .opam file look right, then?
Emilio Jesús Gallego Arias (Nov 05 2021 at 01:25):The current one is a bit more refined https://github.com/ejgallego/pycoq/blob/v8.13/pycoq.opam
Emilio Jesús Gallego Arias (Nov 05 2021 at 01:25):you may want to rebase
Quinn (Nov 05 2021 at 01:29):working on that now haha
Emilio Jesús Gallego Arias (Nov 05 2021 at 01:30):derivation for serapi is here in case it helps https://github.com/NixOS/nixpkgs/blob/master/pkgs/development/coq-modules/serapi/default.nix
Quinn (Nov 05 2021 at 01:30):is the correct submodule branch 8.13+pyml or 8.13?
Emilio Jesús Gallego Arias (Nov 05 2021 at 01:31):8.13+pyml
Quinn (Nov 05 2021 at 01:31):in any case, I had so many MCs in the submodule somehow that I had to rm -rf coq-serapi thinking a simple command would pull it back down since the data in .gitmodules is still there. one moment...
Emilio Jesús Gallego Arias (Nov 05 2021 at 01:31):yeah sometimes is better to just do that
Quinn (Nov 05 2021 at 01:33):quinn@Latitude-3340:~/Dropbox/Projects/misc-coq/pycoq$ cat .gitmodules
[submodule "coq-serapi"]
path = coq-serapi
url = https://github.com/ejgallego/coq-serapi.git
branch = v8.13+pyml```
nothing in git submodule help is working. not sync, not init, ....
Emilio Jesús Gallego Arias (Nov 05 2021 at 01:33):sometimes --force helps
Emilio Jesús Gallego Arias (Nov 05 2021 at 01:34):there is a bit of submodule state in .git
Emilio Jesús Gallego Arias (Nov 05 2021 at 01:34):gonna call it a night, thanks a lot for the efforts
Quinn (Nov 05 2021 at 01:35):i'll get this thing built, you'll see!
Quinn (Nov 05 2021 at 01:35):I need to learn ocaml packaging ecosystem better anyway
Quinn (Nov 05 2021 at 03:34):lmao, gave up on the principles of isolation since opam2nix was having the disappearing coq mystery, just ran opam pin coq 8.13.1 or whatever... and pycoq built!
Quinn (Nov 05 2021 at 04:00): Quinn (Nov 05 2021 at 05:45):pulls/10 is currently bottlenecked by telling pytest and pytype where the coq and pycoq library is, I tried dune exec -- pytest test/py and it didn't work either. I also tried cp -r test _build/default; dune exec -- pytest _build/default/test and it didn't work.
At this point it's sort of unfortunate that the nix attempted is piggybacked with this PR, there's too much different stuff going on with this PR because of the nix stuff. but I don't think it's worth backing it out.
Quinn (Nov 05 2021 at 05:46):moreover, i opened this it's quite concerning to me. I don't know how this happened, must have something to do with ocaml-origin codegen? i have no idea.
Quinn (Nov 07 2021 at 15:10):I don't understand dune exec -- python3
dune build test/py/unit/spec.py test/py/property/spec.py
dune exec -- python3 _build/default/test/py/unit/spec.py
Traceback (most recent call last):
File "_build/default/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
make: *** [Makefile:28: pyci] Error 1
Moreover I can't detect what happened between a little bit ago when things were basically working and now when I can't get examples to run
Emilio Jesús Gallego Arias (Nov 07 2021 at 15:49):See https://github.com/ejgallego/pycoq/pull/10#issuecomment-961893880 , in this case there is nothing telling dune to build pycoq.so
Emilio Jesús Gallego Arias (Nov 07 2021 at 15:49):so it fails, you need to do dune build first
Emilio Jesús Gallego Arias (Nov 07 2021 at 15:49):or write a rule
Emilio Jesús Gallego Arias (Nov 07 2021 at 15:49):the reason we use dune exec is such that the plugins env vars for Coq are properly setup
Emilio Jesús Gallego Arias (Nov 07 2021 at 15:49):compare env vs dune exec -- env
Quinn (Nov 07 2021 at 15:57):dune build is definitely getting called.
Quinn (Nov 07 2021 at 16:00):i reread your comment a couple times and it seems like it should add insight, but the actual behavior of dune exec -- isn't matching what I learned from your comment on my machine.
Quinn (Nov 07 2021 at 16:01):see my Makefile targets pyci and $(BUILDDIR)/pycoq/$(PYNAME).so (which pyci depends on)
Quinn (Nov 07 2021 at 16:04):before I run make clean,
$ ls _build/default/pycoq/
coq_init.ml coq_init.mli __init__.py pycoq.ml pycoq.mli pycoq.so
the .so exists in the _build target dir that dune writes, it just doesn't exist in ~/.local/lib/python3.8/site-packages/pycoq, and why should it.
Quinn (Nov 07 2021 at 16:05):one hypothesis was that eval $(opam env) needs to be ran from inside the Makefile
Quinn (Nov 07 2021 at 16:05):but it hasn't seemed to help.
Quinn (Nov 07 2021 at 16:05):also. Should I be doing dune clean instead of rm -rf _build?
Emilio Jesús Gallego Arias (Nov 07 2021 at 16:06):Quinn said:
also. Should I be doing
dune cleaninstead ofrm -rf _build?
They are pretty similar
Emilio Jesús Gallego Arias (Nov 07 2021 at 16:06):Quinn said:
before I run
make clean,$ ls _build/default/pycoq/ coq_init.ml coq_init.mli __init__.py pycoq.ml pycoq.mli pycoq.sothe
.soexists in the_buildtarget dir thatdunewrites, it just doesn't exist in~/.local/lib/python3.8/site-packages/pycoq, and why should it.
Yeah I have no idea how the stuff in .loca/lib etc... works, that's pip territory
Quinn (Nov 07 2021 at 16:08):exactly: pip is not communicating with dune correctly. I thought running dune exec -- pip3 ... would help, but it doesn't seem to have.
Emilio Jesús Gallego Arias (Nov 07 2021 at 16:08):Not sure I get what the problem is, but note that _build/default is a private directory to dune, so never cp stuff there manually, in this case you _must_ declare a rule in dune with the cp action
Quinn (Nov 07 2021 at 16:09):roger.
Emilio Jesús Gallego Arias (Nov 07 2021 at 16:09):this is because dune will clean up the _build directory automatically to remove stale files, basically all files it doesn't know about, this is required in order to have things such as bisect work properly
Emilio Jesús Gallego Arias (Nov 07 2021 at 16:10):Quinn said:
exactly:
pipis not communicating withdunecorrectly. I thought runningdune exec -- pip3 ...would help, but it doesn't seem to have.
there is not communication indeed, how should they communicate? dune exec -- pip3 does little, as I mentioned, just sets some env vars, but it doesn't even build the stuff
Quinn (Nov 07 2021 at 16:10):wait a minute... the cp into _build thing I did was on an older version of my Makefile, not the one I just pushed.
Emilio Jesús Gallego Arias (Nov 07 2021 at 16:10):still there I think cp requirements.txt _build/default/requirements.txt && cp README.md _build/default/README.md
Quinn (Nov 07 2021 at 16:10):is there a way to tell dune to do this? cd _build/default && dune exec -- python3 setup.py build && dune exec -- pip3 install .
Quinn (Nov 07 2021 at 16:11):oh I see.
Emilio Jesús Gallego Arias (Nov 07 2021 at 16:11):Quinn said:
is there a way to tell
duneto do this?cd _build/default && dune exec -- python3 setup.py build && dune exec -- pip3 install .
My point is that this is likely wrong
Emilio Jesús Gallego Arias (Nov 07 2021 at 16:12):that is not a context free action, but has some dependencies
Quinn (Nov 07 2021 at 16:12):you mean the dune exec i added is likely wrong?
Emilio Jesús Gallego Arias (Nov 07 2021 at 16:12):no, I mean that depends on some stuff to be built before it is called
Emilio Jesús Gallego Arias (Nov 07 2021 at 16:12):so indeed you can write a rule for that
Emilio Jesús Gallego Arias (Nov 07 2021 at 16:12):(rule
(deps ...)
(targets ...) ; whatever pips produces
(action (progn (run python3 setup.py) (run pip3 install .)))
the building target in my Makefile is this
dune build $(SERAPI) pycoq/$(PYNAME).so pycoq/__init__.py setup.py
cp requirements.txt _build/default/requirements.txt && cp README.md _build/default/README.md
cd _build/default && dune exec -- python3 setup.py build && dune exec -- pip3 install .
eval $(shell opam env)
And the error is?
Quinn (Nov 07 2021 at 16:13):sweet. where would I put that rule? in dune-project?
Emilio Jesús Gallego Arias (Nov 07 2021 at 16:13):in dune
Quinn (Nov 07 2021 at 16:14):it doesn't error, a later call to dune exec -- python3 _build/examples/ whatever.py fails
Emilio Jesús Gallego Arias (Nov 07 2021 at 16:14):what is that call supposed to do?
Emilio Jesús Gallego Arias (Nov 07 2021 at 16:14):what's the error message
Emilio Jesús Gallego Arias (Nov 07 2021 at 16:14):I am not familiar with the directory
Quinn (Nov 07 2021 at 16:15):one sec
Emilio Jesús Gallego Arias (Nov 07 2021 at 16:15):likely fails because whatever is run in the wrong cwd
Emilio Jesús Gallego Arias (Nov 07 2021 at 16:15):this I have no idea how to set the python path
Quinn (Nov 07 2021 at 16:15):yes, that's what i was thinking.
Emilio Jesús Gallego Arias (Nov 07 2021 at 16:15):if you put the python3 call in a dune rule
Emilio Jesús Gallego Arias (Nov 07 2021 at 16:15):it will be executed in the _Build/default
Emilio Jesús Gallego Arias (Nov 07 2021 at 16:16):it can even be sandboxed [important for caching build rules]
Quinn (Nov 07 2021 at 16:16):right. so, normally what you can do is PYTHONPATH=../../ python3 foo.py to for example make python's cwd be ../../
Emilio Jesús Gallego Arias (Nov 07 2021 at 16:16):Indeed, so likely python3 foo will set the cwd to . not to _build/default so the .so file is not found
Emilio Jesús Gallego Arias (Nov 07 2021 at 16:17):tho it is hard to tell without seeing the error message
Quinn (Nov 07 2021 at 16:17):Quinn said:
here
Quinn (Nov 07 2021 at 16:18):i just regenerated it in my shell before i remmebered i had already sent it ,sorry for delay.
Quinn (Nov 07 2021 at 16:28):did you want me to put that (rule in pycoq/dune or a new file in the root dir called dune?
Emilio Jesús Gallego Arias (Nov 07 2021 at 16:30):Makes more sense in the root dir I guess?
Quinn (Nov 07 2021 at 16:31):so a new file then?
Emilio Jesús Gallego Arias (Nov 07 2021 at 16:32):Sure
Quinn (Nov 07 2021 at 16:32):oh hey examples are working now
Emilio Jesús Gallego Arias (Nov 07 2021 at 16:32):nice :)
Quinn (Nov 07 2021 at 16:32):they were working, then not working, now working again
Emilio Jesús Gallego Arias (Nov 07 2021 at 16:33):likely due to a missing dependnecy
Emilio Jesús Gallego Arias (Nov 07 2021 at 16:33):it takes some time to get used to a more strict dep setting if you are coming from make
Emilio Jesús Gallego Arias (Nov 07 2021 at 16:33):make is very lenient, as it never cleans stuff etc...
Quinn (Nov 07 2021 at 16:36):well, i'd love to go full isolation with nix-shell --pure but the library i found that converts .opam files to .nix files wasn't playing nicely with coq
Quinn (Nov 07 2021 at 16:37):I kinda despise make lmao but i've been learning it recently as I prepare to build a production coq codebase. it's so hard to be in coq without using make. Dune seems bit better, perhaps we should aim to dune everything.
Quinn (Nov 07 2021 at 16:39):i mean the bottom line is my python isn't isolating properly.
Quinn (Nov 07 2021 at 16:48):meanwhile, these started showing up on dune build
Error: Program js_of_ocaml not found in the tree or in PATH
(context: default)
Hint: opam install js_of_ocaml-compiler
File "coq-serapi/sertop/dune", line 29, characters 63-72:
29 | (libraries sertop ppx_deriving_yojson.runtime zarith_stubs_js jscoq_lib))
^^^^^^^^^
Error: Library "jscoq_lib" in _build/default/coq-serapi/jscoq/coq-js is
hidden (optional with unavailable dependencies).
Hint: try:
dune external-lib-deps --missing @@default
File "coq-serapi/tests/sertop/dune", line 7, characters 0-95:
7 | (rule
8 | (targets full_env.out)
9 | (mode promote)
10 | (action (run gunzip %{dep:full_env.out.gz})))
Error: No rule found for coq-serapi/tests/sertop/full_env.out.gz```
sorry i'm having so much trouble getting on my feet here!!
Emilio Jesús Gallego Arias (Nov 07 2021 at 16:49):Oh, this is due to dune build trying to build all the artifact of coq-serapi including the js_of_ocaml stuff
Quinn (Nov 07 2021 at 16:49):Quinn said: oh i think that was because i was running dune build with no arguments.
Quinn (Nov 07 2021 at 16:49):which i don't need to do in practice
Emilio Jesús Gallego Arias (Nov 07 2021 at 16:49):Yup, that's an artifact of the inclusion of coq-serapi
Emilio Jesús Gallego Arias (Nov 07 2021 at 16:50):dune build works as dune build @all that's a bit too much here
Quinn (Nov 07 2021 at 16:55):i don't understand why pycoq/dune is (libraries pythonlib coq-serapi.serapi_v8_13 coq-serapi.sertop_v8_12) but pycoq.opam lists more deps.
Emilio Jesús Gallego Arias (Nov 07 2021 at 20:43):pycoq.opam lists set set of _all_ required deps
Emilio Jesús Gallego Arias (Nov 07 2021 at 20:43):as of now, this also includes the stuff needed by all the coq-serapi/*/dune files
Quinn (Nov 07 2021 at 20:46):ah
Emilio Jesús Gallego Arias (Nov 07 2021 at 20:47):note that there is not a perfect match between the opam deps and dune deps
Emilio Jesús Gallego Arias (Nov 07 2021 at 20:47):people is working on making it indeed more related
Emilio Jesús Gallego Arias (Nov 07 2021 at 20:48):also there is a flag in dune "implicit_transitive_deps"
Emilio Jesús Gallego Arias (Nov 07 2021 at 20:48):which is related to what you ask, but as of now, it is a bit experimental, in the OCaml world transitive deps are quite implicit
Emilio Jesús Gallego Arias (Nov 07 2021 at 20:48):as a norm, but that may break stuff and it has actually
Quinn (Nov 07 2021 at 20:51):fun
Emilio Jesús Gallego Arias (Nov 07 2021 at 21:02):I've pushed a commit to showcase how to run the tests with dune
Emilio Jesús Gallego Arias (Nov 07 2021 at 21:08):ok another commit pushing, illustrating the approach we discussed
Emilio Jesús Gallego Arias (Nov 07 2021 at 21:08):I hope it helps
Quinn (Nov 07 2021 at 21:46):thanks! this is great material. I was just learning more dune for a pure coq project today.
Quinn (Nov 07 2021 at 21:56):(rule
(alias pip-build)
dune build @pip-build doesn't show up in Makefile. should it?
Quinn (Nov 07 2021 at 21:56):i can see how it might be redundant.
Emilio Jesús Gallego Arias (Nov 07 2021 at 21:58):I added an alias to be able to run it
Emilio Jesús Gallego Arias (Nov 07 2021 at 21:58):As I'm learning about how the python stuff works myself
Emilio Jesús Gallego Arias (Nov 07 2021 at 21:58):so tests depend on pip-build
Emilio Jesús Gallego Arias (Nov 07 2021 at 21:58):or on the target build directory
Emilio Jesús Gallego Arias (Nov 07 2021 at 21:58):I dunno what's best, this is really in progress
Emilio Jesús Gallego Arias (Nov 07 2021 at 21:59):But I'm releasing the lock for now, so feel free to push it forward
Emilio Jesús Gallego Arias (Nov 07 2021 at 22:00):Now the tests fail due to other issues, the output is too precise, but they seem to be running fine, so that's good news
Quinn (Nov 07 2021 at 22:05):that's great!
Quinn (Nov 07 2021 at 22:05):yeah
Quinn (Nov 07 2021 at 22:05):i'm fixing up my branch and catching it up too where you are
Quinn (Nov 07 2021 at 22:05):I kinda manually added your new dune and abandoned most of the Makefile I had written and manually made it like your new one, but i didn't git rebase
Quinn (Nov 07 2021 at 22:10):goals of PR currently are
nix infrastructure (even if it doesn't actually work). future PRs:
make nix actually work
separately
migrate to tox for python-side stuff, might be the right call.
Emilio Jesús Gallego Arias (Nov 07 2021 at 22:19):Cool, note that it is common in our world to also have output tests
Emilio Jesús Gallego Arias (Nov 07 2021 at 22:19):this is good to track changes, and dune supports this workflow natively
Emilio Jesús Gallego Arias (Nov 07 2021 at 22:19):and allows you to review the diff, etc...
Emilio Jesús Gallego Arias (Nov 07 2021 at 22:19):so in this sense, the current "tests" that check that we output what we should are not so bad
Quinn (Nov 07 2021 at 22:20):roger
Emilio Jesús Gallego Arias (Nov 07 2021 at 22:20):but indeed clearly not enough
Quinn (Nov 07 2021 at 22:20):good to keep in mind
Quinn (Nov 07 2021 at 22:20):you said the overall software was a little unstable right now to have piles of unit or property tests just yet
Quinn (Nov 07 2021 at 22:21):$ make examples
dune build @examples/run-examples
python3 build
running build
running build_py
Error: Unable to resolve symlink
_build/default/examples/out/add_commutative.out
Error: Unable to resolve symlink
_build/default/examples/out/definitions_ast.out
Error: Unable to resolve symlink _build/default/examples/out/syntax_error.out
make: *** [Makefile:26: examples] Error 1```
(I changed the filenames in `examples`, triple checked that everything agrees across `dune` files)
do i need to mkdir out manually?
Emilio Jesús Gallego Arias (Nov 07 2021 at 22:25):That means the file examples/out/definitions_ast.out doesn't exist
Emilio Jesús Gallego Arias (Nov 07 2021 at 22:25):you need to touch it to boostrap the process indeed
Emilio Jesús Gallego Arias (Nov 07 2021 at 22:25):maybe there is a better way
Emilio Jesús Gallego Arias (Nov 07 2021 at 22:25):the message is weird, let me check if it is better in dune master
Emilio Jesús Gallego Arias (Nov 07 2021 at 22:26):it says "symlink" due to an internal detail
Quinn (Nov 07 2021 at 22:26):ok, yeah
Quinn (Nov 07 2021 at 22:27):I don't think I mind just touch in Makefile
Quinn (Nov 07 2021 at 22:27):for the time being
Quinn (Nov 07 2021 at 22:27):to get us started
Emilio Jesús Gallego Arias (Nov 07 2021 at 22:27):out files have to be committed
Emilio Jesús Gallego Arias (Nov 07 2021 at 22:27):they are the output reference
Emilio Jesús Gallego Arias (Nov 07 2021 at 22:27):so I mean, you only need to create them once
Quinn (Nov 07 2021 at 22:27):roger.
Emilio Jesús Gallego Arias (Nov 07 2021 at 22:27):or in this case rename
Emilio Jesús Gallego Arias (Nov 07 2021 at 22:28):?
Quinn (Nov 07 2021 at 22:28):ah, so if .log files are writing perfectly fine, then i should just cp whatever.log out/whatever.out?
Quinn (Nov 07 2021 at 22:28):wait do i have to touch out/whatever.out to _build/default or to the actual source?
Emilio Jesús Gallego Arias (Nov 07 2021 at 22:29):You can copy, but also you can start with an empty file
Emilio Jesús Gallego Arias (Nov 07 2021 at 22:29):dune will tell you "the test failed with this diff"
Emilio Jesús Gallego Arias (Nov 07 2021 at 22:29):and you can run dune promote to accept the new output
Quinn (Nov 07 2021 at 22:29):roger.
Quinn (Nov 07 2021 at 22:31):every time i make clean/dune clean tho....
Quinn (Nov 07 2021 at 22:31):not to mention ci
Quinn (Nov 07 2021 at 22:31):the touch should be in Makefile, can even make a inCI target that only gets called in ci
Emilio Jesús Gallego Arias (Nov 07 2021 at 22:37):out is supposed to be the reference output
Emilio Jesús Gallego Arias (Nov 07 2021 at 22:37):so no need to touch it, it is supposed to be commited
Quinn (Nov 07 2021 at 22:39):ok cool
Quinn (Nov 07 2021 at 22:39):got it
Quinn (Nov 07 2021 at 23:09):lmao it would appear that dune build @rule succeeds and dune build --verbose @rule fails. They both fail in fact, but one of them hides this fact.
Emilio Jesús Gallego Arias (Nov 07 2021 at 23:14):The rule as such it is not failing, otherwise dune would print also in regular mode
Emilio Jesús Gallego Arias (Nov 07 2021 at 23:14):maybe the rule is ignoring something
Quinn (Nov 07 2021 at 23:15):okk
Quinn (Nov 07 2021 at 23:15):do we need opam install --deps-only . in ci if dune handles everything? I guess dune isn't ingesting .opam file so, the answer is yes?
Quinn (Nov 07 2021 at 23:18):ok i think i'm ready, if the ci passes. have to fix mc's tho
Quinn (Nov 07 2021 at 23:18):do you mind if i do it? the MC's are things like name changes, housekeeping
Emilio Jesús Gallego Arias (Nov 07 2021 at 23:19):Yes, dune only handles the build, not the package install
Emilio Jesús Gallego Arias (Nov 07 2021 at 23:20):of "global" ocaml libraries
Emilio Jesús Gallego Arias (Nov 07 2021 at 23:20):What's an MC?
Quinn (Nov 07 2021 at 23:20):merge conflict.
Emilio Jesús Gallego Arias (Nov 07 2021 at 23:20):oh indeed, please rebase
Emilio Jesús Gallego Arias (Nov 07 2021 at 23:20):and squash as needed
Emilio Jesús Gallego Arias (Nov 07 2021 at 23:20):will review ASAP once you undraft
Quinn (Nov 07 2021 at 23:21):hm I think the best thing to do is the web interface resolver, rebasing would be much worse. The thing is, it pushes commits to main prematurely when you use the web interface.
Emilio Jesús Gallego Arias (Nov 07 2021 at 23:22):In Coq we always rebase and the workflow is actually good
Emilio Jesús Gallego Arias (Nov 07 2021 at 23:22):actually you may want to cherry-pick to different PRs
Emilio Jesús Gallego Arias (Nov 07 2021 at 23:23):if the title is accurate, the nix stuff is independent of the other adjustments, isn't it?
Emilio Jesús Gallego Arias (Nov 07 2021 at 23:24):For sure you want to squash most of it
Quinn (Nov 07 2021 at 23:25):what do you mean squash?
Emilio Jesús Gallego Arias (Nov 07 2021 at 23:26):commit squashing
Emilio Jesús Gallego Arias (Nov 07 2021 at 23:27):so history doesn't include temporal and internal commits
Quinn (Nov 07 2021 at 23:28):yeah
Quinn (Nov 07 2021 at 23:28):roger
Quinn (Nov 07 2021 at 23:29):what's the commit i should rebase from?
Emilio Jesús Gallego Arias (Nov 07 2021 at 23:31):from master?
Emilio Jesús Gallego Arias (Nov 07 2021 at 23:32):are you experienced with rebasing? If not let me know and I'll be happy to help
Quinn (Nov 07 2021 at 23:32):ah, got it
Quinn (Nov 07 2021 at 23:32):i've done it like 3 times... last time was march 2020 haha
Quinn (Nov 07 2021 at 23:32):so i'm planning to review
Quinn (Nov 07 2021 at 23:33):it's not master tho right it's v8.13
Emilio Jesús Gallego Arias (Nov 07 2021 at 23:33):indeed, sorry
Emilio Jesús Gallego Arias (Nov 07 2021 at 23:33):v8.13
Emilio Jesús Gallego Arias (Nov 07 2021 at 23:33):to rebase it is key to have a good User Interfae
Emilio Jesús Gallego Arias (Nov 07 2021 at 23:33):Interface
Emilio Jesús Gallego Arias (Nov 07 2021 at 23:33):I use magit, but there are many
Emilio Jesús Gallego Arias (Nov 07 2021 at 23:34):if you have to rebase with the command line interface you'll be in problems
Quinn (Nov 07 2021 at 23:34):i have magit installed, now's a great time to actually use it's serious features
Quinn (Nov 07 2021 at 23:34):so
Quinn (Nov 07 2021 at 23:35):oh this is pretty straightforward
Emilio Jesús Gallego Arias (Nov 07 2021 at 23:37):IMVHO programming with rebasing requires a bit of thinking ahead as to how to structure the commits
Emilio Jesús Gallego Arias (Nov 07 2021 at 23:37):but pays off a lot in the long term
Emilio Jesús Gallego Arias (Nov 07 2021 at 23:37):in Coq we systematically rebase everything and IMHO has worked super well
Emilio Jesús Gallego Arias (Nov 07 2021 at 23:37):people do write commits that are quite "modular"
Emilio Jesús Gallego Arias (Nov 07 2021 at 23:37):so they can be foward/backwards ported easily
Emilio Jesús Gallego Arias (Nov 07 2021 at 23:37):but YMMV
Emilio Jesús Gallego Arias (Nov 07 2021 at 23:37):I did struggle with rebase a lot at first
Quinn (Nov 07 2021 at 23:40):ok in magit
Quinn (Nov 07 2021 at 23:40):Screenshot-from-2021-11-07-18-40-10.png i'm here, and i manually fixed the mc at the commit with message nixified
Quinn (Nov 07 2021 at 23:41):how do i continue onwards, admitting in join and flipping it to done since i fixed everything
Quinn (Nov 07 2021 at 23:45):ah, M-x git-rebase-continue
Quinn (Nov 07 2021 at 23:55):once i've got it all worked out locally a git push origin<which is my fork> mybranch is acceptable to do with a fastforward?
Quinn (Nov 07 2021 at 23:58):aaand i think my issue is a commit i was tryign to skip was a commit where i messed up the submodule
Quinn (Nov 08 2021 at 00:00):woah, it looks like the MCs didn't change at all after I rebased
Quinn (Nov 08 2021 at 00:01):just saw your comment.
Quinn (Nov 08 2021 at 00:03):haha my rebase was in vein https://github.com/ejgallego/pycoq/pull/10#issuecomment-962707235 --- currently thinking of putting up three PRs freshly branching off v8.13 as you suggested.
Quinn (Nov 08 2021 at 00:06):weird how the rebase process just duplicated all my commits, unless i did something wrong.
Quinn (Nov 08 2021 at 00:24):well, I decided that since my commits weren't compositional enough I'm not gonna try to salvage the branch, and i'm instead going to make three unrelated branches, manually copy pasting some of the work i did. But doing better to isolate concerns and make atomic/compositional commits!
Quinn (Nov 08 2021 at 00:25):btw, the build from your latest commit is failing
Last updated: Feb 09 2023 at 02:02 UTC