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?
Hi @Quinn , that's amazing, thanks a lot for your help!
Actually we have fixed the error handling problem
so I think the main point now is how to package PyCoq correctly so it can be submitted to PIP etc...
I am not very familiar with Python packaging
ok
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 managerso I wonder how can we have a Python package to depend on an OCaml one
The way we are working is that we specify the "coq" object as an OCaml module, then we add the methods for those
so in a sense, the canonical API is defined in OCaml, this is a bit more convenient
I wonder that too. I have some packaging experience with pypi
but zilch with the opam
ecosystem.
opam will just install the .so in the corresponding root
opam root I mean, that can be in $home/.opam/$switch
or also local to a directory in _opam
opam supports several "switches" so you can have different ocaml installations with different versions etc...
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.
That's an outcome that IMO is worse than not being on pypi
at all.
ibm/pycoq has the same problem
needs to have sertop
installed
that is to say, both python bindings need to install Coq before they can be used
ibm/pycoq needs sertop
which gives access to Coq via an RPC protocol
ejgallego/pycoq skips the RPC and provides access to Coq via Python's FFI [using a .so]
So I dunno what's the best way here, but in a sense this is the same that for example depending on gtk
or any C library that will be used by the Python code
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.
Great thanks!
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
installing Coq is not too hard these days using opam, so I'd be reasonable to require setting up opam first
I will try to do an OPAM release ASAP
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.
Meanwhile, it looks like your examples
dir is for running code to read the output, but would you like unit and/or property tests?
Quinn said:
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.
Thanks!
Quinn said:
Meanwhile, it looks like your
examples
dir 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
The current API is just a Proof of Concept, but as I mentioned, we'll push a unified pyCoq / SerAPI soon
then we can add a few more tests indeed
Feel free to open a Pull Request
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
Thanks @Quinn , just pushed a commit improving the packing on the OCaml side
should make pyCoq much easier to install
that's great. I failed my first attempt at make
haha. Could be a number of things.
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.
@Emilio Jesús Gallego Arias i'm not sure you pushed. it still says the latest commit was 28 days ago
Sorry I just did it, had trouble with the submodule
You don't need ppx_python with the latest commit
It is a long story, but pycoq requires both ppx_import and ppx_python
and due to some portability issues it was not possible to install both
i'm not too familiar with submodules
. do I cd coq-serapi; git checkout 7099b6c
?
it seems to be broken, one sec
I also struggle with submodules, something is off
I ran cd coq-serapi; git submodule update --init --recursive
which may have brought me to the wrong commit
but that was a while ago
I'm looking at this and thinking maybe we should write a .opam
file? I've never used one of those before.
Ok, I think I've fixed it
great
There is already an opam file
oh no, there is none
sorry, will fix
the submodule should work now, sorry for the hassle
lmk when i should git fetch upstream
Done
I'm always confused with git submodules, maybe you need to do git submodules sync
?
Or maybe clone again? Not sure
@Quinn need to go now, thanks for all the feedback
will be around later today, for now the CI seems to work
cool, see ya around
why not put coq-serapi
in pycoq.opam
?
@Quinn it will happen eventually, but we didn't yet release a version of coq-serapi with python support
oh, roger. thanks
so now pycoq is building its own branch of coq-serapi
OCaml has a build system called Dune
which is very practical, as it allows you just to drop another project and things just work
so hence the serapi submodule
i'm thinking of writing a .nix
file for coq-serapi
@quinn there should be already one
@Théo Zimmermann may tell you more
but it might be easier to use fetchFromGitHub
I'm not sure how Nix works, but IIANM, all the packages needed should be in place except for pythonlib
and maybe pyml
see https://github.com/ejgallego/coq-serapi/issues/241
pyml
is in neither coq-serapi.opam
nor pycoq.opam
@Quinn it is pulled by pythonlib
roger
That's actually a bad practice we do, sometimes we rely on implicit transitive deps
That's been the case for a while, I should fix that in SerAPI / PyCoq
Actually I have amended the opam file in a branch, now reads
"ppx_base"
"ppxlib" { >= "0.15.0" & < "0.18.0" }
"pyml" { >= "20200115" }
+ pythonlib
So for the nix package, you need all deps of serapi + these ones
I actually read that coq-serapi.opam
and pycoq.opam
are nearly identical
pycoq.opam
has pythonlib
and coq-serapi.opam
doesn't, but that's the difference
which branch is that?
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.
I've pushed a few more changes
What message are you getting?
Quinn said:
pycoq.opam
haspythonlib
andcoq-serapi.opam
doesn't, but that's the difference
exactly
the serapi branch for python support is this one
https://github.com/ejgallego/coq-serapi/pull/240
Quinn said:
So i still don't know how
pycoq.so
is generated nor howcoq-serapi.install
is generated. This is probably because I haven't gottenmake
to work. I think it has something to do withcoq
versioning on my system, based on the error message, thecoq
version that gets installed via the.opam
file isn't overriding the othercoq
version 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
ocamlfind list
will provide you a list of the things in scope
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?i'll check it out. ocamlfind list | grep coq
is empty. I used this. PR is up in draft.
eval $(opam env)
put all the coq
stuff in ocamlfind list | grep coq
! but not coq.plugins.ring
which is what I need.
what's your coq version?
beware it has to be 8.13 for this branch
you can force opam to stay at a fixed version with opam pin add coq.8.13.1
etc...
or using the opam file opam install --deps-only .
pin avoids upgrades tho
Coq stuff is tricky anyways, I think you may have a bit better luck starting from the serapi derivation
adding the missing stuff should be easy
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.
That particular error you get is due to the version then
and opam-install --deps-only .
says "Nothing to do"
what does opam show coq
say?
which doesn't make sense, because coq
in .opam
file is 8.13
but if you use the derivation for serapi, your background version will be the right one I understand, but not in opam
maybe both nix and opam are providing the coq version?
likely you may want not to use opam if you are on nix
I'm sure when the Coq Nix experts wake up they will be able to provide the right recipe maybe
:)
well, some nix/store/.../coq8.13...
or something would be the which coqc
if nix was working.
yeah, i'd use the coqPackages.coq-serapi
but we're using a non-main branch of coq-serapi
can't you just pull the deps ?
for that derivation, so you would have the right coq, ppx toolchaing, etc...
you could just add pyml ppx_base pythonlib and you would be ok I think
pycoq is just coq-serapi extended a bit
know what I mean? So maybe if you just clone the derivation, and tweak it a bit, that will produce a working setup
I hope
sorry for not being able to help with Nix
does this .opam
file look right, then?
The current one is a bit more refined https://github.com/ejgallego/pycoq/blob/v8.13/pycoq.opam
you may want to rebase
working on that now haha
derivation for serapi is here in case it helps https://github.com/NixOS/nixpkgs/blob/master/pkgs/development/coq-modules/serapi/default.nix
is the correct submodule branch 8.13+pyml
or 8.13
?
8.13+pyml
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...
yeah sometimes is better to just do that
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
, ....
sometimes --force helps
there is a bit of submodule state in .git
gonna call it a night, thanks a lot for the efforts
i'll get this thing built, you'll see!
I need to learn ocaml packaging ecosystem better anyway
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!
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.
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.
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
See https://github.com/ejgallego/pycoq/pull/10#issuecomment-961893880 , in this case there is nothing telling dune to build pycoq.so
so it fails, you need to do dune build
first
or write a rule
the reason we use dune exec
is such that the plugins env vars for Coq are properly setup
compare env
vs dune exec -- env
dune build
is definitely getting called.
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.
see my Makefile
targets pyci
and $(BUILDDIR)/pycoq/$(PYNAME).so
(which pyci
depends on)
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.
one hypothesis was that eval $(opam env)
needs to be ran from inside the Makefile
but it hasn't seemed to help.
also. Should I be doing dune clean
instead of rm -rf _build
?
Quinn said:
also. Should I be doing
dune clean
instead ofrm -rf _build
?
They are pretty similar
Quinn said:
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 thatdune
writes, 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
exactly: pip
is not communicating with dune
correctly. I thought running dune exec -- pip3 ...
would help, but it doesn't seem to have.
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
roger.
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
Quinn said:
exactly:
pip
is not communicating withdune
correctly. 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
wait a minute... the cp
into _build
thing I did was on an older version of my Makefile
, not the one I just pushed.
still there I think cp requirements.txt _build/default/requirements.txt && cp README.md _build/default/README.md
is there a way to tell dune
to do this? cd _build/default && dune exec -- python3 setup.py build && dune exec -- pip3 install .
oh I see.
Quinn said:
is there a way to tell
dune
to do this?cd _build/default && dune exec -- python3 setup.py build && dune exec -- pip3 install .
My point is that this is likely wrong
that is not a context free action, but has some dependencies
you mean the dune exec
i added is likely wrong?
no, I mean that depends on some stuff to be built before it is called
so indeed you can write a rule for that
(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?
sweet. where would I put that rule
? in dune-project
?
in dune
it doesn't error, a later call to dune exec -- python3 _build/examples/ whatever.py
fails
what is that call supposed to do?
what's the error message
I am not familiar with the directory
one sec
likely fails because whatever is run in the wrong cwd
this I have no idea how to set the python path
yes, that's what i was thinking.
if you put the python3 call in a dune rule
it will be executed in the _Build/default
it can even be sandboxed [important for caching build rules]
right. so, normally what you can do is PYTHONPATH=../../ python3 foo.py
to for example make python's cwd
be ../../
Indeed, so likely python3 foo
will set the cwd to . not to _build/default so the .so file is not found
tho it is hard to tell without seeing the error message
Quinn said:
here
i just regenerated it in my shell before i remmebered i had already sent it ,sorry for delay.
did you want me to put that (rule
in pycoq/dune
or a new file in the root dir called dune
?
Makes more sense in the root dir I guess?
so a new file then?
Sure
oh hey examples are working now
nice :)
they were working, then not working, now working again
likely due to a missing dependnecy
it takes some time to get used to a more strict dep setting if you are coming from make
make is very lenient, as it never cleans stuff etc...
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
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.
i mean the bottom line is my python isn't isolating properly.
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!!
Oh, this is due to dune build
trying to build all the artifact of coq-serapi including the js_of_ocaml stuff
Quinn said: oh i think that was because i was running dune build
with no arguments.
which i don't need to do in practice
Yup, that's an artifact of the inclusion of coq-serapi
dune build
works as dune build @all
that's a bit too much here
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.
pycoq.opam lists set set of _all_ required deps
as of now, this also includes the stuff needed by all the coq-serapi/*/dune
files
ah
note that there is not a perfect match between the opam deps and dune deps
people is working on making it indeed more related
also there is a flag in dune "implicit_transitive_deps"
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
as a norm, but that may break stuff and it has actually
fun
I've pushed a commit to showcase how to run the tests with dune
ok another commit pushing, illustrating the approach we discussed
I hope it helps
thanks! this is great material. I was just learning more dune
for a pure coq
project today.
(rule
(alias pip-build)
dune build @pip-build
doesn't show up in Makefile
. should it?
i can see how it might be redundant.
I added an alias to be able to run it
As I'm learning about how the python stuff works myself
so tests depend on pip-build
or on the target build
directory
I dunno what's best, this is really in progress
But I'm releasing the lock for now, so feel free to push it forward
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
that's great!
yeah
i'm fixing up my branch and catching it up too where you are
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
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.
Cool, note that it is common in our world to also have output tests
this is good to track changes, and dune supports this workflow natively
and allows you to review the diff, etc...
so in this sense, the current "tests" that check that we output what we should are not so bad
roger
but indeed clearly not enough
good to keep in mind
you said the overall software was a little unstable right now to have piles of unit or property tests just yet
$ 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?
That means the file examples/out/definitions_ast.out doesn't exist
you need to touch it to boostrap the process indeed
maybe there is a better way
the message is weird, let me check if it is better in dune master
it says "symlink" due to an internal detail
ok, yeah
I don't think I mind just touch
in Makefile
for the time being
to get us started
out files have to be committed
they are the output reference
so I mean, you only need to create them once
roger.
or in this case rename
?
ah, so if .log
files are writing perfectly fine, then i should just cp whatever.log out/whatever.out
?
wait do i have to touch out/whatever.out
to _build/default
or to the actual source?
You can copy, but also you can start with an empty file
dune will tell you "the test failed with this diff"
and you can run dune promote
to accept the new output
roger.
every time i make clean
/dune clean
tho....
not to mention ci
the touch
should be in Makefile
, can even make a inCI
target that only gets called in ci
out is supposed to be the reference output
so no need to touch it, it is supposed to be commited
ok cool
got it
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.
The rule as such it is not failing, otherwise dune would print also in regular mode
maybe the rule is ignoring something
okk
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?
ok i think i'm ready, if the ci passes. have to fix mc's tho
do you mind if i do it? the MC's are things like name changes, housekeeping
Yes, dune only handles the build, not the package install
of "global" ocaml libraries
What's an MC?
merge conflict.
oh indeed, please rebase
and squash as needed
will review ASAP once you undraft
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.
In Coq we always rebase and the workflow is actually good
actually you may want to cherry-pick to different PRs
if the title is accurate, the nix stuff is independent of the other adjustments, isn't it?
For sure you want to squash most of it
what do you mean squash?
commit squashing
so history doesn't include temporal and internal commits
yeah
roger
what's the commit i should rebase from?
from master?
are you experienced with rebasing? If not let me know and I'll be happy to help
ah, got it
i've done it like 3 times... last time was march 2020 haha
so i'm planning to review
it's not master
tho right it's v8.13
indeed, sorry
v8.13
to rebase it is key to have a good User Interfae
Interface
I use magit, but there are many
if you have to rebase with the command line interface you'll be in problems
i have magit installed, now's a great time to actually use it's serious features
so
oh this is pretty straightforward
IMVHO programming with rebasing requires a bit of thinking ahead as to how to structure the commits
but pays off a lot in the long term
in Coq we systematically rebase everything and IMHO has worked super well
people do write commits that are quite "modular"
so they can be foward/backwards ported easily
but YMMV
I did struggle with rebase a lot at first
ok in magit
Screenshot-from-2021-11-07-18-40-10.png i'm here, and i manually fixed the mc at the commit with message nixified
how do i continue onwards, admitting in join
and flipping it to done
since i fixed everything
ah, M-x git-rebase-continue
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?
aaand i think my issue is a commit i was tryign to skip was a commit where i messed up the submodule
woah, it looks like the MCs didn't change at all after I rebased
just saw your comment.
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.
weird how the rebase process just duplicated all my commits, unless i did something wrong.
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!
btw, the build from your latest commit is failing
Last updated: Feb 09 2023 at 02:02 UTC